Step | Hyp | Ref
| Expression |
1 | | ltexnqi 6392 |
. . . . . 6
⊢ (𝑞 <Q
𝑟 → ∃w ∈ Q (𝑞 +Q w) = 𝑟) |
2 | 1 | adantl 262 |
. . . . 5
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → ∃w ∈ Q (𝑞 +Q w) = 𝑟) |
3 | | ltrelpr 6488 |
. . . . . . . . . 10
⊢
<P ⊆ (P ×
P) |
4 | 3 | brel 4335 |
. . . . . . . . 9
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
5 | 4 | simpld 105 |
. . . . . . . 8
⊢ (A<P B → A ∈ P) |
6 | | prop 6458 |
. . . . . . . . 9
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
7 | | prarloc 6486 |
. . . . . . . . 9
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ w ∈ Q) → ∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)y <Q (z +Q w)) |
8 | 6, 7 | sylan 267 |
. . . . . . . 8
⊢
((A ∈ P ∧ w ∈ Q) → ∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)y <Q (z +Q w)) |
9 | 5, 8 | sylan 267 |
. . . . . . 7
⊢
((A<P
B ∧
w ∈
Q) → ∃z ∈
(1st ‘A)∃y ∈ (2nd ‘A)y
<Q (z
+Q w)) |
10 | 9 | ad2ant2r 478 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → ∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)y <Q (z +Q w)) |
11 | 4 | simprd 107 |
. . . . . . . . . . . . . 14
⊢ (A<P B → B ∈ P) |
12 | 11 | ad2antrr 457 |
. . . . . . . . . . . . 13
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → B ∈
P) |
13 | 12 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → B
∈ P) |
14 | | ltanqg 6384 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g))) |
15 | 14 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ (f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → (f
<Q g ↔
(ℎ +Q
f) <Q (ℎ +Q
g))) |
16 | | elprnqu 6465 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
17 | 6, 16 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢
((A ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
18 | 5, 17 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢
((A<P
B ∧
y ∈
(2nd ‘A)) → y ∈
Q) |
19 | 18 | adantlr 446 |
. . . . . . . . . . . . . . . 16
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
20 | 19 | ad2ant2rl 480 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → y
∈ Q) |
21 | | elprnql 6464 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
22 | 6, 21 | sylan 267 |
. . . . . . . . . . . . . . . . . . 19
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
23 | 5, 22 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢
((A<P
B ∧
z ∈
(1st ‘A)) → z ∈
Q) |
24 | 23 | adantlr 446 |
. . . . . . . . . . . . . . . . 17
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ z ∈ (1st ‘A)) → z
∈ Q) |
25 | 24 | ad2ant2r 478 |
. . . . . . . . . . . . . . . 16
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → z
∈ Q) |
26 | | simplrl 487 |
. . . . . . . . . . . . . . . 16
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → w
∈ Q) |
27 | | addclnq 6359 |
. . . . . . . . . . . . . . . 16
⊢
((z ∈ Q ∧ w ∈ Q) → (z +Q w) ∈
Q) |
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (z
+Q w) ∈ Q) |
29 | | ltrelnq 6349 |
. . . . . . . . . . . . . . . . . . 19
⊢
<Q ⊆ (Q ×
Q) |
30 | 29 | brel 4335 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 <Q
𝑟 → (𝑞 ∈
Q ∧ 𝑟 ∈
Q)) |
31 | 30 | simpld 105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 <Q
𝑟 → 𝑞 ∈
Q) |
32 | 31 | adantl 262 |
. . . . . . . . . . . . . . . 16
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → 𝑞 ∈
Q) |
33 | 32 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → 𝑞 ∈
Q) |
34 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . 16
⊢
((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g
+Q f)) |
35 | 34 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ (f ∈
Q ∧ g ∈
Q)) → (f
+Q g) = (g +Q f)) |
36 | 15, 20, 28, 33, 35 | caovord2d 5612 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (y
<Q (z
+Q w) ↔
(y +Q 𝑞) <Q
((z +Q w) +Q 𝑞))) |
37 | | addassnqg 6366 |
. . . . . . . . . . . . . . . . 17
⊢
((z ∈ Q ∧ w ∈ Q ∧ 𝑞
∈ Q) → ((z +Q w) +Q 𝑞) = (z
+Q (w
+Q 𝑞))) |
38 | 25, 26, 33, 37 | syl3anc 1134 |
. . . . . . . . . . . . . . . 16
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → ((z
+Q w)
+Q 𝑞)
= (z +Q (w +Q 𝑞))) |
39 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . . . 18
⊢
((w ∈ Q ∧ 𝑞
∈ Q) → (w +Q 𝑞) = (𝑞 +Q w)) |
40 | 26, 33, 39 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (w
+Q 𝑞)
= (𝑞
+Q w)) |
41 | 40 | oveq2d 5471 |
. . . . . . . . . . . . . . . 16
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (z
+Q (w
+Q 𝑞)) = (z
+Q (𝑞
+Q w))) |
42 | | simplrr 488 |
. . . . . . . . . . . . . . . . 17
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (𝑞 +Q w) = 𝑟) |
43 | 42 | oveq2d 5471 |
. . . . . . . . . . . . . . . 16
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (z
+Q (𝑞
+Q w)) = (z +Q 𝑟)) |
44 | 38, 41, 43 | 3eqtrd 2073 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → ((z
+Q w)
+Q 𝑞)
= (z +Q 𝑟)) |
45 | 44 | breq2d 3767 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → ((y
+Q 𝑞)
<Q ((z
+Q w)
+Q 𝑞)
↔ (y +Q 𝑞) <Q
(z +Q 𝑟))) |
46 | 36, 45 | bitrd 177 |
. . . . . . . . . . . . 13
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (y
<Q (z
+Q w) ↔
(y +Q 𝑞) <Q
(z +Q 𝑟))) |
47 | 46 | biimpa 280 |
. . . . . . . . . . . 12
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → (y
+Q 𝑞)
<Q (z
+Q 𝑟)) |
48 | | prop 6458 |
. . . . . . . . . . . . 13
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
49 | | prloc 6474 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ (y
+Q 𝑞)
<Q (z
+Q 𝑟)) → ((y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B))) |
50 | 48, 49 | sylan 267 |
. . . . . . . . . . . 12
⊢
((B ∈ P ∧ (y
+Q 𝑞)
<Q (z
+Q 𝑟)) → ((y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B))) |
51 | 13, 47, 50 | syl2anc 391 |
. . . . . . . . . . 11
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → ((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B))) |
52 | 51 | ex 108 |
. . . . . . . . . 10
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
(z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A))) → (y
<Q (z
+Q w) →
((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
53 | 52 | anassrs 380 |
. . . . . . . . 9
⊢
(((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
z ∈
(1st ‘A)) ∧ y ∈ (2nd ‘A)) → (y
<Q (z
+Q w) →
((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
54 | 53 | reximdva 2415 |
. . . . . . . 8
⊢
((((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧
z ∈
(1st ‘A)) → (∃y ∈ (2nd ‘A)y
<Q (z
+Q w) → ∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
55 | 54 | reximdva 2415 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)y <Q (z +Q w) → ∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)((y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)))) |
56 | | prml 6460 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘A),
(2nd ‘A)〉 ∈ P → ∃z ∈ Q z ∈
(1st ‘A)) |
57 | | rexex 2362 |
. . . . . . . . . . . 12
⊢ (∃z ∈ Q z ∈
(1st ‘A) → ∃z z ∈
(1st ‘A)) |
58 | 6, 56, 57 | 3syl 17 |
. . . . . . . . . . 11
⊢ (A ∈
P → ∃z z ∈ (1st ‘A)) |
59 | | r19.45mv 3309 |
. . . . . . . . . . 11
⊢ (∃z z ∈
(1st ‘A) → (∃z ∈ (1st ‘A)(∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z
+Q 𝑟)
∈ (2nd ‘B)))) |
60 | 5, 58, 59 | 3syl 17 |
. . . . . . . . . 10
⊢ (A<P B → (∃z ∈ (1st ‘A)(∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z
+Q 𝑟)
∈ (2nd ‘B)))) |
61 | 60 | adantr 261 |
. . . . . . . . 9
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → (∃z ∈ (1st ‘A)(∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z
+Q 𝑟)
∈ (2nd ‘B)))) |
62 | | prmu 6461 |
. . . . . . . . . . . . 13
⊢
(〈(1st ‘A),
(2nd ‘A)〉 ∈ P → ∃x ∈ Q x ∈
(2nd ‘A)) |
63 | | rexex 2362 |
. . . . . . . . . . . . 13
⊢ (∃x ∈ Q x ∈
(2nd ‘A) → ∃x x ∈
(2nd ‘A)) |
64 | 6, 62, 63 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (A ∈
P → ∃x x ∈ (2nd ‘A)) |
65 | | r19.9rmv 3307 |
. . . . . . . . . . . . . 14
⊢ (∃x x ∈
(2nd ‘A) → ((z +Q 𝑟) ∈
(2nd ‘B) ↔ ∃y ∈ (2nd ‘A)(z
+Q 𝑟)
∈ (2nd ‘B))) |
66 | 65 | orbi2d 703 |
. . . . . . . . . . . . 13
⊢ (∃x x ∈
(2nd ‘A) → ((∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃y ∈ (2nd ‘A)(z
+Q 𝑟)
∈ (2nd ‘B)))) |
67 | | r19.43 2462 |
. . . . . . . . . . . . 13
⊢ (∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃y ∈ (2nd ‘A)(z
+Q 𝑟)
∈ (2nd ‘B))) |
68 | 66, 67 | syl6rbbr 188 |
. . . . . . . . . . . 12
⊢ (∃x x ∈
(2nd ‘A) → (∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
69 | 5, 64, 68 | 3syl 17 |
. . . . . . . . . . 11
⊢ (A<P B → (∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
70 | 69 | rexbidv 2321 |
. . . . . . . . . 10
⊢ (A<P B → (∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)((y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ ∃z ∈ (1st ‘A)(∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)))) |
71 | 70 | adantr 261 |
. . . . . . . . 9
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → (∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)((y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ ∃z ∈ (1st ‘A)(∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ (z
+Q 𝑟)
∈ (2nd ‘B)))) |
72 | | ibar 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ Q → (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))))) |
73 | 72 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ Q ∧ 𝑟
∈ Q) → (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))))) |
74 | | ibar 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ Q → (∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (𝑟 ∈
Q ∧ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))))) |
75 | 74 | adantl 262 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ Q ∧ 𝑟
∈ Q) → (∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (𝑟 ∈
Q ∧ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))))) |
76 | 73, 75 | orbi12d 706 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ Q ∧ 𝑟
∈ Q) → ((∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∨ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))) ↔ ((𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B)))))) |
77 | 30, 76 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑞 <Q
𝑟 → ((∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∨ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))) ↔ ((𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B)))))) |
78 | | ltexprlem.1 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
79 | 78 | ltexprlemell 6572 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
80 | 78 | ltexprlemelu 6573 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B)))) |
81 | | eleq1 2097 |
. . . . . . . . . . . . . . . . 17
⊢ (y = z →
(y ∈
(1st ‘A) ↔ z ∈
(1st ‘A))) |
82 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . 18
⊢ (y = z →
(y +Q 𝑟) = (z +Q 𝑟)) |
83 | 82 | eleq1d 2103 |
. . . . . . . . . . . . . . . . 17
⊢ (y = z →
((y +Q 𝑟) ∈ (2nd ‘B) ↔ (z
+Q 𝑟)
∈ (2nd ‘B))) |
84 | 81, 83 | anbi12d 442 |
. . . . . . . . . . . . . . . 16
⊢ (y = z →
((y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B)) ↔ (z
∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B)))) |
85 | 84 | cbvexv 1792 |
. . . . . . . . . . . . . . 15
⊢ (∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B)) ↔ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))) |
86 | 85 | anbi2i 430 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B))) ↔ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B)))) |
87 | 80, 86 | bitri 173 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈
Q ∧ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B)))) |
88 | 79, 87 | orbi12i 680 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ((𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B))))) |
89 | 77, 88 | syl6rbbr 188 |
. . . . . . . . . . 11
⊢ (𝑞 <Q
𝑟 → ((𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))
↔ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∨ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈
(2nd ‘B))))) |
90 | | df-rex 2306 |
. . . . . . . . . . . 12
⊢ (∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ↔ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) |
91 | | df-rex 2306 |
. . . . . . . . . . . 12
⊢ (∃z ∈ (1st ‘A)(z
+Q 𝑟)
∈ (2nd ‘B) ↔ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B))) |
92 | 90, 91 | orbi12i 680 |
. . . . . . . . . . 11
⊢ ((∃y ∈ (2nd ‘A)(y
+Q 𝑞)
∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z
+Q 𝑟)
∈ (2nd ‘B)) ↔ (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∨ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑟)
∈ (2nd ‘B)))) |
93 | 89, 92 | syl6bbr 187 |
. . . . . . . . . 10
⊢ (𝑞 <Q
𝑟 → ((𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))
↔ (∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ ∃z ∈
(1st ‘A)(z +Q 𝑟) ∈
(2nd ‘B)))) |
94 | 93 | adantl 262 |
. . . . . . . . 9
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → ((𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))
↔ (∃y ∈
(2nd ‘A)(y +Q 𝑞) ∈
(1st ‘B) ∨ ∃z ∈
(1st ‘A)(z +Q 𝑟) ∈
(2nd ‘B)))) |
95 | 61, 71, 94 | 3bitr4rd 210 |
. . . . . . . 8
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → ((𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))
↔ ∃z ∈
(1st ‘A)∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
96 | 95 | adantr 261 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → ((𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))
↔ ∃z ∈
(1st ‘A)∃y ∈ (2nd ‘A)((y
+Q 𝑞)
∈ (1st ‘B) ∨ (z +Q 𝑟) ∈
(2nd ‘B)))) |
97 | 55, 96 | sylibrd 158 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (∃z ∈ (1st ‘A)∃y ∈
(2nd ‘A)y <Q (z +Q w) → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶)))) |
98 | 10, 97 | mpd 13 |
. . . . 5
⊢
(((A<P
B ∧ 𝑞 <Q
𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))) |
99 | 2, 98 | rexlimddv 2431 |
. . . 4
⊢
((A<P
B ∧ 𝑞 <Q
𝑟) → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶))) |
100 | 99 | ex 108 |
. . 3
⊢ (A<P B → (𝑞 <Q 𝑟 → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶)))) |
101 | 100 | ralrimivw 2387 |
. 2
⊢ (A<P B → ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶)))) |
102 | 101 | ralrimivw 2387 |
1
⊢ (A<P B → ∀𝑞 ∈ Q ∀𝑟 ∈
Q (𝑞
<Q 𝑟 → (𝑞 ∈
(1st ‘𝐶)
∨ 𝑟 ∈
(2nd ‘𝐶)))) |