Proof of Theorem infxpenlem
| Step | Hyp | Ref
| Expression |
| 1 | | sseq2 4010 |
. . . 4
⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚)) |
| 2 | | xpeq12 5710 |
. . . . . 6
⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
| 3 | 2 | anidms 566 |
. . . . 5
⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚)) |
| 4 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚) |
| 5 | 3, 4 | breq12d 5156 |
. . . 4
⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚)) |
| 6 | 1, 5 | imbi12d 344 |
. . 3
⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))) |
| 7 | | sseq2 4010 |
. . . 4
⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴)) |
| 8 | | xpeq12 5710 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
| 9 | 8 | anidms 566 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴)) |
| 10 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
| 11 | 9, 10 | breq12d 5156 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴)) |
| 12 | 7, 11 | imbi12d 344 |
. . 3
⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))) |
| 13 | | infxpen.2 |
. . . . . . . 8
⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) |
| 14 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
| 15 | 14, 14 | xpex 7773 |
. . . . . . . . . . . 12
⊢ (𝑎 × 𝑎) ∈ V |
| 16 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
| 17 | 13, 16 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑎 ∈ On) |
| 18 | | onss 7805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ On → 𝑎 ⊆ On) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑎 ⊆ On) |
| 20 | | xpss12 5700 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On)) |
| 21 | 19, 19, 20 | syl2anc 584 |
. . . . . . . . . . . . . . 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 10052 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On ×
On)) |
| 25 | 24 | simpli 483 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 We (On ×
On) |
| 26 | | wess 5671 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎))) |
| 27 | 21, 25, 26 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎)) |
| 28 | | weinxp 5770 |
. . . . . . . . . . . . . 14
⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
| 30 | | infxpen.1 |
. . . . . . . . . . . . . 14
⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
| 31 | | weeq1 5672 |
. . . . . . . . . . . . . 14
⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))) |
| 32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)) |
| 33 | 29, 32 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎)) |
| 34 | | infxpen.4 |
. . . . . . . . . . . . 13
⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎)) |
| 35 | 34 | oiiso 9577 |
. . . . . . . . . . . 12
⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
| 36 | 15, 33, 35 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎))) |
| 37 | | isof1o 7343 |
. . . . . . . . . . 11
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎)) |
| 38 | | f1ocnv 6860 |
. . . . . . . . . . 11
⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽) |
| 39 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
| 40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽) |
| 41 | | f1f1orn 6859 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽) |
| 42 | 15 | f1oen 9013 |
. . . . . . . . . 10
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran
◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
| 43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽) |
| 44 | | f1ofn 6849 |
. . . . . . . . . . 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 6100 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄 |
| 49 | | inss2 4238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
| 50 | 30, 49 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
| 51 | | dmss 5913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))) |
| 52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) |
| 53 | | dmxpid 5941 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎) |
| 54 | 52, 53 | sseqtri 4032 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑄 ⊆ (𝑎 × 𝑎) |
| 55 | 48, 54 | sstri 3993 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) |
| 56 | | f1ores 6862 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
| 57 | 47, 55, 56 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤}))) |
| 58 | 15, 15 | xpex 7773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V |
| 59 | 58 | inex2 5318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V |
| 60 | 30, 59 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑄 ∈ V |
| 61 | 60 | cnvex 7947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ◡𝑄 ∈ V |
| 62 | 61 | imaex 7936 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑄 “ {𝑤}) ∈ V |
| 63 | 62 | f1oen 9013 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
| 64 | 46, 57, 63 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤}))) |
| 65 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})) |
| 66 | 55, 65 | mpbi 230 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}) |
| 67 | 66 | imaeq2i 6076 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤})) |
| 68 | | isocnv 7350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
| 69 | 46, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽)) |
| 70 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎)) |
| 71 | | isoini 7358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
| 72 | 69, 70, 71 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)}))) |
| 73 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝐽‘𝑤) ∈ V |
| 74 | 73 | epini 6114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤) |
| 75 | 74 | ineq2i 4217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤)) |
| 76 | 34 | oicl 9569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐽 |
| 77 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom
𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
| 78 | 36, 37, 38, 77 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽) |
| 79 | 78 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽) |
| 80 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
| 81 | 76, 79, 80 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽) |
| 82 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
| 83 | 81, 82 | sylib 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤)) |
| 84 | 75, 83 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤)) |
| 85 | 72, 84 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤)) |
| 86 | 67, 85 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤)) |
| 87 | 64, 86 | breqtrd 5169 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤)) |
| 88 | 87 | ensymd 9045 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤})) |
| 89 | | infxpen.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) |
| 90 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1st ‘𝑤) ∈ V |
| 91 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑤) ∈ V |
| 92 | 90, 91 | unex 7764 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V |
| 93 | 89, 92 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀 ∈ V |
| 94 | 93 | sucex 7826 |
. . . . . . . . . . . . . . . . 17
⊢ suc 𝑀 ∈ V |
| 95 | 94, 94 | xpex 7773 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑀 × suc 𝑀) ∈ V |
| 96 | | xpss 5701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 × 𝑎) ⊆ (V × V) |
| 97 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤})) |
| 98 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑧 ∈ V |
| 99 | 98 | eliniseg 6112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)) |
| 100 | 99 | elv 3485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤) |
| 101 | 97, 100 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤) |
| 102 | 30 | breqi 5149 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤) |
| 103 | | brin 5195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
| 104 | 102, 103 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)) |
| 105 | 104 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤) |
| 106 | | brxp 5734 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎))) |
| 107 | 106 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎)) |
| 108 | 101, 105,
107 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎)) |
| 109 | 96, 108 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V)) |
| 110 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On) |
| 111 | 110 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On) |
| 112 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎) |
| 113 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (1st
‘𝑧) ∈ 𝑎) → (1st
‘𝑧) ∈
On) |
| 114 | 112, 113 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On) |
| 115 | 111, 108,
114 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On) |
| 116 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ On → Ord 𝑎) |
| 117 | | elxp7 8049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎))) |
| 118 | 117 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)) |
| 119 | | ordunel 7847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝑎 ∧ (1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎) |
| 120 | 119 | 3expib 1123 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝑎 → (((1st
‘𝑤) ∈ 𝑎 ∧ (2nd
‘𝑤) ∈ 𝑎) → ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∈ 𝑎)) |
| 121 | 116, 118,
120 | syl2im 40 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎)) |
| 122 | 110, 70, 121 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∈ 𝑎) |
| 123 | 89, 122 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎) |
| 124 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
| 125 | 13, 124 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
| 126 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
| 127 | 13, 126 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ω ⊆ 𝑎) |
| 128 | | iscard 10015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) |
| 129 | | cardlim 10012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ω
⊆ (card‘𝑎)
↔ Lim (card‘𝑎)) |
| 130 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
(card‘𝑎) ↔
ω ⊆ 𝑎)) |
| 131 | | limeq 6396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((card‘𝑎) =
𝑎 → (Lim
(card‘𝑎) ↔ Lim
𝑎)) |
| 132 | 130, 131 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((card‘𝑎) =
𝑎 → ((ω ⊆
(card‘𝑎) ↔ Lim
(card‘𝑎)) ↔
(ω ⊆ 𝑎 ↔
Lim 𝑎))) |
| 133 | 129, 132 | mpbii 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘𝑎) =
𝑎 → (ω ⊆
𝑎 ↔ Lim 𝑎)) |
| 134 | 128, 133 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎)) |
| 135 | 134 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎) |
| 136 | 17, 125, 127, 135 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Lim 𝑎) |
| 137 | 136 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎) |
| 138 | | limsuc 7870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Lim
𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
| 139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎)) |
| 140 | 123, 139 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎) |
| 141 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On) |
| 142 | 17, 140, 141 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On) |
| 143 | 142 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On) |
| 144 | | ssun1 4178 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
| 145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
| 146 | 104 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤) |
| 147 | | df-br 5144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧𝑅𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑅) |
| 148 | 23 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑧, 𝑤〉 ∈ 𝑅 ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))}) |
| 149 | | opabidw 5529 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
| 150 | 147, 148,
149 | 3bitri 297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∨
(((1st ‘𝑧)
∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) ∧ 𝑧𝐿𝑤)))) |
| 151 | 150 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))) |
| 152 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
| 153 | 152 | orim2i 911 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∧ 𝑧𝐿𝑤)) → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
| 154 | 151, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈
((1st ‘𝑤)
∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) =
((1st ‘𝑤)
∪ (2nd ‘𝑤)))) |
| 155 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1st ‘𝑧) ∈ V |
| 156 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(2nd ‘𝑧) ∈ V |
| 157 | 155, 156 | unex 7764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V |
| 158 | 157 | elsuc 6454 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))
↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st
‘𝑤) ∪
(2nd ‘𝑤))
∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st
‘𝑤) ∪
(2nd ‘𝑤)))) |
| 159 | 154, 158 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc
((1st ‘𝑤)
∪ (2nd ‘𝑤))) |
| 160 | | suceq 6450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd
‘𝑤)) → suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤))) |
| 161 | 89, 160 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑀 = suc ((1st
‘𝑤) ∪
(2nd ‘𝑤)) |
| 162 | 159, 161 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
| 163 | 101, 146,
162 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) |
| 164 | | ontr2 6431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) → (1st
‘𝑧) ∈ suc 𝑀)) |
| 165 | 164 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀)) → (1st
‘𝑧) ∈ suc 𝑀) |
| 166 | 115, 143,
145, 163, 165 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀) |
| 167 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎) |
| 168 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ (2nd
‘𝑧) ∈ 𝑎) → (2nd
‘𝑧) ∈
On) |
| 169 | 167, 168 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On) |
| 170 | 111, 108,
169 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On) |
| 171 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) |
| 172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st
‘𝑧) ∪
(2nd ‘𝑧))) |
| 173 | | ontr2 6431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀) → (2nd
‘𝑧) ∈ suc 𝑀)) |
| 174 | 173 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd
‘𝑧) ⊆
((1st ‘𝑧)
∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd
‘𝑧)) ∈ suc 𝑀)) → (2nd
‘𝑧) ∈ suc 𝑀) |
| 175 | 170, 143,
172, 163, 174 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀) |
| 176 | | elxp7 8049 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) ∈ suc 𝑀 ∧ (2nd
‘𝑧) ∈ suc 𝑀))) |
| 177 | 176 | biimpri 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
∈ suc 𝑀 ∧
(2nd ‘𝑧)
∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
| 178 | 109, 166,
175, 177 | syl12anc 837 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)) |
| 179 | 178 | 3expia 1122 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))) |
| 180 | 179 | ssrdv 3989 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀)) |
| 181 | | ssdomg 9040 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))) |
| 182 | 95, 180, 181 | mpsyl 68 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)) |
| 183 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎) |
| 184 | | nnfi 9207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ ω → suc
𝑀 ∈
Fin) |
| 185 | | xpfi 9358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((suc
𝑀 ∈ Fin ∧ suc
𝑀 ∈ Fin) → (suc
𝑀 × suc 𝑀) ∈ Fin) |
| 186 | 185 | anidms 566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ∈ Fin) |
| 187 | | isfinite 9692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((suc
𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω) |
| 188 | 186, 187 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑀 ∈ Fin → (suc
𝑀 × suc 𝑀) ≺
ω) |
| 189 | 184, 188 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑀 ∈ ω →
(suc 𝑀 × suc 𝑀) ≺
ω) |
| 190 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V → (ω
⊆ 𝑎 → ω
≼ 𝑎)) |
| 191 | 190 | elv 3485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
⊆ 𝑎 → ω
≼ 𝑎) |
| 192 | | sdomdomtr 9150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((suc
𝑀 × suc 𝑀) ≺ ω ∧ ω
≼ 𝑎) → (suc
𝑀 × suc 𝑀) ≺ 𝑎) |
| 193 | 189, 191,
192 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑀 ∈ ω ∧
ω ⊆ 𝑎) →
(suc 𝑀 × suc 𝑀) ≺ 𝑎) |
| 194 | 193 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ (ω
⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc
𝑀 × suc 𝑀) ≺ 𝑎)) |
| 195 | 183, 194 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
| 196 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎)) |
| 197 | 125 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
| 198 | 196, 197,
140 | rspcdva 3623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎) |
| 199 | | omelon 9686 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
| 200 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ suc 𝑀
∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω)) |
| 201 | 199, 142,
200 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈
ω)) |
| 202 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀)) |
| 203 | | xpeq12 5710 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
| 204 | 203 | anidms 566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀)) |
| 205 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀) |
| 206 | 204, 205 | breq12d 5156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
| 207 | 202, 206 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))) |
| 208 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
| 209 | 13, 208 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
| 210 | 209 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
| 211 | 207, 210,
140 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
| 212 | 201, 211 | sylbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)) |
| 213 | | ensdomtr 9153 |
. . . . . . . . . . . . . . . . . 18
⊢ (((suc
𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
| 214 | 213 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
| 215 | 198, 212,
214 | sylsyld 61 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎)) |
| 216 | 195, 215 | pm2.61d 179 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎) |
| 217 | | domsdomtr 9152 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
| 218 | 182, 216,
217 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎) |
| 219 | | ensdomtr 9153 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎) |
| 220 | 88, 218, 219 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎) |
| 221 | | ordelon 6408 |
. . . . . . . . . . . . . . 15
⊢ ((Ord dom
𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On) |
| 222 | 76, 79, 221 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On) |
| 223 | | onenon 9989 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → 𝑎 ∈ dom
card) |
| 224 | 110, 223 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card) |
| 225 | | cardsdomel 10014 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
| 226 | 222, 224,
225 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎))) |
| 227 | 220, 226 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎)) |
| 228 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑎) =
𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
| 229 | 128, 228 | sylbir 235 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
| 230 | 17, 197, 229 | syl2an2r 685 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎)) |
| 231 | 227, 230 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎) |
| 232 | 231 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) |
| 233 | | fnfvrnss 7141 |
. . . . . . . . . . 11
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎) |
| 234 | | ssdomg 9040 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎)) |
| 235 | 14, 233, 234 | mpsyl 68 |
. . . . . . . . . 10
⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎) |
| 236 | 45, 232, 235 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎) |
| 237 | | endomtr 9052 |
. . . . . . . . 9
⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎) |
| 238 | 43, 236, 237 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎) |
| 239 | 13, 238 | sylbir 235 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎) |
| 240 | | df1o2 8513 |
. . . . . . . . . . . 12
⊢
1o = {∅} |
| 241 | | 1onn 8678 |
. . . . . . . . . . . 12
⊢
1o ∈ ω |
| 242 | 240, 241 | eqeltrri 2838 |
. . . . . . . . . . 11
⊢ {∅}
∈ ω |
| 243 | | nnsdom 9694 |
. . . . . . . . . . 11
⊢
({∅} ∈ ω → {∅} ≺
ω) |
| 244 | | sdomdom 9020 |
. . . . . . . . . . 11
⊢
({∅} ≺ ω → {∅} ≼
ω) |
| 245 | 242, 243,
244 | mp2b 10 |
. . . . . . . . . 10
⊢ {∅}
≼ ω |
| 246 | | domtr 9047 |
. . . . . . . . . 10
⊢
(({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎) |
| 247 | 245, 191,
246 | sylancr 587 |
. . . . . . . . 9
⊢ (ω
⊆ 𝑎 → {∅}
≼ 𝑎) |
| 248 | | 0ex 5307 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
| 249 | 14, 248 | xpsnen 9095 |
. . . . . . . . . . 11
⊢ (𝑎 × {∅}) ≈
𝑎 |
| 250 | 249 | ensymi 9044 |
. . . . . . . . . 10
⊢ 𝑎 ≈ (𝑎 × {∅}) |
| 251 | 14 | xpdom2 9107 |
. . . . . . . . . 10
⊢
({∅} ≼ 𝑎
→ (𝑎 ×
{∅}) ≼ (𝑎
× 𝑎)) |
| 252 | | endomtr 9052 |
. . . . . . . . . 10
⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
| 253 | 250, 251,
252 | sylancr 587 |
. . . . . . . . 9
⊢
({∅} ≼ 𝑎
→ 𝑎 ≼ (𝑎 × 𝑎)) |
| 254 | 247, 253 | syl 17 |
. . . . . . . 8
⊢ (ω
⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎)) |
| 255 | 254 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎)) |
| 256 | | sbth 9133 |
. . . . . . 7
⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
| 257 | 239, 255,
256 | syl2anc 584 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
| 258 | 257 | expr 456 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
| 259 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) |
| 260 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On) |
| 261 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
| 262 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈
𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) |
| 263 | | onelss 6426 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎)) |
| 264 | | ssdomg 9040 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎)) |
| 265 | 263, 264 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎)) |
| 266 | | bren2 9023 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎)) |
| 267 | 266 | simplbi2 500 |
. . . . . . . . . . . 12
⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)) |
| 268 | 265, 267 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))) |
| 269 | 268 | reximdvai 3165 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
| 270 | 262, 269 | biimtrrid 243 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → (¬
∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)) |
| 271 | 260, 261,
270 | sylc 65 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) |
| 272 | | r19.29 3114 |
. . . . . . . 8
⊢
((∀𝑚 ∈
𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
| 273 | 259, 271,
272 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) |
| 274 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎) |
| 275 | | onelon 6409 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On) |
| 276 | | ensym 9043 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚) |
| 277 | | domentr 9053 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚) |
| 278 | 191, 276,
277 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚) |
| 279 | | domnsym 9139 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
≼ 𝑚 → ¬
𝑚 ≺
ω) |
| 280 | | nnsdom 9694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ω → 𝑚 ≺
ω) |
| 281 | 279, 280 | nsyl 140 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
≼ 𝑚 → ¬
𝑚 ∈
ω) |
| 282 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ω
∈ On ∧ 𝑚 ∈
On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω)) |
| 283 | 199, 282 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ On → (ω
⊆ 𝑚 ↔ ¬
𝑚 ∈
ω)) |
| 284 | 281, 283 | imbitrrid 246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ On → (ω
≼ 𝑚 → ω
⊆ 𝑚)) |
| 285 | 275, 278,
284 | syl2im 40 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚)) |
| 286 | 285 | expd 415 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))) |
| 287 | 286 | impcom 407 |
. . . . . . . . . . . . . 14
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)) |
| 288 | 287 | imim1d 82 |
. . . . . . . . . . . . 13
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚))) |
| 289 | 288 | imp32 418 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚) |
| 290 | | entr 9046 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎) |
| 291 | 290 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎) |
| 292 | | xpen 9180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
| 293 | 292 | anidms 566 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚)) |
| 294 | | entr 9046 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
| 295 | 293, 294 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
| 296 | 276, 291,
295 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎) |
| 297 | 296 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
| 298 | 297 | ad2antll 729 |
. . . . . . . . . . . 12
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎)) |
| 299 | 289, 298 | mpd 15 |
. . . . . . . . . . 11
⊢
(((ω ⊆ 𝑎
∧ (𝑎 ∈ On ∧
𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
| 300 | 299 | ex 412 |
. . . . . . . . . 10
⊢ ((ω
⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
| 301 | 300 | expr 456 |
. . . . . . . . 9
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))) |
| 302 | 301 | rexlimdv 3153 |
. . . . . . . 8
⊢ ((ω
⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
| 303 | 274, 260,
302 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)) |
| 304 | 273, 303 | mpd 15 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎) |
| 305 | 304 | expr 456 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)) |
| 306 | 258, 305 | pm2.61d 179 |
. . . 4
⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎) |
| 307 | 306 | exp31 419 |
. . 3
⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))) |
| 308 | 6, 12, 307 | tfis3 7879 |
. 2
⊢ (𝐴 ∈ On → (ω
⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)) |
| 309 | 308 | imp 406 |
1
⊢ ((𝐴 ∈ On ∧ ω ⊆
𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |