Step | Hyp | Ref
| Expression |
1 | | ltexnqi 6507 |
. . . . . 6
⊢ (𝑞 <Q
𝑟 → ∃𝑤 ∈ Q (𝑞 +Q
𝑤) = 𝑟) |
2 | 1 | adantl 262 |
. . . . 5
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → ∃𝑤 ∈ Q (𝑞 +Q
𝑤) = 𝑟) |
3 | | ltrelpr 6603 |
. . . . . . . . . 10
⊢
<P ⊆ (P ×
P) |
4 | 3 | brel 4392 |
. . . . . . . . 9
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
5 | 4 | simpld 105 |
. . . . . . . 8
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
6 | | prop 6573 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
7 | | prarloc 6601 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑤 ∈ Q) →
∃𝑧 ∈
(1st ‘𝐴)∃𝑦 ∈ (2nd ‘𝐴)𝑦 <Q (𝑧 +Q
𝑤)) |
8 | 6, 7 | sylan 267 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑤 ∈ Q)
→ ∃𝑧 ∈
(1st ‘𝐴)∃𝑦 ∈ (2nd ‘𝐴)𝑦 <Q (𝑧 +Q
𝑤)) |
9 | 5, 8 | sylan 267 |
. . . . . . 7
⊢ ((𝐴<P
𝐵 ∧ 𝑤 ∈ Q) → ∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)𝑦 <Q (𝑧 +Q
𝑤)) |
10 | 9 | ad2ant2r 478 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → ∃𝑧 ∈ (1st ‘𝐴)∃𝑦 ∈ (2nd ‘𝐴)𝑦 <Q (𝑧 +Q
𝑤)) |
11 | 4 | simprd 107 |
. . . . . . . . . . . . . 14
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
12 | 11 | ad2antrr 457 |
. . . . . . . . . . . . 13
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → 𝐵 ∈ P) |
13 | 12 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) ∧ 𝑦 <Q (𝑧 +Q
𝑤)) → 𝐵 ∈
P) |
14 | | ltanqg 6498 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
15 | 14 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧
ℎ ∈ Q))
→ (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
16 | | elprnqu 6580 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑦 ∈ (2nd
‘𝐴)) → 𝑦 ∈
Q) |
17 | 6, 16 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ (2nd
‘𝐴)) → 𝑦 ∈
Q) |
18 | 5, 17 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑦 ∈ Q) |
19 | 18 | adantlr 446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑦 ∈ Q) |
20 | 19 | ad2ant2rl 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → 𝑦 ∈ Q) |
21 | | elprnql 6579 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (1st
‘𝐴)) → 𝑧 ∈
Q) |
22 | 6, 21 | sylan 267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (1st
‘𝐴)) → 𝑧 ∈
Q) |
23 | 5, 22 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴<P
𝐵 ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 ∈ Q) |
24 | 23 | adantlr 446 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 ∈ Q) |
25 | 24 | ad2ant2r 478 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → 𝑧 ∈ Q) |
26 | | simplrl 487 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → 𝑤 ∈ Q) |
27 | | addclnq 6473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑧
+Q 𝑤) ∈ Q) |
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑧 +Q 𝑤) ∈
Q) |
29 | | ltrelnq 6463 |
. . . . . . . . . . . . . . . . . . 19
⊢
<Q ⊆ (Q ×
Q) |
30 | 29 | brel 4392 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 <Q
𝑟 → (𝑞 ∈ Q ∧
𝑟 ∈
Q)) |
31 | 30 | simpld 105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 <Q
𝑟 → 𝑞 ∈ Q) |
32 | 31 | adantl 262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → 𝑞 ∈ Q) |
33 | 32 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → 𝑞 ∈ Q) |
34 | | addcomnqg 6479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
35 | 34 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) →
(𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
36 | 15, 20, 28, 33, 35 | caovord2d 5670 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑦 <Q (𝑧 +Q
𝑤) ↔ (𝑦 +Q
𝑞)
<Q ((𝑧 +Q 𝑤) +Q
𝑞))) |
37 | | addassnqg 6480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ Q ∧
𝑤 ∈ Q
∧ 𝑞 ∈
Q) → ((𝑧
+Q 𝑤) +Q 𝑞) = (𝑧 +Q (𝑤 +Q
𝑞))) |
38 | 25, 26, 33, 37 | syl3anc 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → ((𝑧 +Q 𝑤) +Q
𝑞) = (𝑧 +Q (𝑤 +Q
𝑞))) |
39 | | addcomnqg 6479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Q ∧
𝑞 ∈ Q)
→ (𝑤
+Q 𝑞) = (𝑞 +Q 𝑤)) |
40 | 26, 33, 39 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑤 +Q 𝑞) = (𝑞 +Q 𝑤)) |
41 | 40 | oveq2d 5528 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑧 +Q (𝑤 +Q
𝑞)) = (𝑧 +Q (𝑞 +Q
𝑤))) |
42 | | simplrr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑞 +Q 𝑤) = 𝑟) |
43 | 42 | oveq2d 5528 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑧 +Q (𝑞 +Q
𝑤)) = (𝑧 +Q 𝑟)) |
44 | 38, 41, 43 | 3eqtrd 2076 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → ((𝑧 +Q 𝑤) +Q
𝑞) = (𝑧 +Q 𝑟)) |
45 | 44 | breq2d 3776 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → ((𝑦 +Q 𝑞) <Q
((𝑧
+Q 𝑤) +Q 𝑞) ↔ (𝑦 +Q 𝑞) <Q
(𝑧
+Q 𝑟))) |
46 | 36, 45 | bitrd 177 |
. . . . . . . . . . . . 13
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑦 <Q (𝑧 +Q
𝑤) ↔ (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑟))) |
47 | 46 | biimpa 280 |
. . . . . . . . . . . 12
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) ∧ 𝑦 <Q (𝑧 +Q
𝑤)) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑟)) |
48 | | prop 6573 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
49 | | prloc 6589 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑟)) → ((𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵))) |
50 | 48, 49 | sylan 267 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑞) <Q (𝑧 +Q
𝑟)) → ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵))) |
51 | 13, 47, 50 | syl2anc 391 |
. . . . . . . . . . 11
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) ∧ 𝑦 <Q (𝑧 +Q
𝑤)) → ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵))) |
52 | 51 | ex 108 |
. . . . . . . . . 10
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ (𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴))) → (𝑦 <Q (𝑧 +Q
𝑤) → ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
53 | 52 | anassrs 380 |
. . . . . . . . 9
⊢
(((((𝐴<P 𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ 𝑧 ∈ (1st ‘𝐴)) ∧ 𝑦 ∈ (2nd ‘𝐴)) → (𝑦 <Q (𝑧 +Q
𝑤) → ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
54 | 53 | reximdva 2421 |
. . . . . . . 8
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) ∧ 𝑧 ∈ (1st ‘𝐴)) → (∃𝑦 ∈ (2nd
‘𝐴)𝑦 <Q (𝑧 +Q
𝑤) → ∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
55 | 54 | reximdva 2421 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → (∃𝑧 ∈ (1st ‘𝐴)∃𝑦 ∈ (2nd ‘𝐴)𝑦 <Q (𝑧 +Q
𝑤) → ∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
56 | | prml 6575 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P →
∃𝑧 ∈
Q 𝑧 ∈
(1st ‘𝐴)) |
57 | | rexex 2368 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
Q 𝑧 ∈
(1st ‘𝐴)
→ ∃𝑧 𝑧 ∈ (1st
‘𝐴)) |
58 | 6, 56, 57 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ P →
∃𝑧 𝑧 ∈ (1st ‘𝐴)) |
59 | | r19.45mv 3315 |
. . . . . . . . . . 11
⊢
(∃𝑧 𝑧 ∈ (1st
‘𝐴) →
(∃𝑧 ∈
(1st ‘𝐴)(∃𝑦 ∈ (2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
60 | 5, 58, 59 | 3syl 17 |
. . . . . . . . . 10
⊢ (𝐴<P
𝐵 → (∃𝑧 ∈ (1st
‘𝐴)(∃𝑦 ∈ (2nd
‘𝐴)(𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
61 | 60 | adantr 261 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → (∃𝑧 ∈ (1st
‘𝐴)(∃𝑦 ∈ (2nd
‘𝐴)(𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
62 | | prmu 6576 |
. . . . . . . . . . . . 13
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P →
∃𝑥 ∈
Q 𝑥 ∈
(2nd ‘𝐴)) |
63 | | rexex 2368 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
Q 𝑥 ∈
(2nd ‘𝐴)
→ ∃𝑥 𝑥 ∈ (2nd
‘𝐴)) |
64 | 6, 62, 63 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ P →
∃𝑥 𝑥 ∈ (2nd ‘𝐴)) |
65 | | r19.9rmv 3313 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 𝑥 ∈ (2nd
‘𝐴) → ((𝑧 +Q
𝑟) ∈ (2nd
‘𝐵) ↔
∃𝑦 ∈
(2nd ‘𝐴)(𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))) |
66 | 65 | orbi2d 704 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 𝑥 ∈ (2nd
‘𝐴) →
((∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑦 ∈ (2nd
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
67 | | r19.43 2468 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
(2nd ‘𝐴)((𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑦 ∈ (2nd
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵))) |
68 | 66, 67 | syl6rbbr 188 |
. . . . . . . . . . . 12
⊢
(∃𝑥 𝑥 ∈ (2nd
‘𝐴) →
(∃𝑦 ∈
(2nd ‘𝐴)((𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
69 | 5, 64, 68 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝐴<P
𝐵 → (∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
70 | 69 | rexbidv 2327 |
. . . . . . . . . 10
⊢ (𝐴<P
𝐵 → (∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
∃𝑧 ∈
(1st ‘𝐴)(∃𝑦 ∈ (2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
71 | 70 | adantr 261 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → (∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
∃𝑧 ∈
(1st ‘𝐴)(∃𝑦 ∈ (2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
72 | | ibar 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ Q →
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))))) |
73 | 72 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ Q ∧
𝑟 ∈ Q)
→ (∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))))) |
74 | | ibar 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ Q →
(∃𝑧(𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))))) |
75 | 74 | adantl 262 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ Q ∧
𝑟 ∈ Q)
→ (∃𝑧(𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))))) |
76 | 73, 75 | orbi12d 707 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ Q ∧
𝑟 ∈ Q)
→ ((∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∨
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))) ↔ ((𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) ∨ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵)))))) |
77 | 30, 76 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑞 <Q
𝑟 → ((∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∨
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))) ↔ ((𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) ∨ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵)))))) |
78 | | ltexprlem.1 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd
‘𝐵))}〉 |
79 | 78 | ltexprlemell 6696 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (1st
‘𝐶) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
80 | 78 | ltexprlemelu 6697 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ (2nd
‘𝐶) ↔ (𝑟 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
81 | | eleq1 2100 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (1st ‘𝐴) ↔ 𝑧 ∈ (1st ‘𝐴))) |
82 | | oveq1 5519 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → (𝑦 +Q 𝑟) = (𝑧 +Q 𝑟)) |
83 | 82 | eleq1d 2106 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → ((𝑦 +Q 𝑟) ∈ (2nd
‘𝐵) ↔ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵))) |
84 | 81, 83 | anbi12d 442 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)) ↔ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
85 | 84 | cbvexv 1795 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))) |
86 | 85 | anbi2i 430 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵))) ↔ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
87 | 80, 86 | bitri 173 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (2nd
‘𝐶) ↔ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
88 | 79, 87 | orbi12i 681 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)) ↔ ((𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) ∨ (𝑟 ∈ Q ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))))) |
89 | 77, 88 | syl6rbbr 188 |
. . . . . . . . . . 11
⊢ (𝑞 <Q
𝑟 → ((𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∨
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))))) |
90 | | df-rex 2312 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ↔
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) |
91 | | df-rex 2312 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(1st ‘𝐴)(𝑧 +Q 𝑟) ∈ (2nd
‘𝐵) ↔
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵))) |
92 | 90, 91 | orbi12i 681 |
. . . . . . . . . . 11
⊢
((∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∨
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
93 | 89, 92 | syl6bbr 187 |
. . . . . . . . . 10
⊢ (𝑞 <Q
𝑟 → ((𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)) ↔
(∃𝑦 ∈
(2nd ‘𝐴)(𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
94 | 93 | adantl 262 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ (∃𝑦 ∈ (2nd
‘𝐴)(𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ ∃𝑧 ∈ (1st
‘𝐴)(𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
95 | 61, 71, 94 | 3bitr4rd 210 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
96 | 95 | adantr 261 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ∃𝑧 ∈ (1st
‘𝐴)∃𝑦 ∈ (2nd
‘𝐴)((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∨ (𝑧 +Q
𝑟) ∈ (2nd
‘𝐵)))) |
97 | 55, 96 | sylibrd 158 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → (∃𝑧 ∈ (1st ‘𝐴)∃𝑦 ∈ (2nd ‘𝐴)𝑦 <Q (𝑧 +Q
𝑤) → (𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)))) |
98 | 10, 97 | mpd 13 |
. . . . 5
⊢ (((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) ∧ (𝑤 ∈ Q ∧ (𝑞 +Q
𝑤) = 𝑟)) → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))) |
99 | 2, 98 | rexlimddv 2437 |
. . . 4
⊢ ((𝐴<P
𝐵 ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))) |
100 | 99 | ex 108 |
. . 3
⊢ (𝐴<P
𝐵 → (𝑞 <Q
𝑟 → (𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)))) |
101 | 100 | ralrimivw 2393 |
. 2
⊢ (𝐴<P
𝐵 → ∀𝑟 ∈ Q (𝑞 <Q
𝑟 → (𝑞 ∈ (1st
‘𝐶) ∨ 𝑟 ∈ (2nd
‘𝐶)))) |
102 | 101 | ralrimivw 2393 |
1
⊢ (𝐴<P
𝐵 → ∀𝑞 ∈ Q
∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))) |