Step | Hyp | Ref
| Expression |
1 | | ltsonq 6382 |
. . . . . 6
⊢
<Q Or Q |
2 | | ltrelnq 6349 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
3 | 1, 2 | son2lpi 4664 |
. . . . 5
⊢ ¬
((*Q‘z)
<Q (*Q‘y) ∧
(*Q‘y)
<Q (*Q‘z)) |
4 | | simprr 484 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
(*Q‘z) ∈ (1st ‘A)) |
5 | | simplr 482 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
(*Q‘y) ∈ (2nd ‘A)) |
6 | 4, 5 | jca 290 |
. . . . . . . . 9
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
((*Q‘z)
∈ (1st ‘A) ∧
(*Q‘y) ∈ (2nd ‘A))) |
7 | | prop 6458 |
. . . . . . . . . . 11
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
8 | | prltlu 6470 |
. . . . . . . . . . 11
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ (*Q‘z) ∈
(1st ‘A) ∧ (*Q‘y) ∈
(2nd ‘A)) →
(*Q‘z)
<Q (*Q‘y)) |
9 | 7, 8 | syl3an1 1167 |
. . . . . . . . . 10
⊢
((A ∈ P ∧ (*Q‘z) ∈
(1st ‘A) ∧ (*Q‘y) ∈
(2nd ‘A)) →
(*Q‘z)
<Q (*Q‘y)) |
10 | 9 | 3expb 1104 |
. . . . . . . . 9
⊢
((A ∈ P ∧ ((*Q‘z) ∈
(1st ‘A) ∧ (*Q‘y) ∈
(2nd ‘A))) →
(*Q‘z)
<Q (*Q‘y)) |
11 | 6, 10 | sylan2 270 |
. . . . . . . 8
⊢
((A ∈ P ∧ ((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) →
(*Q‘z)
<Q (*Q‘y)) |
12 | | simprl 483 |
. . . . . . . . . . 11
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) → z
<Q 𝑞) |
13 | | simpll 481 |
. . . . . . . . . . 11
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) → 𝑞 <Q y) |
14 | 1, 2 | sotri 4663 |
. . . . . . . . . . 11
⊢
((z <Q
𝑞 ∧ 𝑞
<Q y) →
z <Q y) |
15 | 12, 13, 14 | syl2anc 391 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) → z
<Q y) |
16 | | ltrnqi 6404 |
. . . . . . . . . 10
⊢ (z <Q y → (*Q‘y) <Q
(*Q‘z)) |
17 | 15, 16 | syl 14 |
. . . . . . . . 9
⊢ (((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
(*Q‘y)
<Q (*Q‘z)) |
18 | 17 | adantl 262 |
. . . . . . . 8
⊢
((A ∈ P ∧ ((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) →
(*Q‘y)
<Q (*Q‘z)) |
19 | 11, 18 | jca 290 |
. . . . . . 7
⊢
((A ∈ P ∧ ((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) →
((*Q‘z)
<Q (*Q‘y) ∧
(*Q‘y)
<Q (*Q‘z))) |
20 | 19 | ex 108 |
. . . . . 6
⊢ (A ∈
P → (((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
((*Q‘z)
<Q (*Q‘y) ∧
(*Q‘y)
<Q (*Q‘z)))) |
21 | 20 | adantr 261 |
. . . . 5
⊢
((A ∈ P ∧ 𝑞
∈ Q) → (((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) →
((*Q‘z)
<Q (*Q‘y) ∧
(*Q‘y)
<Q (*Q‘z)))) |
22 | 3, 21 | mtoi 589 |
. . . 4
⊢
((A ∈ P ∧ 𝑞
∈ Q) → ¬ ((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
23 | 22 | alrimivv 1752 |
. . 3
⊢
((A ∈ P ∧ 𝑞
∈ Q) → ∀y∀z ¬
((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
24 | | recexpr.1 |
. . . . . . . . 9
⊢ B = 〈{x
∣ ∃y(x
<Q y ∧ (*Q‘y) ∈
(2nd ‘A))}, {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))}〉 |
25 | 24 | recexprlemell 6594 |
. . . . . . . 8
⊢ (𝑞 ∈ (1st ‘B) ↔ ∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A))) |
26 | 24 | recexprlemelu 6595 |
. . . . . . . 8
⊢ (𝑞 ∈ (2nd ‘B) ↔ ∃y(y <Q 𝑞 ∧
(*Q‘y) ∈ (1st ‘A))) |
27 | 25, 26 | anbi12i 433 |
. . . . . . 7
⊢ ((𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ↔ (∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ ∃y(y <Q 𝑞 ∧
(*Q‘y) ∈ (1st ‘A)))) |
28 | | breq1 3758 |
. . . . . . . . . 10
⊢ (y = z →
(y <Q 𝑞 ↔ z <Q 𝑞)) |
29 | | fveq2 5121 |
. . . . . . . . . . 11
⊢ (y = z →
(*Q‘y) =
(*Q‘z)) |
30 | 29 | eleq1d 2103 |
. . . . . . . . . 10
⊢ (y = z →
((*Q‘y)
∈ (1st ‘A) ↔
(*Q‘z) ∈ (1st ‘A))) |
31 | 28, 30 | anbi12d 442 |
. . . . . . . . 9
⊢ (y = z →
((y <Q 𝑞 ∧
(*Q‘y) ∈ (1st ‘A)) ↔ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
32 | 31 | cbvexv 1792 |
. . . . . . . 8
⊢ (∃y(y <Q 𝑞 ∧
(*Q‘y) ∈ (1st ‘A)) ↔ ∃z(z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) |
33 | 32 | anbi2i 430 |
. . . . . . 7
⊢ ((∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ ∃y(y <Q 𝑞 ∧
(*Q‘y) ∈ (1st ‘A))) ↔ (∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ ∃z(z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
34 | 27, 33 | bitri 173 |
. . . . . 6
⊢ ((𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ↔ (∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ ∃z(z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
35 | | eeanv 1804 |
. . . . . 6
⊢ (∃y∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) ↔ (∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ ∃z(z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
36 | 34, 35 | bitr4i 176 |
. . . . 5
⊢ ((𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ↔ ∃y∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
37 | 36 | notbii 593 |
. . . 4
⊢ (¬
(𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ↔ ¬ ∃y∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
38 | | alnex 1385 |
. . . . . 6
⊢ (∀z ¬
((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) ↔ ¬ ∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
39 | 38 | albii 1356 |
. . . . 5
⊢ (∀y∀z ¬
((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) ↔ ∀y ¬
∃z((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
40 | | alnex 1385 |
. . . . 5
⊢ (∀y ¬
∃z((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) ↔ ¬ ∃y∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
41 | 39, 40 | bitri 173 |
. . . 4
⊢ (∀y∀z ¬
((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A))) ↔ ¬ ∃y∃z((𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) ∧ (z <Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
42 | 37, 41 | bitr4i 176 |
. . 3
⊢ (¬
(𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B)) ↔ ∀y∀z ¬
((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) ∧ (z
<Q 𝑞 ∧
(*Q‘z) ∈ (1st ‘A)))) |
43 | 23, 42 | sylibr 137 |
. 2
⊢
((A ∈ P ∧ 𝑞
∈ Q) → ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B))) |
44 | 43 | ralrimiva 2386 |
1
⊢ (A ∈
P → ∀𝑞 ∈
Q ¬ (𝑞 ∈ (1st ‘B) ∧ 𝑞 ∈ (2nd ‘B))) |