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

Theorem infxpenlem 8780
Description: Lemma for infxpen 8781. (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 3606 . . . 4 (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2 xpeq12 5094 . . . . . 6 ((𝑎 = 𝑚𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
32anidms 676 . . . . 5 (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4 id 22 . . . . 5 (𝑎 = 𝑚𝑎 = 𝑚)
53, 4breq12d 4626 . . . 4 (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
61, 5imbi12d 334 . . 3 (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7 sseq2 3606 . . . 4 (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8 xpeq12 5094 . . . . . 6 ((𝑎 = 𝐴𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
98anidms 676 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10 id 22 . . . . 5 (𝑎 = 𝐴𝑎 = 𝐴)
119, 10breq12d 4626 . . . 4 (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
127, 11imbi12d 334 . . 3 (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13 infxpen.2 . . . . . . . 8 (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)))
14 vex 3189 . . . . . . . . . . . . 13 𝑎 ∈ V
1514, 14xpex 6915 . . . . . . . . . . . 12 (𝑎 × 𝑎) ∈ V
16 simpll 789 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ∈ On)
1713, 16sylbi 207 . . . . . . . . . . . . . . . . 17 (𝜑𝑎 ∈ On)
18 onss 6937 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ On → 𝑎 ⊆ On)
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑎 ⊆ On)
20 xpss12 5186 . . . . . . . . . . . . . . . 16 ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
2119, 19, 20syl2anc 692 . . . . . . . . . . . . . . 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 8779 . . . . . . . . . . . . . . . 16 (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
2524simpli 474 . . . . . . . . . . . . . . 15 𝑅 We (On × On)
26 wess 5061 . . . . . . . . . . . . . . 15 ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
2721, 25, 26mpisyl 21 . . . . . . . . . . . . . 14 (𝜑𝑅 We (𝑎 × 𝑎))
28 weinxp 5147 . . . . . . . . . . . . . 14 (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
2927, 28sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30 infxpen.1 . . . . . . . . . . . . . 14 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31 weeq1 5062 . . . . . . . . . . . . . 14 (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
3329, 32sylibr 224 . . . . . . . . . . . 12 (𝜑𝑄 We (𝑎 × 𝑎))
34 infxpen.4 . . . . . . . . . . . . 13 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
3534oiiso 8386 . . . . . . . . . . . 12 (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
3615, 33, 35sylancr 694 . . . . . . . . . . 11 (𝜑𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37 isof1o 6527 . . . . . . . . . . 11 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎))
38 f1ocnv 6106 . . . . . . . . . . 11 (𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎) → 𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39 f1of1 6093 . . . . . . . . . . 11 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
4036, 37, 38, 394syl 19 . . . . . . . . . 10 (𝜑𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41 f1f1orn 6105 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽)
4215f1oen 7920 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽 → (𝑎 × 𝑎) ≈ ran 𝐽)
4340, 41, 423syl 18 . . . . . . . . 9 (𝜑 → (𝑎 × 𝑎) ≈ ran 𝐽)
44 f1ofn 6095 . . . . . . . . . . 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 5444 . . . . . . . . . . . . . . . . . . 19 (𝑄 “ {𝑤}) ⊆ dom 𝑄
49 inss2 3812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
5030, 49eqsstri 3614 . . . . . . . . . . . . . . . . . . . . 21 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51 dmss 5283 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53 dmxpid 5305 . . . . . . . . . . . . . . . . . . . 20 dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
5452, 53sseqtri 3616 . . . . . . . . . . . . . . . . . . 19 dom 𝑄 ⊆ (𝑎 × 𝑎)
5548, 54sstri 3592 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56 f1ores 6108 . . . . . . . . . . . . . . . . . 18 ((𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5747, 55, 56sylancl 693 . . . . . . . . . . . . . . . . 17 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5815, 15xpex 6915 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
5958inex2 4760 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
6030, 59eqeltri 2694 . . . . . . . . . . . . . . . . . . . 20 𝑄 ∈ V
6160cnvex 7060 . . . . . . . . . . . . . . . . . . 19 𝑄 ∈ V
6261imaex 7051 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ∈ V
6362f1oen 7920 . . . . . . . . . . . . . . . . 17 ((𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
6446, 57, 633syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
65 sseqin2 3795 . . . . . . . . . . . . . . . . . . 19 ((𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤}))
6655, 65mpbi 220 . . . . . . . . . . . . . . . . . 18 ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤})
6766imaeq2i 5423 . . . . . . . . . . . . . . . . 17 (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽 “ (𝑄 “ {𝑤}))
68 isocnv 6534 . . . . . . . . . . . . . . . . . . . 20 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
6946, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71 isoini 6542 . . . . . . . . . . . . . . . . . . 19 ((𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
7269, 70, 71syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
73 fvex 6158 . . . . . . . . . . . . . . . . . . . . 21 (𝐽𝑤) ∈ V
7473epini 5454 . . . . . . . . . . . . . . . . . . . 20 ( E “ {(𝐽𝑤)}) = (𝐽𝑤)
7574ineq2i 3789 . . . . . . . . . . . . . . . . . . 19 (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (dom 𝐽 ∩ (𝐽𝑤))
7634oicl 8378 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐽
77 f1of 6094 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7836, 37, 38, 774syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7978ffvelrnda 6315 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ dom 𝐽)
80 ordelss 5698 . . . . . . . . . . . . . . . . . . . . 21 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ⊆ dom 𝐽)
8176, 79, 80sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ⊆ dom 𝐽)
82 sseqin2 3795 . . . . . . . . . . . . . . . . . . . 20 ((𝐽𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8381, 82sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8475, 83syl5eq 2667 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (𝐽𝑤))
8572, 84eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽𝑤))
8667, 85syl5eqr 2669 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ (𝑄 “ {𝑤})) = (𝐽𝑤))
8764, 86breqtrd 4639 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽𝑤))
8887ensymd 7951 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≈ (𝑄 “ {𝑤}))
89 infxpen.3 . . . . . . . . . . . . . . . . . . 19 𝑀 = ((1st𝑤) ∪ (2nd𝑤))
90 fvex 6158 . . . . . . . . . . . . . . . . . . . 20 (1st𝑤) ∈ V
91 fvex 6158 . . . . . . . . . . . . . . . . . . . 20 (2nd𝑤) ∈ V
9290, 91unex 6909 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∪ (2nd𝑤)) ∈ V
9389, 92eqeltri 2694 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
9493sucex 6958 . . . . . . . . . . . . . . . . 17 suc 𝑀 ∈ V
9594, 94xpex 6915 . . . . . . . . . . . . . . . 16 (suc 𝑀 × suc 𝑀) ∈ V
96 xpss 5187 . . . . . . . . . . . . . . . . . . . 20 (𝑎 × 𝑎) ⊆ (V × V)
97 simp3 1061 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑄 “ {𝑤}))
98 vex 3189 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
99 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
10099eliniseg 5453 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ V → (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
10198, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
10297, 101sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
10330breqi 4619 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑄𝑤𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
104 brin 4664 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105103, 104bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
106105simprbi 480 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
107 brxp 5107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
108107simplbi 476 . . . . . . . . . . . . . . . . . . . . 21 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤𝑧 ∈ (𝑎 × 𝑎))
109102, 106, 1083syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
11096, 109sseldi 3581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
11117adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
1121113adant3 1079 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑎 ∈ On)
113 xp1st 7143 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (1st𝑧) ∈ 𝑎)
114 onelon 5707 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (1st𝑧) ∈ 𝑎) → (1st𝑧) ∈ On)
115113, 114sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st𝑧) ∈ On)
116112, 109, 115syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ On)
117 eloni 5692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ On → Ord 𝑎)
118 elxp7 7146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎)))
119118simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎))
120 ordunel 6974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑎 ∧ (1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
1211203expib 1265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑎 → (((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
122117, 119, 121syl2im 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
123111, 70, 122sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
12489, 123syl5eqel 2702 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑀𝑎)
125 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 𝑚𝑎)
12613, 125sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑎 𝑚𝑎)
127 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
12813, 127sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ω ⊆ 𝑎)
129 iscard 8745 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎))
130 cardlim 8742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
131 sseq2 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
132 limeq 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
133131, 132bibi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
134130, 133mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135129, 134sylbir 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
136135biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
13717, 126, 128, 136syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → Lim 𝑎)
138137adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
139 limsuc 6996 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑎 → (𝑀𝑎 ↔ suc 𝑀𝑎))
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑀𝑎 ↔ suc 𝑀𝑎))
141124, 140mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
142 onelon 5707 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ suc 𝑀𝑎) → suc 𝑀 ∈ On)
14317, 141, 142syl2an2r 875 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
1441433adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
145 ssun1 3754 . . . . . . . . . . . . . . . . . . . . 21 (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
146145a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
147105simplbi 476 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧𝑅𝑤)
148 df-br 4614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
14923eleq2i 2690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))})
150 opabid 4942 . . . . . . . . . . . . . . . . . . . . . . . . . 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𝑤)) ∧ 𝑧𝐿𝑤))))
151148, 149, 1503bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤))))
152151simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧𝑅𝑤 → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))
153 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤) → ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)))
154153orim2i 540 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)) → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
155152, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑅𝑤 → (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
156 fvex 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1st𝑧) ∈ V
157 fvex 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd𝑧) ∈ V
158156, 157unex 6909 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∪ (2nd𝑧)) ∈ V
159158elsuc 5753 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∪ (2nd𝑧)) ∈ suc ((1st𝑤) ∪ (2nd𝑤)) ↔ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ ((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤))))
160155, 159sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑅𝑤 → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc ((1st𝑤) ∪ (2nd𝑤)))
161 suceq 5749 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 = ((1st𝑤) ∪ (2nd𝑤)) → suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤)))
16289, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤))
163160, 162syl6eleqr 2709 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑅𝑤 → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
164102, 147, 1633syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
165 ontr2 5731 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀) → (1st𝑧) ∈ suc 𝑀))
166165imp 445 . . . . . . . . . . . . . . . . . . . 20 ((((1st𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)) → (1st𝑧) ∈ suc 𝑀)
167116, 144, 146, 164, 166syl22anc 1324 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ suc 𝑀)
168 xp2nd 7144 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (2nd𝑧) ∈ 𝑎)
169 onelon 5707 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (2nd𝑧) ∈ 𝑎) → (2nd𝑧) ∈ On)
170168, 169sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd𝑧) ∈ On)
171112, 109, 170syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ On)
172 ssun2 3755 . . . . . . . . . . . . . . . . . . . . 21 (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
173172a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
174 ontr2 5731 . . . . . . . . . . . . . . . . . . . . 21 (((2nd𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀) → (2nd𝑧) ∈ suc 𝑀))
175174imp 445 . . . . . . . . . . . . . . . . . . . 20 ((((2nd𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)) ∧ ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)) → (2nd𝑧) ∈ suc 𝑀)
176171, 144, 173, 164, 175syl22anc 1324 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ suc 𝑀)
177 elxp7 7146 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)))
178177biimpri 218 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179110, 167, 176, 178syl12anc 1321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
1801793expia 1264 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
181180ssrdv 3589 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
182 ssdomg 7945 . . . . . . . . . . . . . . . 16 ((suc 𝑀 × suc 𝑀) ∈ V → ((𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
18395, 181, 182mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
184128adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
185 nnfi 8097 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
186 xpfi 8175 . . . . . . . . . . . . . . . . . . . . . 22 ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
187186anidms 676 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
188 isfinite 8493 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
189187, 188sylib 208 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
190185, 189syl 17 . . . . . . . . . . . . . . . . . . 19 (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
191 ssdomg 7945 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
19214, 191ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (ω ⊆ 𝑎 → ω ≼ 𝑎)
193 sdomdomtr 8037 . . . . . . . . . . . . . . . . . . 19 (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194190, 192, 193syl2an 494 . . . . . . . . . . . . . . . . . 18 ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
195194expcom 451 . . . . . . . . . . . . . . . . 17 (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196184, 195syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
197126adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚𝑎 𝑚𝑎)
198 breq1 4616 . . . . . . . . . . . . . . . . . . 19 (𝑚 = suc 𝑀 → (𝑚𝑎 ↔ suc 𝑀𝑎))
199198rspccv 3292 . . . . . . . . . . . . . . . . . 18 (∀𝑚𝑎 𝑚𝑎 → (suc 𝑀𝑎 → suc 𝑀𝑎))
200197, 141, 199sylc 65 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
201 omelon 8487 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
202 ontri1 5716 . . . . . . . . . . . . . . . . . . 19 ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
203201, 143, 202sylancr 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
204 simplr 791 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
20513, 204sylbi 207 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
206205adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
207 sseq2 3606 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
208 xpeq12 5094 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = suc 𝑀𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
209208anidms 676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
210 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = suc 𝑀𝑚 = suc 𝑀)
211209, 210breq12d 4626 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212207, 211imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
213212rspccv 3292 . . . . . . . . . . . . . . . . . . 19 (∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (suc 𝑀𝑎 → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
214206, 141, 213sylc 65 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
215203, 214sylbird 250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
216 ensdomtr 8040 . . . . . . . . . . . . . . . . . 18 (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
217216expcom 451 . . . . . . . . . . . . . . . . 17 (suc 𝑀𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
218200, 215, 217sylsyld 61 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
219196, 218pm2.61d 170 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
220 domsdomtr 8039 . . . . . . . . . . . . . . 15 (((𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (𝑄 “ {𝑤}) ≺ 𝑎)
221183, 219, 220syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≺ 𝑎)
222 ensdomtr 8040 . . . . . . . . . . . . . 14 (((𝐽𝑤) ≈ (𝑄 “ {𝑤}) ∧ (𝑄 “ {𝑤}) ≺ 𝑎) → (𝐽𝑤) ≺ 𝑎)
22388, 221, 222syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≺ 𝑎)
224 ordelon 5706 . . . . . . . . . . . . . . 15 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ∈ On)
22576, 79, 224sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ On)
226 onenon 8719 . . . . . . . . . . . . . . 15 (𝑎 ∈ On → 𝑎 ∈ dom card)
227111, 226syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
228 cardsdomel 8744 . . . . . . . . . . . . . 14 (((𝐽𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
229225, 227, 228syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
230223, 229mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ (card‘𝑎))
231 eleq2 2687 . . . . . . . . . . . . . 14 ((card‘𝑎) = 𝑎 → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
232129, 231sylbir 225 . . . . . . . . . . . . 13 ((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
23317, 197, 232syl2an2r 875 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
234230, 233mpbid 222 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ 𝑎)
235234ralrimiva 2960 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎)
236 fnfvrnss 6345 . . . . . . . . . . 11 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
237 ssdomg 7945 . . . . . . . . . . 11 (𝑎 ∈ V → (ran 𝐽𝑎 → ran 𝐽𝑎))
23814, 236, 237mpsyl 68 . . . . . . . . . 10 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
23945, 235, 238syl2anc 692 . . . . . . . . 9 (𝜑 → ran 𝐽𝑎)
240 endomtr 7958 . . . . . . . . 9 (((𝑎 × 𝑎) ≈ ran 𝐽 ∧ ran 𝐽𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
24143, 239, 240syl2anc 692 . . . . . . . 8 (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
24213, 241sylbir 225 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
243 df1o2 7517 . . . . . . . . . . . 12 1𝑜 = {∅}
244 1onn 7664 . . . . . . . . . . . 12 1𝑜 ∈ ω
245243, 244eqeltrri 2695 . . . . . . . . . . 11 {∅} ∈ ω
246 nnsdom 8495 . . . . . . . . . . 11 ({∅} ∈ ω → {∅} ≺ ω)
247 sdomdom 7927 . . . . . . . . . . 11 ({∅} ≺ ω → {∅} ≼ ω)
248245, 246, 247mp2b 10 . . . . . . . . . 10 {∅} ≼ ω
249 domtr 7953 . . . . . . . . . 10 (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
250248, 192, 249sylancr 694 . . . . . . . . 9 (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
251 0ex 4750 . . . . . . . . . . . 12 ∅ ∈ V
25214, 251xpsnen 7988 . . . . . . . . . . 11 (𝑎 × {∅}) ≈ 𝑎
253252ensymi 7950 . . . . . . . . . 10 𝑎 ≈ (𝑎 × {∅})
25414xpdom2 7999 . . . . . . . . . 10 ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
255 endomtr 7958 . . . . . . . . . 10 ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256253, 254, 255sylancr 694 . . . . . . . . 9 ({∅} ≼ 𝑎𝑎 ≼ (𝑎 × 𝑎))
257250, 256syl 17 . . . . . . . 8 (ω ⊆ 𝑎𝑎 ≼ (𝑎 × 𝑎))
258257ad2antrl 763 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
259 sbth 8024 . . . . . . 7 (((𝑎 × 𝑎) ≼ 𝑎𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
260242, 258, 259syl2anc 692 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
261260expr 642 . . . . 5 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚𝑎 𝑚𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
262 simplr 791 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
263 simpll 789 . . . . . . . . 9 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ∈ On)
264 simprr 795 . . . . . . . . 9 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ¬ ∀𝑚𝑎 𝑚𝑎)
265 rexnal 2989 . . . . . . . . . 10 (∃𝑚𝑎 ¬ 𝑚𝑎 ↔ ¬ ∀𝑚𝑎 𝑚𝑎)
266 onelss 5725 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
267 ssdomg 7945 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
268266, 267syld 47 . . . . . . . . . . . 12 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
269 bren2 7930 . . . . . . . . . . . . 13 (𝑚𝑎 ↔ (𝑚𝑎 ∧ ¬ 𝑚𝑎))
270269simplbi2 654 . . . . . . . . . . . 12 (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎))
271268, 270syl6 35 . . . . . . . . . . 11 (𝑎 ∈ On → (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎)))
272271reximdvai 3009 . . . . . . . . . 10 (𝑎 ∈ On → (∃𝑚𝑎 ¬ 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
273265, 272syl5bir 233 . . . . . . . . 9 (𝑎 ∈ On → (¬ ∀𝑚𝑎 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
274263, 264, 273sylc 65 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 𝑚𝑎)
275 r19.29 3065 . . . . . . . 8 ((∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚𝑎 𝑚𝑎) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
276262, 274, 275syl2anc 692 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
277 simprl 793 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
278 onelon 5707 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ On ∧ 𝑚𝑎) → 𝑚 ∈ On)
279 ensym 7949 . . . . . . . . . . . . . . . . . 18 (𝑚𝑎𝑎𝑚)
280 domentr 7959 . . . . . . . . . . . . . . . . . 18 ((ω ≼ 𝑎𝑎𝑚) → ω ≼ 𝑚)
281192, 279, 280syl2an 494 . . . . . . . . . . . . . . . . 17 ((ω ⊆ 𝑎𝑚𝑎) → ω ≼ 𝑚)
282 domnsym 8030 . . . . . . . . . . . . . . . . . . 19 (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
283 nnsdom 8495 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ω → 𝑚 ≺ ω)
284282, 283nsyl 135 . . . . . . . . . . . . . . . . . 18 (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
285 ontri1 5716 . . . . . . . . . . . . . . . . . . 19 ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
286201, 285mpan 705 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
287284, 286syl5ibr 236 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
288278, 281, 287syl2im 40 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ On ∧ 𝑚𝑎) → ((ω ⊆ 𝑎𝑚𝑎) → ω ⊆ 𝑚))
289288expd 452 . . . . . . . . . . . . . . 15 ((𝑎 ∈ On ∧ 𝑚𝑎) → (ω ⊆ 𝑎 → (𝑚𝑎 → ω ⊆ 𝑚)))
290289impcom 446 . . . . . . . . . . . . . 14 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → (𝑚𝑎 → ω ⊆ 𝑚))
291290imim1d 82 . . . . . . . . . . . . 13 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
292291imp32 449 . . . . . . . . . . . 12 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
293 entr 7952 . . . . . . . . . . . . . . . 16 (((𝑚 × 𝑚) ≈ 𝑚𝑚𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
294293ancoms 469 . . . . . . . . . . . . . . 15 ((𝑚𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
295 xpen 8067 . . . . . . . . . . . . . . . . 17 ((𝑎𝑚𝑎𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
296295anidms 676 . . . . . . . . . . . . . . . 16 (𝑎𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
297 entr 7952 . . . . . . . . . . . . . . . 16 (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
298296, 297sylan 488 . . . . . . . . . . . . . . 15 ((𝑎𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
299279, 294, 298syl2an2r 875 . . . . . . . . . . . . . 14 ((𝑚𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
300299ex 450 . . . . . . . . . . . . 13 (𝑚𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
301300ad2antll 764 . . . . . . . . . . . 12 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
302292, 301mpd 15 . . . . . . . . . . 11 (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
303302ex 450 . . . . . . . . . 10 ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304303expr 642 . . . . . . . . 9 ((ω ⊆ 𝑎𝑎 ∈ On) → (𝑚𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
305304rexlimdv 3023 . . . . . . . 8 ((ω ⊆ 𝑎𝑎 ∈ On) → (∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
306277, 263, 305syl2anc 692 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → (∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
307276, 306mpd 15 . . . . . 6 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
308307expr 642 . . . . 5 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚𝑎 𝑚𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
309261, 308pm2.61d 170 . . . 4 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
310309exp31 629 . . 3 (𝑎 ∈ On → (∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
3116, 12, 310tfis3 7004 . 2 (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
312311imp 445 1 ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  cun 3553  cin 3554  wss 3555  c0 3891  {csn 4148  cop 4154   class class class wbr 4613  {copab 4672   E cep 4983   Se wse 5031   We wwe 5032   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Ord word 5681  Oncon0 5682  Lim wlim 5683  suc csuc 5684   Fn wfn 5842  wf 5843  1-1wf1 5844  1-1-ontowf1o 5846  cfv 5847   Isom wiso 5848  ωcom 7012  1st c1st 7111  2nd c2nd 7112  1𝑜c1o 7498  cen 7896  cdom 7897  csdm 7898  Fincfn 7899  OrdIsocoi 8358  cardccrd 8705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-oi 8359  df-card 8709
This theorem is referenced by:  infxpen  8781
  Copyright terms: Public domain W3C validator