Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7426 |
. . . . . . . 8
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4639 |
. . . . . . 7
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
3 | 2 | simprd 113 |
. . . . . 6
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
4 | | prop 7396 |
. . . . . 6
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
6 | | prnminu 7410 |
. . . . 5
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑤 ∈ (2nd
‘𝐵)) →
∃𝑡 ∈
(2nd ‘𝐵)𝑡 <Q 𝑤) |
7 | 5, 6 | sylan 281 |
. . . 4
⊢ ((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) → ∃𝑡 ∈ (2nd
‘𝐵)𝑡 <Q 𝑤) |
8 | | simprr 522 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → 𝑡 <Q 𝑤) |
9 | | elprnqu 7403 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑡 ∈ (2nd
‘𝐵)) → 𝑡 ∈
Q) |
10 | 5, 9 | sylan 281 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑡 ∈ (2nd ‘𝐵)) → 𝑡 ∈ Q) |
11 | 10 | ad2ant2r 501 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → 𝑡 ∈ Q) |
12 | | elprnqu 7403 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑤 ∈ (2nd
‘𝐵)) → 𝑤 ∈
Q) |
13 | 5, 12 | sylan 281 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) → 𝑤 ∈ Q) |
14 | 13 | adantr 274 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → 𝑤 ∈ Q) |
15 | | ltexnqq 7329 |
. . . . . . 7
⊢ ((𝑡 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑡
<Q 𝑤 ↔ ∃𝑣 ∈ Q (𝑡 +Q 𝑣) = 𝑤)) |
16 | 11, 14, 15 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → (𝑡 <Q 𝑤 ↔ ∃𝑣 ∈ Q (𝑡 +Q
𝑣) = 𝑤)) |
17 | 8, 16 | mpbid 146 |
. . . . 5
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → ∃𝑣 ∈ Q (𝑡 +Q
𝑣) = 𝑤) |
18 | 2 | simpld 111 |
. . . . . . . . . 10
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
19 | | prop 7396 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
21 | | prarloc 7424 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑣 ∈ Q) →
∃𝑧 ∈
(1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑧 +Q
𝑣)) |
22 | 20, 21 | sylan 281 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑣 ∈ Q) → ∃𝑧 ∈ (1st
‘𝐴)∃𝑢 ∈ (2nd
‘𝐴)𝑢 <Q (𝑧 +Q
𝑣)) |
23 | 22 | adantlr 469 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ 𝑣 ∈ Q) → ∃𝑧 ∈ (1st
‘𝐴)∃𝑢 ∈ (2nd
‘𝐴)𝑢 <Q (𝑧 +Q
𝑣)) |
24 | 23 | ad2ant2r 501 |
. . . . . 6
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) → ∃𝑧 ∈ (1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑧 +Q
𝑣)) |
25 | | simplll 523 |
. . . . . . . . . . . . 13
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) → 𝐴<P 𝐵) |
26 | 25 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝐴<P
𝐵) |
27 | | ltdfpr 7427 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) |
28 | 27 | biimpd 143 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 → ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) |
29 | 2, 28 | mpcom 36 |
. . . . . . . . . . . 12
⊢ (𝐴<P
𝐵 → ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵))) |
30 | 26, 29 | syl 14 |
. . . . . . . . . . 11
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵))) |
31 | 25 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → 𝐴<P 𝐵) |
32 | 31 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝐴<P
𝐵) |
33 | | simplrl 525 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝑧 ∈ (1st
‘𝐴)) |
34 | 33 | adantr 274 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑧 ∈ (1st
‘𝐴)) |
35 | | simprrl 529 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑞 ∈ (2nd
‘𝐴)) |
36 | | prltlu 7408 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (1st
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐴)) → 𝑧 <Q
𝑞) |
37 | 20, 36 | syl3an1 1253 |
. . . . . . . . . . . . 13
⊢ ((𝐴<P
𝐵 ∧ 𝑧 ∈ (1st ‘𝐴) ∧ 𝑞 ∈ (2nd ‘𝐴)) → 𝑧 <Q 𝑞) |
38 | 32, 34, 35, 37 | syl3anc 1220 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑧 <Q
𝑞) |
39 | | simprrr 530 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑞 ∈ (1st
‘𝐵)) |
40 | | simplrl 525 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) → 𝑡 ∈ (2nd ‘𝐵)) |
41 | 40 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → 𝑡 ∈ (2nd ‘𝐵)) |
42 | 41 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑡 ∈ (2nd
‘𝐵)) |
43 | | prltlu 7408 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑞 ∈ (1st
‘𝐵) ∧ 𝑡 ∈ (2nd
‘𝐵)) → 𝑞 <Q
𝑡) |
44 | 5, 43 | syl3an1 1253 |
. . . . . . . . . . . . 13
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ (1st ‘𝐵) ∧ 𝑡 ∈ (2nd ‘𝐵)) → 𝑞 <Q 𝑡) |
45 | 32, 39, 42, 44 | syl3anc 1220 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑞 <Q
𝑡) |
46 | | ltsonq 7319 |
. . . . . . . . . . . . 13
⊢
<Q Or Q |
47 | | ltrelnq 7286 |
. . . . . . . . . . . . 13
⊢
<Q ⊆ (Q ×
Q) |
48 | 46, 47 | sotri 4982 |
. . . . . . . . . . . 12
⊢ ((𝑧 <Q
𝑞 ∧ 𝑞 <Q 𝑡) → 𝑧 <Q 𝑡) |
49 | 38, 45, 48 | syl2anc 409 |
. . . . . . . . . . 11
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑞 ∈ Q ∧
(𝑞 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (1st
‘𝐵)))) → 𝑧 <Q
𝑡) |
50 | 30, 49 | rexlimddv 2579 |
. . . . . . . . . 10
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝑧 <Q
𝑡) |
51 | | ltexnqi 7330 |
. . . . . . . . . 10
⊢ (𝑧 <Q
𝑡 → ∃𝑠 ∈ Q (𝑧 +Q
𝑠) = 𝑡) |
52 | 50, 51 | syl 14 |
. . . . . . . . 9
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → ∃𝑠 ∈ Q (𝑧 +Q
𝑠) = 𝑡) |
53 | | simplrr 526 |
. . . . . . . . . . . 12
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → (𝑡 +Q 𝑣) = 𝑤) |
54 | 53 | ad2antrr 480 |
. . . . . . . . . . 11
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (𝑡 +Q 𝑣) = 𝑤) |
55 | | simprr 522 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (𝑧 +Q 𝑠) = 𝑡) |
56 | | oveq1 5832 |
. . . . . . . . . . . . 13
⊢ ((𝑧 +Q
𝑠) = 𝑡 → ((𝑧 +Q 𝑠) +Q
𝑣) = (𝑡 +Q 𝑣)) |
57 | 56 | eqeq1d 2166 |
. . . . . . . . . . . 12
⊢ ((𝑧 +Q
𝑠) = 𝑡 → (((𝑧 +Q 𝑠) +Q
𝑣) = 𝑤 ↔ (𝑡 +Q 𝑣) = 𝑤)) |
58 | 55, 57 | syl 14 |
. . . . . . . . . . 11
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (((𝑧 +Q 𝑠) +Q
𝑣) = 𝑤 ↔ (𝑡 +Q 𝑣) = 𝑤)) |
59 | 54, 58 | mpbird 166 |
. . . . . . . . . 10
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → ((𝑧 +Q 𝑠) +Q
𝑣) = 𝑤) |
60 | | elprnql 7402 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (1st
‘𝐴)) → 𝑧 ∈
Q) |
61 | 20, 60 | sylan 281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴<P
𝐵 ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 ∈ Q) |
62 | 61 | adantlr 469 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 ∈ Q) |
63 | 62 | ad2ant2r 501 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → 𝑧 ∈ Q) |
64 | 63 | adantlr 469 |
. . . . . . . . . . . . 13
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → 𝑧 ∈ Q) |
65 | 64 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑧 ∈ Q) |
66 | | simplrl 525 |
. . . . . . . . . . . . 13
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → 𝑣 ∈ Q) |
67 | 66 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑣 ∈ Q) |
68 | | simprl 521 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑠 ∈ Q) |
69 | | addcomnqg 7302 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
70 | 69 | adantl 275 |
. . . . . . . . . . . 12
⊢
((((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) →
(𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
71 | | addassnqg 7303 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓
+Q 𝑔) +Q ℎ) = (𝑓 +Q (𝑔 +Q
ℎ))) |
72 | 71 | adantl 275 |
. . . . . . . . . . . 12
⊢
((((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ ((𝑓
+Q 𝑔) +Q ℎ) = (𝑓 +Q (𝑔 +Q
ℎ))) |
73 | 65, 67, 68, 70, 72 | caov32d 6002 |
. . . . . . . . . . 11
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → ((𝑧 +Q 𝑣) +Q
𝑠) = ((𝑧 +Q 𝑠) +Q
𝑣)) |
74 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝑢 <Q
(𝑧
+Q 𝑣)) |
75 | | simplrr 526 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝑢 ∈ (2nd
‘𝐴)) |
76 | | prcunqu 7406 |
. . . . . . . . . . . . . . . 16
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑢 ∈ (2nd
‘𝐴)) → (𝑢 <Q
(𝑧
+Q 𝑣) → (𝑧 +Q 𝑣) ∈ (2nd
‘𝐴))) |
77 | 20, 76 | sylan 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴<P
𝐵 ∧ 𝑢 ∈ (2nd ‘𝐴)) → (𝑢 <Q (𝑧 +Q
𝑣) → (𝑧 +Q
𝑣) ∈ (2nd
‘𝐴))) |
78 | 26, 75, 77 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → (𝑢 <Q
(𝑧
+Q 𝑣) → (𝑧 +Q 𝑣) ∈ (2nd
‘𝐴))) |
79 | 74, 78 | mpd 13 |
. . . . . . . . . . . . 13
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → (𝑧 +Q
𝑣) ∈ (2nd
‘𝐴)) |
80 | 79 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (𝑧 +Q 𝑣) ∈ (2nd
‘𝐴)) |
81 | 33 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑧 ∈ (1st ‘𝐴)) |
82 | 41 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑡 ∈ (2nd ‘𝐵)) |
83 | 55, 82 | eqeltrd 2234 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (𝑧 +Q 𝑠) ∈ (2nd
‘𝐵)) |
84 | | eleq1 2220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (1st ‘𝐴) ↔ 𝑧 ∈ (1st ‘𝐴))) |
85 | | oveq1 5832 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → (𝑦 +Q 𝑠) = (𝑧 +Q 𝑠)) |
86 | 85 | eleq1d 2226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → ((𝑦 +Q 𝑠) ∈ (2nd
‘𝐵) ↔ (𝑧 +Q
𝑠) ∈ (2nd
‘𝐵))) |
87 | 84, 86 | anbi12d 465 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑠) ∈ (2nd
‘𝐵)) ↔ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑠) ∈ (2nd
‘𝐵)))) |
88 | 87 | spcegv 2800 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (1st
‘𝐴) → ((𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑠) ∈ (2nd
‘𝐵)) →
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑠) ∈ (2nd
‘𝐵)))) |
89 | 88 | anabsi5 569 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑠) ∈ (2nd
‘𝐵)) →
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑠) ∈ (2nd
‘𝐵))) |
90 | 81, 83, 89 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑠) ∈ (2nd
‘𝐵))) |
91 | | ltexprlem.1 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd
‘𝐵))}〉 |
92 | 91 | ltexprlemelu 7520 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (2nd
‘𝐶) ↔ (𝑠 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑠) ∈ (2nd
‘𝐵)))) |
93 | 68, 90, 92 | sylanbrc 414 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑠 ∈ (2nd ‘𝐶)) |
94 | 31 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝐴<P 𝐵) |
95 | 94, 18 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝐴 ∈ P) |
96 | 91 | ltexprlempr 7529 |
. . . . . . . . . . . . . 14
⊢ (𝐴<P
𝐵 → 𝐶 ∈ P) |
97 | 94, 96 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝐶 ∈ P) |
98 | | df-iplp 7389 |
. . . . . . . . . . . . . 14
⊢
+P = (𝑥 ∈ P, 𝑤 ∈ P ↦ 〈{𝑧 ∈ Q ∣
∃𝑓 ∈
Q ∃𝑣
∈ Q (𝑓
∈ (1st ‘𝑥) ∧ 𝑣 ∈ (1st ‘𝑤) ∧ 𝑧 = (𝑓 +Q 𝑣))}, {𝑧 ∈ Q ∣ ∃𝑓 ∈ Q
∃𝑣 ∈
Q (𝑓 ∈
(2nd ‘𝑥)
∧ 𝑣 ∈
(2nd ‘𝑤)
∧ 𝑧 = (𝑓 +Q
𝑣))}〉) |
99 | | addclnq 7296 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑓
+Q 𝑣) ∈ Q) |
100 | 98, 99 | genppreclu 7436 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (((𝑧
+Q 𝑣) ∈ (2nd ‘𝐴) ∧ 𝑠 ∈ (2nd ‘𝐶)) → ((𝑧 +Q 𝑣) +Q
𝑠) ∈ (2nd
‘(𝐴
+P 𝐶)))) |
101 | 95, 97, 100 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → (((𝑧 +Q 𝑣) ∈ (2nd
‘𝐴) ∧ 𝑠 ∈ (2nd
‘𝐶)) → ((𝑧 +Q
𝑣)
+Q 𝑠) ∈ (2nd ‘(𝐴 +P
𝐶)))) |
102 | 80, 93, 101 | mp2and 430 |
. . . . . . . . . . 11
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → ((𝑧 +Q 𝑣) +Q
𝑠) ∈ (2nd
‘(𝐴
+P 𝐶))) |
103 | 73, 102 | eqeltrrd 2235 |
. . . . . . . . . 10
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → ((𝑧 +Q 𝑠) +Q
𝑣) ∈ (2nd
‘(𝐴
+P 𝐶))) |
104 | 59, 103 | eqeltrrd 2235 |
. . . . . . . . 9
⊢
(((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) ∧ (𝑠 ∈ Q ∧
(𝑧
+Q 𝑠) = 𝑡)) → 𝑤 ∈ (2nd ‘(𝐴 +P
𝐶))) |
105 | 52, 104 | rexlimddv 2579 |
. . . . . . . 8
⊢
((((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) ∧ 𝑢 <Q (𝑧 +Q
𝑣)) → 𝑤 ∈ (2nd
‘(𝐴
+P 𝐶))) |
106 | 105 | ex 114 |
. . . . . . 7
⊢
(((((𝐴<P 𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (2nd ‘𝐴))) → (𝑢 <Q (𝑧 +Q
𝑣) → 𝑤 ∈ (2nd
‘(𝐴
+P 𝐶)))) |
107 | 106 | rexlimdvva 2582 |
. . . . . 6
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) → (∃𝑧 ∈ (1st ‘𝐴)∃𝑢 ∈ (2nd ‘𝐴)𝑢 <Q (𝑧 +Q
𝑣) → 𝑤 ∈ (2nd
‘(𝐴
+P 𝐶)))) |
108 | 24, 107 | mpd 13 |
. . . . 5
⊢ ((((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) ∧ (𝑣 ∈ Q ∧ (𝑡 +Q
𝑣) = 𝑤)) → 𝑤 ∈ (2nd ‘(𝐴 +P
𝐶))) |
109 | 17, 108 | rexlimddv 2579 |
. . . 4
⊢ (((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) ∧ (𝑡 ∈ (2nd ‘𝐵) ∧ 𝑡 <Q 𝑤)) → 𝑤 ∈ (2nd ‘(𝐴 +P
𝐶))) |
110 | 7, 109 | rexlimddv 2579 |
. . 3
⊢ ((𝐴<P
𝐵 ∧ 𝑤 ∈ (2nd ‘𝐵)) → 𝑤 ∈ (2nd ‘(𝐴 +P
𝐶))) |
111 | 110 | ex 114 |
. 2
⊢ (𝐴<P
𝐵 → (𝑤 ∈ (2nd
‘𝐵) → 𝑤 ∈ (2nd
‘(𝐴
+P 𝐶)))) |
112 | 111 | ssrdv 3134 |
1
⊢ (𝐴<P
𝐵 → (2nd
‘𝐵) ⊆
(2nd ‘(𝐴
+P 𝐶))) |