Proof of Theorem infxpenlem
Step | Hyp | Ref
| Expression |
1 | | sseq2 3590 |
. . . 4
⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚)) |
2 | | xpeq12 5058 |
. . . . . 6
⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
3 | 2 | anidms 675 |
. . . . 5
⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
4 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚) |
5 | 3, 4 | breq12d 4596 |
. . . 4
⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚)) |
6 | 1, 5 | imbi12d 333 |
. . 3
⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))) |
7 | | sseq2 3590 |
. . . 4
⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴)) |
8 | | xpeq12 5058 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
9 | 8 | anidms 675 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
10 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
11 | 9, 10 | breq12d 4596 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴)) |
12 | 7, 11 | imbi12d 333 |
. . 3
⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))) |
13 | | infxpen.2 |
. . . . . . . 8
⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) |
14 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
15 | 14, 14 | xpex 6860 |
. . . . . . . . . . . 12
⊢ (𝑎 × 𝑎) ∈ V |
16 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
17 | 13, 16 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑎 ∈ On) |
18 | | onss 6882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ On → 𝑎 ⊆ On) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑎 ⊆ On) |
20 | | xpss12 5148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On)) |
21 | 19, 19, 20 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎 × 𝑎) ⊆ (On × On)) |
22 | | leweon.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧
((1st ‘𝑥)
∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) ∈
(2nd ‘𝑦))))} |
23 | | r0weon.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))} |
24 | 22, 23 | r0weon 8718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |
25 | 24 | simpli 473 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 We (On ×
On) |
26 | | wess 5025 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎))) |
27 | 21, 25, 26 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎)) |
28 | | weinxp 5109 |
. . . . . . . . . . . . . 14
⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
29 | 27, 28 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
30 | | infxpen.1 |
. . . . . . . . . . . . . 14
⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
31 | | weeq1 5026 |
. . . . . . . . . . . . . 14
⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
33 | 29, 32 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎)) |
34 | | infxpen.4 |
. . . . . . . . . . . . 13
⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎)) |
35 | 34 | oiiso 8325 |
. . . . . . . . . . . 12
⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
36 | 15, 33, 35 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
37 | | isof1o 6473 |
. . . . . . . . . . 11
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎)) |
38 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽) |
39 | | f1of1 6049 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
41 | | f1f1orn 6061 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽) |
42 | 15 | f1oen 7862 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
44 | | f1ofn 6051 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽 Fn (𝑎 × 𝑎)) |
45 | 36, 37, 38, 44 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽 Fn (𝑎 × 𝑎)) |
46 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
47 | 37, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
48 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄 |
49 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
50 | 30, 49 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
51 | | dmss 5245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
53 | | dmxpid 5266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎) |
54 | 52, 53 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑄 ⊆ (𝑎 × 𝑎) |
55 | 48, 54 | sstri 3577 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) |
56 | | f1ores 6064 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
57 | 47, 55, 56 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
58 | 15, 15 | xpex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V |
59 | 58 | inex2 4728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V |
60 | 30, 59 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑄 ∈ V |
61 | 60 | cnvex 7006 |
. . . . . . . . . . . . . . . . . . 19
⊢ ◡𝑄 ∈ V |
62 | 61 | imaex 6996 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ∈ V |
63 | 62 | f1oen 7862 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
64 | 46, 57, 63 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
65 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})) |
66 | 55, 65 | mpbi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}) |
67 | 66 | imaeq2i 5383 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤})) |
68 | | isocnv 6480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
69 | 46, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
70 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎)) |
71 | | isoini 6488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
72 | 69, 70, 71 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
73 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝐽‘𝑤) ∈ V |
74 | 73 | epini 5414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤) |
75 | 74 | ineq2i 3773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤)) |
76 | 34 | oicl 8317 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐽 |
77 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
78 | 36, 37, 38, 77 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
79 | 78 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽) |
80 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
81 | 76, 79, 80 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
82 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
83 | 81, 82 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
84 | 75, 83 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤)) |
85 | 72, 84 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤)) |
86 | 67, 85 | syl5eqr 2658 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤)) |
87 | 64, 86 | breqtrd 4609 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤)) |
88 | 87 | ensymd 7893 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤})) |
89 | | infxpen.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) |
90 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1st ‘𝑤) ∈ V |
91 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑤) ∈ V |
92 | 90, 91 | unex 6854 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V |
93 | 89, 92 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀 ∈ V |
94 | 93 | sucex 6903 |
. . . . . . . . . . . . . . . . 17
⊢ suc 𝑀 ∈ V |
95 | 94, 94 | xpex 6860 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑀 × suc 𝑀) ∈ V |
96 | | xpss 5149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 × 𝑎) ⊆ (V × V) |
97 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤})) |
98 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
99 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑧 ∈ V |
100 | 99 | eliniseg 5413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)) |
101 | 98, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤) |
102 | 97, 101 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤) |
103 | 30 | breqi 4589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤) |
104 | | brin 4634 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
105 | 103, 104 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
106 | 105 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤) |
107 | | brxp 5071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎))) |
108 | 107 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎)) |
109 | 102, 106,
108 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎)) |
110 | 96, 109 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V)) |
111 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On) |
112 | 111 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On) |
113 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎) |
114 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (1st
‘𝑧) ∈ 𝑎) → (1st
‘𝑧) ∈
On) |
115 | 113, 114 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On) |
116 | 112, 109,
115 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On) |
117 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ On → Ord 𝑎) |
118 | | elxp7 7092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎))) |
119 | 118 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)) |
120 | | ordunel 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝑎 ∧ (1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎) |
121 | 120 | 3expib 1260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝑎 → (((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎)) |
122 | 117, 119,
121 | syl2im 39 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎)) |
123 | 111, 70, 122 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎) |
124 | 89, 123 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎) |
125 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
126 | 13, 125 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
127 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
128 | 13, 127 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ω ⊆ 𝑎) |
129 | | iscard 8684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) |
130 | | cardlim 8681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ω
⊆ (card‘𝑎)
↔ Lim (card‘𝑎)) |
131 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
(card‘𝑎) ↔
ω ⊆ 𝑎)) |
132 | | limeq 5652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (Lim
(card‘𝑎) ↔ Lim
𝑎)) |
133 | 131, 132 | bibi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((card‘𝑎) =
𝑎 → ((ω ⊆
(card‘𝑎) ↔ Lim
(card‘𝑎)) ↔
(ω ⊆ 𝑎 ↔
Lim 𝑎))) |
134 | 130, 133 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
𝑎 ↔ Lim 𝑎)) |
135 | 129, 134 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎)) |
136 | 135 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎) |
137 | 17, 126, 128, 136 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Lim 𝑎) |
138 | 137 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎) |
139 | | limsuc 6941 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Lim
𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
141 | 124, 140 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎) |
142 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On) |
143 | 17, 141, 142 | syl2an2r 872 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On) |
144 | 143 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On) |
145 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
147 | 105 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤) |
148 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧𝑅𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑅) |
149 | 23 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑧, 𝑤〉 ∈ 𝑅 ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))}) |
150 | | opabid 4907 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑧, 𝑤〉 ∈ {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))} ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
151 | 148, 149,
150 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
152 | 151 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
153 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
154 | 153 | orim2i 539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∧ 𝑧𝐿𝑤)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
155 | 152, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
156 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1st ‘𝑧) ∈ V |
157 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(2nd ‘𝑧) ∈ V |
158 | 156, 157 | unex 6854 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V |
159 | 158 | elsuc 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))
↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤)))) |
160 | 155, 159 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
161 | | suceq 5707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) → suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))) |
162 | 89, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤)) |
163 | 160, 162 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
164 | 102, 147,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
165 | | ontr2 5689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) → (1st
‘𝑧) ∈ suc 𝑀)) |
166 | 165 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀)) → (1st
‘𝑧) ∈ suc 𝑀) |
167 | 116, 144,
146, 164, 166 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀) |
168 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎) |
169 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (2nd
‘𝑧) ∈ 𝑎) → (2nd
‘𝑧) ∈
On) |
170 | 168, 169 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On) |
171 | 112, 109,
170 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On) |
172 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
174 | | ontr2 5689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) → (2nd
‘𝑧) ∈ suc 𝑀)) |
175 | 174 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀)) → (2nd
‘𝑧) ∈ suc 𝑀) |
176 | 171, 144,
173, 164, 175 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀) |
177 | | elxp7 7092 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈ suc 𝑀 ∧ (2nd
‘𝑧) ∈ suc 𝑀))) |
178 | 177 | biimpri 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ suc 𝑀 ∧
(2nd ‘𝑧)
∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
179 | 110, 167,
176, 178 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
180 | 179 | 3expia 1259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))) |
181 | 180 | ssrdv 3574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀)) |
182 | | ssdomg 7887 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))) |
183 | 95, 181, 182 | mpsyl 66 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)) |
184 | 128 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎) |
185 | | nnfi 8038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ ω → suc
𝑀 ∈
Fin) |
186 | | xpfi 8116 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((suc
𝑀 ∈ Fin ∧ suc
𝑀 ∈ Fin) → (suc
𝑀 × suc 𝑀) ∈ Fin) |
187 | 186 | anidms 675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ∈ Fin) |
188 | | isfinite 8432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((suc
𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω) |
189 | 187, 188 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ≺
ω) |
190 | 185, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑀 ∈ ω →
(suc 𝑀 × suc 𝑀) ≺
ω) |
191 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V → (ω
⊆ 𝑎 → ω
≼ 𝑎)) |
192 | 14, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
⊆ 𝑎 → ω
≼ 𝑎) |
193 | | sdomdomtr 7978 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((suc
𝑀 × suc 𝑀) ≺ ω ∧ ω
≼ 𝑎) → (suc
𝑀 × suc 𝑀) ≺ 𝑎) |
194 | 190, 192,
193 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑀 ∈ ω ∧
ω ⊆ 𝑎) →
(suc 𝑀 × suc 𝑀) ≺ 𝑎) |
195 | 194 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (ω
⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc
𝑀 × suc 𝑀) ≺ 𝑎)) |
196 | 184, 195 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
197 | 126 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
198 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎)) |
199 | 198 | rspccv 3279 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑚 ∈
𝑎 𝑚 ≺ 𝑎 → (suc 𝑀 ∈ 𝑎 → suc 𝑀 ≺ 𝑎)) |
200 | 197, 141,
199 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎) |
201 | | omelon 8426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
202 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ suc 𝑀
∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω)) |
203 | 201, 143,
202 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈
ω)) |
204 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
205 | 13, 204 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
206 | 205 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
207 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀)) |
208 | | xpeq12 5058 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
209 | 208 | anidms 675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
210 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀) |
211 | 209, 210 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
212 | 207, 211 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))) |
213 | 212 | rspccv 3279 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑚 ∈
𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (suc 𝑀 ∈ 𝑎 → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))) |
214 | 206, 141,
213 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
215 | 203, 214 | sylbird 249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
216 | | ensdomtr 7981 |
. . . . . . . . . . . . . . . . . 18
⊢ (((suc
𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
217 | 216 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
218 | 200, 215,
217 | sylsyld 59 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
219 | 196, 218 | pm2.61d 169 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
220 | | domsdomtr 7980 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
221 | 183, 219,
220 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
222 | | ensdomtr 7981 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎) |
223 | 88, 221, 222 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎) |
224 | | ordelon 5664 |
. . . . . . . . . . . . . . 15
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On) |
225 | 76, 79, 224 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On) |
226 | | onenon 8658 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → 𝑎 ∈ dom
card) |
227 | 111, 226 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card) |
228 | | cardsdomel 8683 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
229 | 225, 227,
228 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
230 | 223, 229 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎)) |
231 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑎) =
𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
232 | 129, 231 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
233 | 17, 197, 232 | syl2an2r 872 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
234 | 230, 233 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎) |
235 | 234 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) |
236 | | fnfvrnss 6297 |
. . . . . . . . . . 11
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎) |
237 | | ssdomg 7887 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎)) |
238 | 14, 236, 237 | mpsyl 66 |
. . . . . . . . . 10
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎) |
239 | 45, 235, 238 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎) |
240 | | endomtr 7900 |
. . . . . . . . 9
⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎) |
241 | 43, 239, 240 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎) |
242 | 13, 241 | sylbir 224 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎) |
243 | | df1o2 7459 |
. . . . . . . . . . . 12
⊢
1𝑜 = {∅} |
244 | | 1onn 7606 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
245 | 243, 244 | eqeltrri 2685 |
. . . . . . . . . . 11
⊢ {∅}
∈ ω |
246 | | nnsdom 8434 |
. . . . . . . . . . 11
⊢
({∅} ∈ ω → {∅} ≺
ω) |
247 | | sdomdom 7869 |
. . . . . . . . . . 11
⊢
({∅} ≺ ω → {∅} ≼
ω) |
248 | 245, 246,
247 | mp2b 10 |
. . . . . . . . . 10
⊢ {∅}
≼ ω |
249 | | domtr 7895 |
. . . . . . . . . 10
⊢
(({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎) |
250 | 248, 192,
249 | sylancr 694 |
. . . . . . . . 9
⊢ (ω
⊆ 𝑎 → {∅}
≼ 𝑎) |
251 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
252 | 14, 251 | xpsnen 7929 |
. . . . . . . . . . 11
⊢ (𝑎 × {∅}) ≈
𝑎 |
253 | 252 | ensymi 7892 |
. . . . . . . . . 10
⊢ 𝑎 ≈ (𝑎 × {∅}) |
254 | 14 | xpdom2 7940 |
. . . . . . . . . 10
⊢
({∅} ≼ 𝑎
→ (𝑎 ×
{∅}) ≼ (𝑎
× 𝑎)) |
255 | | endomtr 7900 |
. . . . . . . . . 10
⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
256 | 253, 254,
255 | sylancr 694 |
. . . . . . . . 9
⊢
({∅} ≼ 𝑎
→ 𝑎 ≼ (𝑎 × 𝑎)) |
257 | 250, 256 | syl 17 |
. . . . . . . 8
⊢ (ω
⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎)) |
258 | 257 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
259 | | sbth 7965 |
. . . . . . 7
⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
260 | 242, 258,
259 | syl2anc 691 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
261 | 260 | expr 641 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
262 | | simplr 788 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
263 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
264 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
265 | | rexnal 2978 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈
𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
266 | | onelss 5683 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎)) |
267 | | ssdomg 7887 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎)) |
268 | 266, 267 | syld 46 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎)) |
269 | | bren2 7872 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎)) |
270 | 269 | simplbi2 653 |
. . . . . . . . . . . 12
⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)) |
271 | 268, 270 | syl6 34 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))) |
272 | 271 | reximdvai 2998 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
273 | 265, 272 | syl5bir 232 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → (¬
∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
274 | 263, 264,
273 | sylc 63 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) |
275 | | r19.29 3054 |
. . . . . . . 8
⊢
((∀𝑚 ∈
𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
276 | 262, 274,
275 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
277 | | simprl 790 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
278 | | onelon 5665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On) |
279 | | ensym 7891 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚) |
280 | | domentr 7901 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚) |
281 | 192, 279,
280 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚) |
282 | | domnsym 7971 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
≼ 𝑚 → ¬
𝑚 ≺
ω) |
283 | | nnsdom 8434 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ω → 𝑚 ≺
ω) |
284 | 282, 283 | nsyl 134 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
≼ 𝑚 → ¬
𝑚 ∈
ω) |
285 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ 𝑚 ∈
On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω)) |
286 | 201, 285 | mpan 702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ On → (ω
⊆ 𝑚 ↔ ¬
𝑚 ∈
ω)) |
287 | 284, 286 | syl5ibr 235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ On → (ω
≼ 𝑚 → ω
⊆ 𝑚)) |
288 | 278, 281,
287 | syl2im 39 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚)) |
289 | 288 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))) |
290 | 289 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)) |
291 | 290 | imim1d 80 |
. . . . . . . . . . . . 13
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚))) |
292 | 291 | imp32 448 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚) |
293 | | entr 7894 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎) |
294 | 293 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎) |
295 | | xpen 8008 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
296 | 295 | anidms 675 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
297 | | entr 7894 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
298 | 296, 297 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
299 | 279, 294,
298 | syl2an2r 872 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎) |
300 | 299 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
301 | 300 | ad2antll 761 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
302 | 292, 301 | mpd 15 |
. . . . . . . . . . 11
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
303 | 302 | ex 449 |
. . . . . . . . . 10
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
304 | 303 | expr 641 |
. . . . . . . . 9
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))) |
305 | 304 | rexlimdv 3012 |
. . . . . . . 8
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
306 | 277, 263,
305 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
307 | 276, 306 | mpd 15 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
308 | 307 | expr 641 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
309 | 261, 308 | pm2.61d 169 |
. . . 4
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
310 | 309 | exp31 628 |
. . 3
⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))) |
311 | 6, 12, 310 | tfis3 6949 |
. 2
⊢ (𝐴 ∈ On → (ω
⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)) |
312 | 311 | imp 444 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |