MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infxpenlem Structured version   Visualization version   GIF version

Theorem infxpenlem 9949
Description: Lemma for infxpen 9950. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
leweon.1 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st𝑥) ∈ (1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) ∈ (2nd𝑦))))}
r0weon.1 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))}
infxpen.1 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
infxpen.2 (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)))
infxpen.3 𝑀 = ((1st𝑤) ∪ (2nd𝑤))
infxpen.4 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
Assertion
Ref Expression
infxpenlem ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Distinct variable groups:   𝐴,𝑎   𝑤,𝐽   𝑧,𝑤,𝐿   𝑧,𝑚,𝑀   𝜑,𝑤,𝑧   𝑧,𝑄   𝑚,𝑎,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑚,𝑎)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑚)   𝑄(𝑥,𝑦,𝑤,𝑚,𝑎)   𝑅(𝑥,𝑦,𝑧,𝑤,𝑚,𝑎)   𝐽(𝑥,𝑦,𝑧,𝑚,𝑎)   𝐿(𝑥,𝑦,𝑚,𝑎)   𝑀(𝑥,𝑦,𝑤,𝑎)

Proof of Theorem infxpenlem
StepHypRef Expression
1 sseq2 3970 . . . 4 (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2 xpeq12 5658 . . . . . 6 ((𝑎 = 𝑚𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
32anidms 567 . . . . 5 (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4 id 22 . . . . 5 (𝑎 = 𝑚𝑎 = 𝑚)
53, 4breq12d 5118 . . . 4 (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
61, 5imbi12d 344 . . 3 (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7 sseq2 3970 . . . 4 (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8 xpeq12 5658 . . . . . 6 ((𝑎 = 𝐴𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
98anidms 567 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10 id 22 . . . . 5 (𝑎 = 𝐴𝑎 = 𝐴)
119, 10breq12d 5118 . . . 4 (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
127, 11imbi12d 344 . . 3 (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13 infxpen.2 . . . . . . . 8 (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)))
14 vex 3449 . . . . . . . . . . . . 13 𝑎 ∈ V
1514, 14xpex 7687 . . . . . . . . . . . 12 (𝑎 × 𝑎) ∈ V
16 simpll 765 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ∈ On)
1713, 16sylbi 216 . . . . . . . . . . . . . . . . 17 (𝜑𝑎 ∈ On)
18 onss 7719 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ On → 𝑎 ⊆ On)
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑎 ⊆ On)
20 xpss12 5648 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
2119, 19, 20syl2anc 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𝑤)) ∧ 𝑧𝐿𝑤)))}
2422, 23r0weon 9948 . . . . . . . . . . . . . . . 16 (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
2524simpli 484 . . . . . . . . . . . . . . 15 𝑅 We (On × On)
26 wess 5620 . . . . . . . . . . . . . . 15 ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
2721, 25, 26mpisyl 21 . . . . . . . . . . . . . 14 (𝜑𝑅 We (𝑎 × 𝑎))
28 weinxp 5716 . . . . . . . . . . . . . 14 (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
2927, 28sylib 217 . . . . . . . . . . . . 13 (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30 infxpen.1 . . . . . . . . . . . . . 14 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31 weeq1 5621 . . . . . . . . . . . . . 14 (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
3329, 32sylibr 233 . . . . . . . . . . . 12 (𝜑𝑄 We (𝑎 × 𝑎))
34 infxpen.4 . . . . . . . . . . . . 13 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
3534oiiso 9473 . . . . . . . . . . . 12 (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
3615, 33, 35sylancr 587 . . . . . . . . . . 11 (𝜑𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37 isof1o 7268 . . . . . . . . . . 11 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎))
38 f1ocnv 6796 . . . . . . . . . . 11 (𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎) → 𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39 f1of1 6783 . . . . . . . . . . 11 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
4036, 37, 38, 394syl 19 . . . . . . . . . 10 (𝜑𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41 f1f1orn 6795 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽)
4215f1oen 8913 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽 → (𝑎 × 𝑎) ≈ ran 𝐽)
4340, 41, 423syl 18 . . . . . . . . 9 (𝜑 → (𝑎 × 𝑎) ≈ ran 𝐽)
44 f1ofn 6785 . . . . . . . . . . 11 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽 Fn (𝑎 × 𝑎))
4536, 37, 38, 444syl 19 . . . . . . . . . 10 (𝜑𝐽 Fn (𝑎 × 𝑎))
4636adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
4737, 38, 393syl 18 . . . . . . . . . . . . . . . . . 18 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
48 cnvimass 6033 . . . . . . . . . . . . . . . . . . 19 (𝑄 “ {𝑤}) ⊆ dom 𝑄
49 inss2 4189 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
5030, 49eqsstri 3978 . . . . . . . . . . . . . . . . . . . . 21 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51 dmss 5858 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53 dmxpid 5885 . . . . . . . . . . . . . . . . . . . 20 dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
5452, 53sseqtri 3980 . . . . . . . . . . . . . . . . . . 19 dom 𝑄 ⊆ (𝑎 × 𝑎)
5548, 54sstri 3953 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56 f1ores 6798 . . . . . . . . . . . . . . . . . 18 ((𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5747, 55, 56sylancl 586 . . . . . . . . . . . . . . . . 17 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5815, 15xpex 7687 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
5958inex2 5275 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
6030, 59eqeltri 2834 . . . . . . . . . . . . . . . . . . . 20 𝑄 ∈ V
6160cnvex 7862 . . . . . . . . . . . . . . . . . . 19 𝑄 ∈ V
6261imaex 7853 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ∈ V
6362f1oen 8913 . . . . . . . . . . . . . . . . 17 ((𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
6446, 57, 633syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
65 sseqin2 4175 . . . . . . . . . . . . . . . . . . 19 ((𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤}))
6655, 65mpbi 229 . . . . . . . . . . . . . . . . . 18 ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤})
6766imaeq2i 6011 . . . . . . . . . . . . . . . . 17 (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽 “ (𝑄 “ {𝑤}))
68 isocnv 7275 . . . . . . . . . . . . . . . . . . . 20 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
6946, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71 isoini 7283 . . . . . . . . . . . . . . . . . . 19 ((𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
7269, 70, 71syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
73 fvex 6855 . . . . . . . . . . . . . . . . . . . . 21 (𝐽𝑤) ∈ V
7473epini 6048 . . . . . . . . . . . . . . . . . . . 20 ( E “ {(𝐽𝑤)}) = (𝐽𝑤)
7574ineq2i 4169 . . . . . . . . . . . . . . . . . . 19 (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (dom 𝐽 ∩ (𝐽𝑤))
7634oicl 9465 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐽
77 f1of 6784 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7836, 37, 38, 774syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7978ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ dom 𝐽)
80 ordelss 6333 . . . . . . . . . . . . . . . . . . . . 21 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ⊆ dom 𝐽)
8176, 79, 80sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ⊆ dom 𝐽)
82 sseqin2 4175 . . . . . . . . . . . . . . . . . . . 20 ((𝐽𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8381, 82sylib 217 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8475, 83eqtrid 2788 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (𝐽𝑤))
8572, 84eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽𝑤))
8667, 85eqtr3id 2790 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ (𝑄 “ {𝑤})) = (𝐽𝑤))
8764, 86breqtrd 5131 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽𝑤))
8887ensymd 8945 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≈ (𝑄 “ {𝑤}))
89 infxpen.3 . . . . . . . . . . . . . . . . . . 19 𝑀 = ((1st𝑤) ∪ (2nd𝑤))
90 fvex 6855 . . . . . . . . . . . . . . . . . . . 20 (1st𝑤) ∈ V
91 fvex 6855 . . . . . . . . . . . . . . . . . . . 20 (2nd𝑤) ∈ V
9290, 91unex 7680 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∪ (2nd𝑤)) ∈ V
9389, 92eqeltri 2834 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
9493sucex 7741 . . . . . . . . . . . . . . . . 17 suc 𝑀 ∈ V
9594, 94xpex 7687 . . . . . . . . . . . . . . . 16 (suc 𝑀 × suc 𝑀) ∈ V
96 xpss 5649 . . . . . . . . . . . . . . . . . . . 20 (𝑎 × 𝑎) ⊆ (V × V)
97 simp3 1138 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑄 “ {𝑤}))
98 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
9998eliniseg 6046 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ V → (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
10099elv 3451 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
10197, 100sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
10230breqi 5111 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑄𝑤𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
103 brin 5157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
104102, 103bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105104simprbi 497 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
106 brxp 5681 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
107106simplbi 498 . . . . . . . . . . . . . . . . . . . . 21 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤𝑧 ∈ (𝑎 × 𝑎))
108101, 105, 1073syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
10996, 108sselid 3942 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
11017adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
1111103adant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑎 ∈ On)
112 xp1st 7953 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (1st𝑧) ∈ 𝑎)
113 onelon 6342 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (1st𝑧) ∈ 𝑎) → (1st𝑧) ∈ On)
114112, 113sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st𝑧) ∈ On)
115111, 108, 114syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ On)
116 eloni 6327 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ On → Ord 𝑎)
117 elxp7 7956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎)))
118117simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎))
119 ordunel 7762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑎 ∧ (1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
1201193expib 1122 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑎 → (((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
121116, 118, 120syl2im 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
122110, 70, 121sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
12389, 122eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑀𝑎)
124 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 𝑚𝑎)
12513, 124sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑎 𝑚𝑎)
126 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
12713, 126sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ω ⊆ 𝑎)
128 iscard 9911 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎))
129 cardlim 9908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
130 sseq2 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
131 limeq 6329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
132130, 131bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
133129, 132mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
134128, 133sylbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135134biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
13617, 125, 127, 135syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → Lim 𝑎)
137136adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
138 limsuc 7785 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑎 → (𝑀𝑎 ↔ suc 𝑀𝑎))
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑀𝑎 ↔ suc 𝑀𝑎))
140123, 139mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
141 onelon 6342 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ suc 𝑀𝑎) → suc 𝑀 ∈ On)
14217, 140, 141syl2an2r 683 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
1431423adant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
144 ssun1 4132 . . . . . . . . . . . . . . . . . . . . 21 (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
145144a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
146104simplbi 498 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧𝑅𝑤)
147 df-br 5106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
14823eleq2i 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))})
149 opabidw 5481 . . . . . . . . . . . . . . . . . . . . . . . . . 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𝑤)) ∧ 𝑧𝐿𝑤))))
150147, 148, 1493bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤))))
151150simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧𝑅𝑤 → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))
152 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤) → ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)))
153152orim2i 909 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)) → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
154151, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑅𝑤 → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
155 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1st𝑧) ∈ V
156 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd𝑧) ∈ V
157155, 156unex 7680 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∪ (2nd𝑧)) ∈ V
158157elsuc 6387 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∪ (2nd𝑧)) ∈ suc ((1st𝑤) ∪ (2nd𝑤)) ↔ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
159154, 158sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑅𝑤 → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc ((1st𝑤) ∪ (2nd𝑤)))
160 suceq 6383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 = ((1st𝑤) ∪ (2nd𝑤)) → suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤)))
16189, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤))
162159, 161eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑅𝑤 → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
163101, 146, 1623syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
164 ontr2 6364 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀) → (1st𝑧) ∈ suc 𝑀))
165164imp 407 . . . . . . . . . . . . . . . . . . . 20 ((((1st𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)) → (1st𝑧) ∈ suc 𝑀)
166115, 143, 145, 163, 165syl22anc 837 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ suc 𝑀)
167 xp2nd 7954 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (2nd𝑧) ∈ 𝑎)
168 onelon 6342 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (2nd𝑧) ∈ 𝑎) → (2nd𝑧) ∈ On)
169167, 168sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd𝑧) ∈ On)
170111, 108, 169syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ On)
171 ssun2 4133 . . . . . . . . . . . . . . . . . . . . 21 (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
172171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
173 ontr2 6364 . . . . . . . . . . . . . . . . . . . . 21 (((2nd𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀) → (2nd𝑧) ∈ suc 𝑀))
174173imp 407 . . . . . . . . . . . . . . . . . . . 20 ((((2nd𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)) → (2nd𝑧) ∈ suc 𝑀)
175170, 143, 172, 163, 174syl22anc 837 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ suc 𝑀)
176 elxp7 7956 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)))
177176biimpri 227 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
178109, 166, 175, 177syl12anc 835 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
1791783expia 1121 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
180179ssrdv 3950 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
181 ssdomg 8940 . . . . . . . . . . . . . . . 16 ((suc 𝑀 × suc 𝑀) ∈ V → ((𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
18295, 180, 181mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
183127adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
184 nnfi 9111 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
185 xpfi 9261 . . . . . . . . . . . . . . . . . . . . . 22 ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
186185anidms 567 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
187 isfinite 9588 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
188186, 187sylib 217 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
189184, 188syl 17 . . . . . . . . . . . . . . . . . . 19 (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
190 ssdomg 8940 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
191190elv 3451 . . . . . . . . . . . . . . . . . . 19 (ω ⊆ 𝑎 → ω ≼ 𝑎)
192 sdomdomtr 9054 . . . . . . . . . . . . . . . . . . 19 (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
193189, 191, 192syl2an 596 . . . . . . . . . . . . . . . . . 18 ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194193expcom 414 . . . . . . . . . . . . . . . . 17 (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
195183, 194syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196 breq1 5108 . . . . . . . . . . . . . . . . . 18 (𝑚 = suc 𝑀 → (𝑚𝑎 ↔ suc 𝑀𝑎))
197125adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚𝑎 𝑚𝑎)
198196, 197, 140rspcdva 3582 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
199 omelon 9582 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
200 ontri1 6351 . . . . . . . . . . . . . . . . . . 19 ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
201199, 142, 200sylancr 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
202 sseq2 3970 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
203 xpeq12 5658 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = suc 𝑀𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
204203anidms 567 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
205 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀𝑚 = suc 𝑀)
206204, 205breq12d 5118 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
207202, 206imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
208 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
20913, 208sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
210209adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
211207, 210, 140rspcdva 3582 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212201, 211sylbird 259 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
213 ensdomtr 9057 . . . . . . . . . . . . . . . . . 18 (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
214213expcom 414 . . . . . . . . . . . . . . . . 17 (suc 𝑀𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
215198, 212, 214sylsyld 61 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
216195, 215pm2.61d 179 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
217 domsdomtr 9056 . . . . . . . . . . . . . . 15 (((𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (𝑄 “ {𝑤}) ≺ 𝑎)
218182, 216, 217syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≺ 𝑎)
219 ensdomtr 9057 . . . . . . . . . . . . . 14 (((𝐽𝑤) ≈ (𝑄 “ {𝑤}) ∧ (𝑄 “ {𝑤}) ≺ 𝑎) → (𝐽𝑤) ≺ 𝑎)
22088, 218, 219syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≺ 𝑎)
221 ordelon 6341 . . . . . . . . . . . . . . 15 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ∈ On)
22276, 79, 221sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ On)
223 onenon 9885 . . . . . . . . . . . . . . 15 (𝑎 ∈ On → 𝑎 ∈ dom card)
224110, 223syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
225 cardsdomel 9910 . . . . . . . . . . . . . 14 (((𝐽𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
226222, 224, 225syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
227220, 226mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ (card‘𝑎))
228 eleq2 2826 . . . . . . . . . . . . . 14 ((card‘𝑎) = 𝑎 → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
229128, 228sylbir 234 . . . . . . . . . . . . 13 ((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
23017, 197, 229syl2an2r 683 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
231227, 230mpbid 231 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ 𝑎)
232231ralrimiva 3143 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎)
233 fnfvrnss 7068 . . . . . . . . . . 11 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
234 ssdomg 8940 . . . . . . . . . . 11 (𝑎 ∈ V → (ran 𝐽𝑎 → ran 𝐽𝑎))
23514, 233, 234mpsyl 68 . . . . . . . . . 10 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
23645, 232, 235syl2anc 584 . . . . . . . . 9 (𝜑 → ran 𝐽𝑎)
237 endomtr 8952 . . . . . . . . 9 (((𝑎 × 𝑎) ≈ ran 𝐽 ∧ ran 𝐽𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
23843, 236, 237syl2anc 584 . . . . . . . 8 (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
23913, 238sylbir 234 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
240 df1o2 8419 . . . . . . . . . . . 12 1o = {∅}
241 1onn 8586 . . . . . . . . . . . 12 1o ∈ ω
242240, 241eqeltrri 2835 . . . . . . . . . . 11 {∅} ∈ ω
243 nnsdom 9590 . . . . . . . . . . 11 ({∅} ∈ ω → {∅} ≺ ω)
244 sdomdom 8920 . . . . . . . . . . 11 ({∅} ≺ ω → {∅} ≼ ω)
245242, 243, 244mp2b 10 . . . . . . . . . 10 {∅} ≼ ω
246 domtr 8947 . . . . . . . . . 10 (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
247245, 191, 246sylancr 587 . . . . . . . . 9 (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
248 0ex 5264 . . . . . . . . . . . 12 ∅ ∈ V
24914, 248xpsnen 8999 . . . . . . . . . . 11 (𝑎 × {∅}) ≈ 𝑎
250249ensymi 8944 . . . . . . . . . 10 𝑎 ≈ (𝑎 × {∅})
25114xpdom2 9011 . . . . . . . . . 10 ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
252 endomtr 8952 . . . . . . . . . 10 ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
253250, 251, 252sylancr 587 . . . . . . . . 9 ({∅} ≼ 𝑎𝑎 ≼ (𝑎 × 𝑎))
254247, 253syl 17 . . . . . . . 8 (ω ⊆ 𝑎𝑎 ≼ (𝑎 × 𝑎))
255254ad2antrl 726 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256 sbth 9037 . . . . . . 7 (((𝑎 × 𝑎) ≼ 𝑎𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
257239, 255, 256syl2anc 584 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
258257expr 457 . . . . 5 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚𝑎 𝑚𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
259 simplr 767 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
260 simpll 765 . . . . . . . . 9 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ∈ On)
261 simprr 771 . . . . . . . . 9 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ¬ ∀𝑚𝑎 𝑚𝑎)
262 rexnal 3103 . . . . . . . . . 10 (∃𝑚𝑎 ¬ 𝑚𝑎 ↔ ¬ ∀𝑚𝑎 𝑚𝑎)
263 onelss 6359 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
264 ssdomg 8940 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
265263, 264syld 47 . . . . . . . . . . . 12 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
266 bren2 8923 . . . . . . . . . . . . 13 (𝑚𝑎 ↔ (𝑚𝑎 ∧ ¬ 𝑚𝑎))
267266simplbi2 501 . . . . . . . . . . . 12 (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎))
268265, 267syl6 35 . . . . . . . . . . 11 (𝑎 ∈ On → (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎)))
269268reximdvai 3162 . . . . . . . . . 10 (𝑎 ∈ On → (∃𝑚𝑎 ¬ 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
270262, 269biimtrrid 242 . . . . . . . . 9 (𝑎 ∈ On → (¬ ∀𝑚𝑎 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
271260, 261, 270sylc 65 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 𝑚𝑎)
272 r19.29 3117 . . . . . . . 8 ((∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚𝑎 𝑚𝑎) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
273259, 271, 272syl2anc 584 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
274 simprl 769 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
275 onelon 6342 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ On ∧ 𝑚𝑎) → 𝑚 ∈ On)
276 ensym 8943 . . . . . . . . . . . . . . . . . 18 (𝑚𝑎𝑎𝑚)
277 domentr 8953 . . . . . . . . . . . . . . . . . 18 ((ω ≼ 𝑎𝑎𝑚) → ω ≼ 𝑚)
278191, 276, 277syl2an 596 . . . . . . . . . . . . . . . . 17 ((ω ⊆ 𝑎𝑚𝑎) → ω ≼ 𝑚)
279 domnsym 9043 . . . . . . . . . . . . . . . . . . 19 (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
280 nnsdom 9590 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ω → 𝑚 ≺ ω)
281279, 280nsyl 140 . . . . . . . . . . . . . . . . . 18 (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
282 ontri1 6351 . . . . . . . . . . . . . . . . . . 19 ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
283199, 282mpan 688 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
284281, 283syl5ibr 245 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
285275, 278, 284syl2im 40 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ On ∧ 𝑚𝑎) → ((ω ⊆ 𝑎𝑚𝑎) → ω ⊆ 𝑚))
286285expd 416 . . . . . . . . . . . . . . 15 ((𝑎 ∈ On ∧ 𝑚𝑎) → (ω ⊆ 𝑎 → (𝑚𝑎 → ω ⊆ 𝑚)))
287286impcom 408 . . . . . . . . . . . . . 14 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → (𝑚𝑎 → ω ⊆ 𝑚))
288287imim1d 82 . . . . . . . . . . . . 13 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
289288imp32 419 . . . . . . . . . . . 12 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
290 entr 8946 . . . . . . . . . . . . . . . 16 (((𝑚 × 𝑚) ≈ 𝑚𝑚𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
291290ancoms 459 . . . . . . . . . . . . . . 15 ((𝑚𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
292 xpen 9084 . . . . . . . . . . . . . . . . 17 ((𝑎𝑚𝑎𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
293292anidms 567 . . . . . . . . . . . . . . . 16 (𝑎𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
294 entr 8946 . . . . . . . . . . . . . . . 16 (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
295293, 294sylan 580 . . . . . . . . . . . . . . 15 ((𝑎𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
296276, 291, 295syl2an2r 683 . . . . . . . . . . . . . 14 ((𝑚𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
297296ex 413 . . . . . . . . . . . . 13 (𝑚𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
298297ad2antll 727 . . . . . . . . . . . 12 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
299289, 298mpd 15 . . . . . . . . . . 11 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
300299ex 413 . . . . . . . . . 10 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
301300expr 457 . . . . . . . . 9 ((ω ⊆ 𝑎𝑎 ∈ On) → (𝑚𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
302301rexlimdv 3150 . . . . . . . 8 ((ω ⊆ 𝑎𝑎 ∈ On) → (∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
303274, 260, 302syl2anc 584 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → (∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304273, 303mpd 15 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
305304expr 457 . . . . 5 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚𝑎 𝑚𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
306258, 305pm2.61d 179 . . . 4 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
307306exp31 420 . . 3 (𝑎 ∈ On → (∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
3086, 12, 307tfis3 7794 . 2 (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
309308imp 407 1 ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  cop 4592   class class class wbr 5105  {copab 5167   E cep 5536   Se wse 5586   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319   Fn wfn 6491  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496   Isom wiso 6497  ωcom 7802  1st c1st 7919  2nd c2nd 7920  1oc1o 8405  cen 8880  cdom 8881  csdm 8882  Fincfn 8883  OrdIsocoi 9445  cardccrd 9871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-card 9875
This theorem is referenced by:  infxpen  9950
  Copyright terms: Public domain W3C validator