Proof of Theorem infxpenlem
Step | Hyp | Ref
| Expression |
1 | | sseq2 3768 |
. . . 4
⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚)) |
2 | | xpeq12 5291 |
. . . . . 6
⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
3 | 2 | anidms 680 |
. . . . 5
⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
4 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚) |
5 | 3, 4 | breq12d 4817 |
. . . 4
⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚)) |
6 | 1, 5 | imbi12d 333 |
. . 3
⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))) |
7 | | sseq2 3768 |
. . . 4
⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴)) |
8 | | xpeq12 5291 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
9 | 8 | anidms 680 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
10 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
11 | 9, 10 | breq12d 4817 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴)) |
12 | 7, 11 | imbi12d 333 |
. . 3
⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))) |
13 | | infxpen.2 |
. . . . . . . 8
⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) |
14 | | vex 3343 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
15 | 14, 14 | xpex 7128 |
. . . . . . . . . . . 12
⊢ (𝑎 × 𝑎) ∈ V |
16 | | simpll 807 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
17 | 13, 16 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑎 ∈ On) |
18 | | onss 7156 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ On → 𝑎 ⊆ On) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑎 ⊆ On) |
20 | | xpss12 5281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On)) |
21 | 19, 19, 20 | syl2anc 696 |
. . . . . . . . . . . . . . 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 9045 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |
25 | 24 | simpli 476 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 We (On ×
On) |
26 | | wess 5253 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎))) |
27 | 21, 25, 26 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎)) |
28 | | weinxp 5343 |
. . . . . . . . . . . . . 14
⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
29 | 27, 28 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
30 | | infxpen.1 |
. . . . . . . . . . . . . 14
⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
31 | | weeq1 5254 |
. . . . . . . . . . . . . 14
⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
33 | 29, 32 | sylibr 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎)) |
34 | | infxpen.4 |
. . . . . . . . . . . . 13
⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎)) |
35 | 34 | oiiso 8609 |
. . . . . . . . . . . 12
⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
36 | 15, 33, 35 | sylancr 698 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
37 | | isof1o 6737 |
. . . . . . . . . . 11
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎)) |
38 | | f1ocnv 6311 |
. . . . . . . . . . 11
⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽) |
39 | | f1of1 6298 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
41 | | f1f1orn 6310 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽) |
42 | 15 | f1oen 8144 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
44 | | f1ofn 6300 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽 Fn (𝑎 × 𝑎)) |
45 | 36, 37, 38, 44 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽 Fn (𝑎 × 𝑎)) |
46 | 36 | adantr 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
47 | 37, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
48 | | cnvimass 5643 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄 |
49 | | inss2 3977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
50 | 30, 49 | eqsstri 3776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
51 | | dmss 5478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
53 | | dmxpid 5500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎) |
54 | 52, 53 | sseqtri 3778 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑄 ⊆ (𝑎 × 𝑎) |
55 | 48, 54 | sstri 3753 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) |
56 | | f1ores 6313 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
57 | 47, 55, 56 | sylancl 697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
58 | 15, 15 | xpex 7128 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V |
59 | 58 | inex2 4952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V |
60 | 30, 59 | eqeltri 2835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑄 ∈ V |
61 | 60 | cnvex 7279 |
. . . . . . . . . . . . . . . . . . 19
⊢ ◡𝑄 ∈ V |
62 | 61 | imaex 7270 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ∈ V |
63 | 62 | f1oen 8144 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
64 | 46, 57, 63 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
65 | | sseqin2 3960 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})) |
66 | 55, 65 | mpbi 220 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}) |
67 | 66 | imaeq2i 5622 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤})) |
68 | | isocnv 6744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
69 | 46, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
70 | | simpr 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎)) |
71 | | isoini 6752 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
72 | 69, 70, 71 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
73 | | fvex 6363 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝐽‘𝑤) ∈ V |
74 | 73 | epini 5653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤) |
75 | 74 | ineq2i 3954 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤)) |
76 | 34 | oicl 8601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐽 |
77 | | f1of 6299 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
78 | 36, 37, 38, 77 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
79 | 78 | ffvelrnda 6523 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽) |
80 | | ordelss 5900 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
81 | 76, 79, 80 | sylancr 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
82 | | sseqin2 3960 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
83 | 81, 82 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
84 | 75, 83 | syl5eq 2806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤)) |
85 | 72, 84 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤)) |
86 | 67, 85 | syl5eqr 2808 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤)) |
87 | 64, 86 | breqtrd 4830 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤)) |
88 | 87 | ensymd 8174 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤})) |
89 | | infxpen.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) |
90 | | fvex 6363 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1st ‘𝑤) ∈ V |
91 | | fvex 6363 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑤) ∈ V |
92 | 90, 91 | unex 7122 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V |
93 | 89, 92 | eqeltri 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀 ∈ V |
94 | 93 | sucex 7177 |
. . . . . . . . . . . . . . . . 17
⊢ suc 𝑀 ∈ V |
95 | 94, 94 | xpex 7128 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑀 × suc 𝑀) ∈ V |
96 | | xpss 5282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 × 𝑎) ⊆ (V × V) |
97 | | simp3 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤})) |
98 | | vex 3343 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
99 | | vex 3343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑧 ∈ V |
100 | 99 | eliniseg 5652 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)) |
101 | 98, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤) |
102 | 97, 101 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤) |
103 | 30 | breqi 4810 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤) |
104 | | brin 4856 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
105 | 103, 104 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
106 | 105 | simprbi 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤) |
107 | | brxp 5304 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎))) |
108 | 107 | simplbi 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎)) |
109 | 102, 106,
108 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎)) |
110 | 96, 109 | sseldi 3742 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V)) |
111 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On) |
112 | 111 | 3adant3 1127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On) |
113 | | xp1st 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎) |
114 | | onelon 5909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (1st
‘𝑧) ∈ 𝑎) → (1st
‘𝑧) ∈
On) |
115 | 113, 114 | sylan2 492 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On) |
116 | 112, 109,
115 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On) |
117 | | eloni 5894 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ On → Ord 𝑎) |
118 | | elxp7 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎))) |
119 | 118 | simprbi 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)) |
120 | | ordunel 7193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝑎 ∧ (1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎) |
121 | 120 | 3expib 1117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝑎 → (((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎)) |
122 | 117, 119,
121 | syl2im 40 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎)) |
123 | 111, 70, 122 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎) |
124 | 89, 123 | syl5eqel 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎) |
125 | | simprr 813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
126 | 13, 125 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
127 | | simprl 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
128 | 13, 127 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ω ⊆ 𝑎) |
129 | | iscard 9011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) |
130 | | cardlim 9008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ω
⊆ (card‘𝑎)
↔ Lim (card‘𝑎)) |
131 | | sseq2 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
(card‘𝑎) ↔
ω ⊆ 𝑎)) |
132 | | limeq 5896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (Lim
(card‘𝑎) ↔ Lim
𝑎)) |
133 | 131, 132 | bibi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((card‘𝑎) =
𝑎 → ((ω ⊆
(card‘𝑎) ↔ Lim
(card‘𝑎)) ↔
(ω ⊆ 𝑎 ↔
Lim 𝑎))) |
134 | 130, 133 | mpbii 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
𝑎 ↔ Lim 𝑎)) |
135 | 129, 134 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎)) |
136 | 135 | biimpa 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎) |
137 | 17, 126, 128, 136 | syl21anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Lim 𝑎) |
138 | 137 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎) |
139 | | limsuc 7215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Lim
𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
141 | 124, 140 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎) |
142 | | onelon 5909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On) |
143 | 17, 141, 142 | syl2an2r 911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On) |
144 | 143 | 3adant3 1127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On) |
145 | | ssun1 3919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
147 | 105 | simplbi 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤) |
148 | | df-br 4805 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧𝑅𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑅) |
149 | 23 | eleq2i 2831 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑧, 𝑤〉 ∈ 𝑅 ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))}) |
150 | | opabid 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 286 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
152 | 151 | simprbi 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
153 | | simpl 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
154 | 153 | orim2i 541 |
. . . . . . . . . . . . . . . . . . . . . . . 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 6363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1st ‘𝑧) ∈ V |
157 | | fvex 6363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(2nd ‘𝑧) ∈ V |
158 | 156, 157 | unex 7122 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V |
159 | 158 | elsuc 5955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))
↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤)))) |
160 | 155, 159 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
161 | | suceq 5951 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) → suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))) |
162 | 89, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤)) |
163 | 160, 162 | syl6eleqr 2850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
164 | 102, 147,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
165 | | ontr2 5933 |
. . . . . . . . . . . . . . . . . . . . 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 1478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀) |
168 | | xp2nd 7367 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎) |
169 | | onelon 5909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (2nd
‘𝑧) ∈ 𝑎) → (2nd
‘𝑧) ∈
On) |
170 | 168, 169 | sylan2 492 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On) |
171 | 112, 109,
170 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On) |
172 | | ssun2 3920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
174 | | ontr2 5933 |
. . . . . . . . . . . . . . . . . . . . 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 1478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀) |
177 | | elxp7 7369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈ suc 𝑀 ∧ (2nd
‘𝑧) ∈ suc 𝑀))) |
178 | 177 | biimpri 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ suc 𝑀 ∧
(2nd ‘𝑧)
∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
179 | 110, 167,
176, 178 | syl12anc 1475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
180 | 179 | 3expia 1115 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))) |
181 | 180 | ssrdv 3750 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀)) |
182 | | ssdomg 8169 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))) |
183 | 95, 181, 182 | mpsyl 68 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)) |
184 | 128 | adantr 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎) |
185 | | nnfi 8320 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ ω → suc
𝑀 ∈
Fin) |
186 | | xpfi 8398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((suc
𝑀 ∈ Fin ∧ suc
𝑀 ∈ Fin) → (suc
𝑀 × suc 𝑀) ∈ Fin) |
187 | 186 | anidms 680 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ∈ Fin) |
188 | | isfinite 8724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((suc
𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω) |
189 | 187, 188 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ≺
ω) |
190 | 185, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑀 ∈ ω →
(suc 𝑀 × suc 𝑀) ≺
ω) |
191 | | ssdomg 8169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V → (ω
⊆ 𝑎 → ω
≼ 𝑎)) |
192 | 14, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
⊆ 𝑎 → ω
≼ 𝑎) |
193 | | sdomdomtr 8260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((suc
𝑀 × suc 𝑀) ≺ ω ∧ ω
≼ 𝑎) → (suc
𝑀 × suc 𝑀) ≺ 𝑎) |
194 | 190, 192,
193 | syl2an 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑀 ∈ ω ∧
ω ⊆ 𝑎) →
(suc 𝑀 × suc 𝑀) ≺ 𝑎) |
195 | 194 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (ω
⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc
𝑀 × suc 𝑀) ≺ 𝑎)) |
196 | 184, 195 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
197 | | breq1 4807 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎)) |
198 | 126 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
199 | 197, 198,
141 | rspcdva 3455 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎) |
200 | | omelon 8718 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
201 | | ontri1 5918 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ suc 𝑀
∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω)) |
202 | 200, 143,
201 | sylancr 698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈
ω)) |
203 | | sseq2 3768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀)) |
204 | | xpeq12 5291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
205 | 204 | anidms 680 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
206 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀) |
207 | 205, 206 | breq12d 4817 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
208 | 203, 207 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))) |
209 | | simplr 809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
210 | 13, 209 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
211 | 210 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
212 | 208, 211,
141 | rspcdva 3455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
213 | 202, 212 | sylbird 250 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
214 | | ensdomtr 8263 |
. . . . . . . . . . . . . . . . . 18
⊢ (((suc
𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
215 | 214 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
216 | 199, 213,
215 | sylsyld 61 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
217 | 196, 216 | pm2.61d 170 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
218 | | domsdomtr 8262 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
219 | 183, 217,
218 | syl2anc 696 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
220 | | ensdomtr 8263 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎) |
221 | 88, 219, 220 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎) |
222 | | ordelon 5908 |
. . . . . . . . . . . . . . 15
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On) |
223 | 76, 79, 222 | sylancr 698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On) |
224 | | onenon 8985 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → 𝑎 ∈ dom
card) |
225 | 111, 224 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card) |
226 | | cardsdomel 9010 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
227 | 223, 225,
226 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
228 | 221, 227 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎)) |
229 | | eleq2 2828 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑎) =
𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
230 | 129, 229 | sylbir 225 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
231 | 17, 198, 230 | syl2an2r 911 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
232 | 228, 231 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎) |
233 | 232 | ralrimiva 3104 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) |
234 | | fnfvrnss 6554 |
. . . . . . . . . . 11
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎) |
235 | | ssdomg 8169 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎)) |
236 | 14, 234, 235 | mpsyl 68 |
. . . . . . . . . 10
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎) |
237 | 45, 233, 236 | syl2anc 696 |
. . . . . . . . 9
⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎) |
238 | | endomtr 8181 |
. . . . . . . . 9
⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎) |
239 | 43, 237, 238 | syl2anc 696 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎) |
240 | 13, 239 | sylbir 225 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎) |
241 | | df1o2 7743 |
. . . . . . . . . . . 12
⊢
1𝑜 = {∅} |
242 | | 1onn 7890 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
243 | 241, 242 | eqeltrri 2836 |
. . . . . . . . . . 11
⊢ {∅}
∈ ω |
244 | | nnsdom 8726 |
. . . . . . . . . . 11
⊢
({∅} ∈ ω → {∅} ≺
ω) |
245 | | sdomdom 8151 |
. . . . . . . . . . 11
⊢
({∅} ≺ ω → {∅} ≼
ω) |
246 | 243, 244,
245 | mp2b 10 |
. . . . . . . . . 10
⊢ {∅}
≼ ω |
247 | | domtr 8176 |
. . . . . . . . . 10
⊢
(({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎) |
248 | 246, 192,
247 | sylancr 698 |
. . . . . . . . 9
⊢ (ω
⊆ 𝑎 → {∅}
≼ 𝑎) |
249 | | 0ex 4942 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
250 | 14, 249 | xpsnen 8211 |
. . . . . . . . . . 11
⊢ (𝑎 × {∅}) ≈
𝑎 |
251 | 250 | ensymi 8173 |
. . . . . . . . . 10
⊢ 𝑎 ≈ (𝑎 × {∅}) |
252 | 14 | xpdom2 8222 |
. . . . . . . . . 10
⊢
({∅} ≼ 𝑎
→ (𝑎 ×
{∅}) ≼ (𝑎
× 𝑎)) |
253 | | endomtr 8181 |
. . . . . . . . . 10
⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
254 | 251, 252,
253 | sylancr 698 |
. . . . . . . . 9
⊢
({∅} ≼ 𝑎
→ 𝑎 ≼ (𝑎 × 𝑎)) |
255 | 248, 254 | syl 17 |
. . . . . . . 8
⊢ (ω
⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎)) |
256 | 255 | ad2antrl 766 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
257 | | sbth 8247 |
. . . . . . 7
⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
258 | 240, 256,
257 | syl2anc 696 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
259 | 258 | expr 644 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
260 | | simplr 809 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
261 | | simpll 807 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
262 | | simprr 813 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
263 | | rexnal 3133 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈
𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
264 | | onelss 5927 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎)) |
265 | | ssdomg 8169 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎)) |
266 | 264, 265 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎)) |
267 | | bren2 8154 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎)) |
268 | 267 | simplbi2 656 |
. . . . . . . . . . . 12
⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)) |
269 | 266, 268 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))) |
270 | 269 | reximdvai 3153 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
271 | 263, 270 | syl5bir 233 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → (¬
∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
272 | 261, 262,
271 | sylc 65 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) |
273 | | r19.29 3210 |
. . . . . . . 8
⊢
((∀𝑚 ∈
𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
274 | 260, 272,
273 | syl2anc 696 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
275 | | simprl 811 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
276 | | onelon 5909 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On) |
277 | | ensym 8172 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚) |
278 | | domentr 8182 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚) |
279 | 192, 277,
278 | syl2an 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚) |
280 | | domnsym 8253 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
≼ 𝑚 → ¬
𝑚 ≺
ω) |
281 | | nnsdom 8726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ω → 𝑚 ≺
ω) |
282 | 280, 281 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
≼ 𝑚 → ¬
𝑚 ∈
ω) |
283 | | ontri1 5918 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ 𝑚 ∈
On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω)) |
284 | 200, 283 | mpan 708 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ On → (ω
⊆ 𝑚 ↔ ¬
𝑚 ∈
ω)) |
285 | 282, 284 | syl5ibr 236 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ On → (ω
≼ 𝑚 → ω
⊆ 𝑚)) |
286 | 276, 279,
285 | syl2im 40 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚)) |
287 | 286 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))) |
288 | 287 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)) |
289 | 288 | imim1d 82 |
. . . . . . . . . . . . 13
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚))) |
290 | 289 | imp32 448 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚) |
291 | | entr 8175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎) |
292 | 291 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎) |
293 | | xpen 8290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
294 | 293 | anidms 680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
295 | | entr 8175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
296 | 294, 295 | sylan 489 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
297 | 277, 292,
296 | syl2an2r 911 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎) |
298 | 297 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
299 | 298 | ad2antll 767 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
300 | 290, 299 | mpd 15 |
. . . . . . . . . . 11
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
301 | 300 | ex 449 |
. . . . . . . . . 10
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
302 | 301 | expr 644 |
. . . . . . . . 9
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))) |
303 | 302 | rexlimdv 3168 |
. . . . . . . 8
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
304 | 275, 261,
303 | syl2anc 696 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
305 | 274, 304 | mpd 15 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
306 | 305 | expr 644 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
307 | 259, 306 | pm2.61d 170 |
. . . 4
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
308 | 307 | exp31 631 |
. . 3
⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))) |
309 | 6, 12, 308 | tfis3 7223 |
. 2
⊢ (𝐴 ∈ On → (ω
⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)) |
310 | 309 | imp 444 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |