Step | Hyp | Ref
| Expression |
1 | | ltsonq 6382 |
. . . . . 6
⊢
<Q Or Q |
2 | | ltrelnq 6349 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
3 | 1, 2 | son2lpi 4664 |
. . . . 5
⊢ ¬
(y <Q z ∧ z <Q y) |
4 | | ltrelpr 6488 |
. . . . . . . . . . . . . . . 16
⊢
<P ⊆ (P ×
P) |
5 | 4 | brel 4335 |
. . . . . . . . . . . . . . 15
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
6 | 5 | simprd 107 |
. . . . . . . . . . . . . 14
⊢ (A<P B → B ∈ P) |
7 | | prop 6458 |
. . . . . . . . . . . . . 14
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
8 | 6, 7 | syl 14 |
. . . . . . . . . . . . 13
⊢ (A<P B → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
9 | | prltlu 6470 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ (y
+Q 𝑞)
∈ (1st ‘B) ∧ (z +Q 𝑞) ∈
(2nd ‘B)) → (y +Q 𝑞) <Q (z +Q 𝑞)) |
10 | 8, 9 | syl3an1 1167 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧
(y +Q 𝑞) ∈ (1st ‘B) ∧ (z +Q 𝑞) ∈
(2nd ‘B)) → (y +Q 𝑞) <Q (z +Q 𝑞)) |
11 | 10 | 3expb 1104 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
((y +Q 𝑞) ∈ (1st ‘B) ∧ (z +Q 𝑞) ∈
(2nd ‘B))) →
(y +Q 𝑞) <Q
(z +Q 𝑞)) |
12 | 11 | adantlr 446 |
. . . . . . . . . 10
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y
+Q 𝑞)
∈ (1st ‘B) ∧ (z +Q 𝑞) ∈
(2nd ‘B))) →
(y +Q 𝑞) <Q
(z +Q 𝑞)) |
13 | 12 | adantrll 453 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) → (y
+Q 𝑞)
<Q (z
+Q 𝑞)) |
14 | 13 | adantrrl 455 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
(y +Q 𝑞) <Q
(z +Q 𝑞)) |
15 | | ltanqg 6384 |
. . . . . . . . . 10
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g))) |
16 | 15 | adantl 262 |
. . . . . . . . 9
⊢
((((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q)) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g))) |
17 | 5 | simpld 105 |
. . . . . . . . . . . . 13
⊢ (A<P B → A ∈ P) |
18 | | prop 6458 |
. . . . . . . . . . . . 13
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . 12
⊢ (A<P B → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
20 | | elprnqu 6465 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
21 | 19, 20 | sylan 267 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
y ∈
(2nd ‘A)) → y ∈
Q) |
22 | 21 | ad2ant2r 478 |
. . . . . . . . . 10
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) → y ∈
Q) |
23 | 22 | adantrr 448 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
y ∈
Q) |
24 | | elprnql 6464 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
25 | 19, 24 | sylan 267 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
z ∈
(1st ‘A)) → z ∈
Q) |
26 | 25 | ad2ant2r 478 |
. . . . . . . . . 10
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))) → z ∈
Q) |
27 | 26 | adantrl 447 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
z ∈
Q) |
28 | | simplr 482 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) → 𝑞 ∈ Q) |
29 | | addcomnqg 6365 |
. . . . . . . . . 10
⊢
((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g
+Q f)) |
30 | 29 | adantl 262 |
. . . . . . . . 9
⊢
((((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) ∧ (f ∈ Q ∧ g ∈ Q)) → (f +Q g) = (g
+Q f)) |
31 | 16, 23, 27, 28, 30 | caovord2d 5612 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
(y <Q z ↔ (y
+Q 𝑞)
<Q (z
+Q 𝑞))) |
32 | 14, 31 | mpbird 156 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
y <Q z) |
33 | | prltlu 6470 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A) ∧ y ∈
(2nd ‘A)) → z <Q y) |
34 | 19, 33 | syl3an1 1167 |
. . . . . . . . . . . 12
⊢
((A<P
B ∧
z ∈
(1st ‘A) ∧ y ∈ (2nd ‘A)) → z
<Q y) |
35 | 34 | 3com23 1109 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
y ∈
(2nd ‘A) ∧ z ∈ (1st ‘A)) → z
<Q y) |
36 | 35 | 3expb 1104 |
. . . . . . . . . 10
⊢
((A<P
B ∧
(y ∈
(2nd ‘A) ∧ z ∈ (1st ‘A))) → z
<Q y) |
37 | 36 | adantlr 446 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (y ∈ (2nd ‘A) ∧ z ∈
(1st ‘A))) → z <Q y) |
38 | 37 | adantrlr 454 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ z ∈ (1st ‘A))) → z
<Q y) |
39 | 38 | adantrrr 456 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
z <Q y) |
40 | 32, 39 | jca 290 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) →
(y <Q z ∧ z <Q y)) |
41 | 40 | ex 108 |
. . . . 5
⊢
((A<P
B ∧ 𝑞 ∈ Q) → (((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) → (y
<Q z ∧ z
<Q y))) |
42 | 3, 41 | mtoi 589 |
. . . 4
⊢
((A<P
B ∧ 𝑞 ∈ Q) → ¬ ((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
43 | 42 | alrimivv 1752 |
. . 3
⊢
((A<P
B ∧ 𝑞 ∈ Q) → ∀y∀z ¬
((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
44 | | ltexprlem.1 |
. . . . . . . . . . . 12
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
45 | 44 | ltexprlemell 6572 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
46 | 44 | ltexprlemelu 6573 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ (2nd ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)))) |
47 | 45, 46 | anbi12i 433 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶)) ↔ ((𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B))) ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
48 | | anandi 524 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ Q ∧ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))) ↔ ((𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) ∧ (𝑞 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B))))) |
49 | 47, 48 | bitr4i 176 |
. . . . . . . . 9
⊢ ((𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶)) ↔ (𝑞 ∈
Q ∧ (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B))))) |
50 | 49 | baib 827 |
. . . . . . . 8
⊢ (𝑞 ∈ Q → ((𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
51 | | eleq1 2097 |
. . . . . . . . . . 11
⊢ (y = z →
(y ∈
(1st ‘A) ↔ z ∈
(1st ‘A))) |
52 | | oveq1 5462 |
. . . . . . . . . . . 12
⊢ (y = z →
(y +Q 𝑞) = (z +Q 𝑞)) |
53 | 52 | eleq1d 2103 |
. . . . . . . . . . 11
⊢ (y = z →
((y +Q 𝑞) ∈ (2nd ‘B) ↔ (z
+Q 𝑞)
∈ (2nd ‘B))) |
54 | 51, 53 | anbi12d 442 |
. . . . . . . . . 10
⊢ (y = z →
((y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)) ↔ (z
∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) |
55 | 54 | cbvexv 1792 |
. . . . . . . . 9
⊢ (∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)) ↔ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) |
56 | 55 | anbi2i 430 |
. . . . . . . 8
⊢ ((∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B))) ↔ (∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ ∃z(z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
57 | 50, 56 | syl6bb 185 |
. . . . . . 7
⊢ (𝑞 ∈ Q → ((𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))))) |
58 | | eeanv 1804 |
. . . . . . 7
⊢ (∃y∃z((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)))) |
59 | 57, 58 | syl6bbr 187 |
. . . . . 6
⊢ (𝑞 ∈ Q → ((𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ∃y∃z((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))))) |
60 | 59 | notbid 591 |
. . . . 5
⊢ (𝑞 ∈ Q → (¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ¬ ∃y∃z((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))))) |
61 | | alnex 1385 |
. . . . . . 7
⊢ (∀z ¬
((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) ↔ ¬ ∃z((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
62 | 61 | albii 1356 |
. . . . . 6
⊢ (∀y∀z ¬
((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) ↔ ∀y ¬
∃z((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B)))) |
63 | | alnex 1385 |
. . . . . 6
⊢ (∀y ¬
∃z((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))) ↔ ¬
∃y∃z((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
64 | 62, 63 | bitri 173 |
. . . . 5
⊢ (∀y∀z ¬
((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B))) ↔ ¬ ∃y∃z((y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)) ∧ (z ∈
(1st ‘A) ∧ (z
+Q 𝑞)
∈ (2nd ‘B)))) |
65 | 60, 64 | syl6bbr 187 |
. . . 4
⊢ (𝑞 ∈ Q → (¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ∀y∀z ¬ ((y
∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))))) |
66 | 65 | adantl 262 |
. . 3
⊢
((A<P
B ∧ 𝑞 ∈ Q) → (¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ∀y∀z ¬ ((y
∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)) ∧ (z ∈ (1st ‘A) ∧ (z +Q 𝑞) ∈
(2nd ‘B))))) |
67 | 43, 66 | mpbird 156 |
. 2
⊢
((A<P
B ∧ 𝑞 ∈ Q) → ¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))) |
68 | 67 | ralrimiva 2386 |
1
⊢ (A<P B → ∀𝑞 ∈ Q ¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))) |