Step | Hyp | Ref
| Expression |
1 | | ltsonq 6496 |
. . . . . 6
⊢
<Q Or Q |
2 | | ltrelnq 6463 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
3 | 1, 2 | son2lpi 4721 |
. . . . 5
⊢ ¬
((*Q‘𝑧) <Q
(*Q‘𝑦) ∧
(*Q‘𝑦) <Q
(*Q‘𝑧)) |
4 | | simprr 484 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
(*Q‘𝑧) ∈ (1st ‘𝐴)) |
5 | | simplr 482 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
(*Q‘𝑦) ∈ (2nd ‘𝐴)) |
6 | 4, 5 | jca 290 |
. . . . . . . . 9
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
((*Q‘𝑧) ∈ (1st ‘𝐴) ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))) |
7 | | prop 6573 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
8 | | prltlu 6585 |
. . . . . . . . . . 11
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧
(*Q‘𝑧) ∈ (1st ‘𝐴) ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) →
(*Q‘𝑧) <Q
(*Q‘𝑦)) |
9 | 7, 8 | syl3an1 1168 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑧) ∈ (1st ‘𝐴) ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) →
(*Q‘𝑧) <Q
(*Q‘𝑦)) |
10 | 9 | 3expb 1105 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
((*Q‘𝑧) ∈ (1st ‘𝐴) ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))) →
(*Q‘𝑧) <Q
(*Q‘𝑦)) |
11 | 6, 10 | sylan2 270 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) →
(*Q‘𝑧) <Q
(*Q‘𝑦)) |
12 | | simprl 483 |
. . . . . . . . . . 11
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) → 𝑧 <Q 𝑞) |
13 | | simpll 481 |
. . . . . . . . . . 11
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) → 𝑞 <Q 𝑦) |
14 | 1, 2 | sotri 4720 |
. . . . . . . . . . 11
⊢ ((𝑧 <Q
𝑞 ∧ 𝑞 <Q 𝑦) → 𝑧 <Q 𝑦) |
15 | 12, 13, 14 | syl2anc 391 |
. . . . . . . . . 10
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) → 𝑧 <Q 𝑦) |
16 | | ltrnqi 6519 |
. . . . . . . . . 10
⊢ (𝑧 <Q
𝑦 →
(*Q‘𝑦) <Q
(*Q‘𝑧)) |
17 | 15, 16 | syl 14 |
. . . . . . . . 9
⊢ (((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
(*Q‘𝑦) <Q
(*Q‘𝑧)) |
18 | 17 | adantl 262 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) →
(*Q‘𝑦) <Q
(*Q‘𝑧)) |
19 | 11, 18 | jca 290 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) →
((*Q‘𝑧) <Q
(*Q‘𝑦) ∧
(*Q‘𝑦) <Q
(*Q‘𝑧))) |
20 | 19 | ex 108 |
. . . . . 6
⊢ (𝐴 ∈ P →
(((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
((*Q‘𝑧) <Q
(*Q‘𝑦) ∧
(*Q‘𝑦) <Q
(*Q‘𝑧)))) |
21 | 20 | adantr 261 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑞 ∈ Q)
→ (((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) →
((*Q‘𝑧) <Q
(*Q‘𝑦) ∧
(*Q‘𝑦) <Q
(*Q‘𝑧)))) |
22 | 3, 21 | mtoi 590 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑞 ∈ Q)
→ ¬ ((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
23 | 22 | alrimivv 1755 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝑞 ∈ Q)
→ ∀𝑦∀𝑧 ¬ ((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
24 | | recexpr.1 |
. . . . . . . . 9
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))}〉 |
25 | 24 | recexprlemell 6720 |
. . . . . . . 8
⊢ (𝑞 ∈ (1st
‘𝐵) ↔
∃𝑦(𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))) |
26 | 24 | recexprlemelu 6721 |
. . . . . . . 8
⊢ (𝑞 ∈ (2nd
‘𝐵) ↔
∃𝑦(𝑦 <Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))) |
27 | 25, 26 | anbi12i 433 |
. . . . . . 7
⊢ ((𝑞 ∈ (1st
‘𝐵) ∧ 𝑞 ∈ (2nd
‘𝐵)) ↔
(∃𝑦(𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ ∃𝑦(𝑦 <Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)))) |
28 | | breq1 3767 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 <Q 𝑞 ↔ 𝑧 <Q 𝑞)) |
29 | | fveq2 5178 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 →
(*Q‘𝑦) = (*Q‘𝑧)) |
30 | 29 | eleq1d 2106 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 →
((*Q‘𝑦) ∈ (1st ‘𝐴) ↔
(*Q‘𝑧) ∈ (1st ‘𝐴))) |
31 | 28, 30 | anbi12d 442 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝑦 <Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) ↔ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
32 | 31 | cbvexv 1795 |
. . . . . . . 8
⊢
(∃𝑦(𝑦 <Q
𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) ↔ ∃𝑧(𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) |
33 | 32 | anbi2i 430 |
. . . . . . 7
⊢
((∃𝑦(𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ ∃𝑦(𝑦 <Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))) ↔ (∃𝑦(𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ ∃𝑧(𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
34 | 27, 33 | bitri 173 |
. . . . . 6
⊢ ((𝑞 ∈ (1st
‘𝐵) ∧ 𝑞 ∈ (2nd
‘𝐵)) ↔
(∃𝑦(𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ ∃𝑧(𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
35 | | eeanv 1807 |
. . . . . 6
⊢
(∃𝑦∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) ↔ (∃𝑦(𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ ∃𝑧(𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
36 | 34, 35 | bitr4i 176 |
. . . . 5
⊢ ((𝑞 ∈ (1st
‘𝐵) ∧ 𝑞 ∈ (2nd
‘𝐵)) ↔
∃𝑦∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
37 | 36 | notbii 594 |
. . . 4
⊢ (¬
(𝑞 ∈ (1st
‘𝐵) ∧ 𝑞 ∈ (2nd
‘𝐵)) ↔ ¬
∃𝑦∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
38 | | alnex 1388 |
. . . . . 6
⊢
(∀𝑧 ¬
((𝑞
<Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) ↔ ¬ ∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
39 | 38 | albii 1359 |
. . . . 5
⊢
(∀𝑦∀𝑧 ¬ ((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) ↔ ∀𝑦 ¬ ∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
40 | | alnex 1388 |
. . . . 5
⊢
(∀𝑦 ¬
∃𝑧((𝑞 <Q
𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) ↔ ¬ ∃𝑦∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
41 | 39, 40 | bitri 173 |
. . . 4
⊢
(∀𝑦∀𝑧 ¬ ((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴))) ↔ ¬ ∃𝑦∃𝑧((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
42 | 37, 41 | bitr4i 176 |
. . 3
⊢ (¬
(𝑞 ∈ (1st
‘𝐵) ∧ 𝑞 ∈ (2nd
‘𝐵)) ↔
∀𝑦∀𝑧 ¬ ((𝑞 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴)) ∧ (𝑧 <Q 𝑞 ∧
(*Q‘𝑧) ∈ (1st ‘𝐴)))) |
43 | 23, 42 | sylibr 137 |
. 2
⊢ ((𝐴 ∈ P ∧
𝑞 ∈ Q)
→ ¬ (𝑞 ∈
(1st ‘𝐵)
∧ 𝑞 ∈
(2nd ‘𝐵))) |
44 | 43 | ralrimiva 2392 |
1
⊢ (𝐴 ∈ P →
∀𝑞 ∈
Q ¬ (𝑞
∈ (1st ‘𝐵) ∧ 𝑞 ∈ (2nd ‘𝐵))) |