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

Theorem infxpenlem 8821
Description: Lemma for infxpen 8822. (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 3619 . . . 4 (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2 xpeq12 5124 . . . . . 6 ((𝑎 = 𝑚𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
32anidms 676 . . . . 5 (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4 id 22 . . . . 5 (𝑎 = 𝑚𝑎 = 𝑚)
53, 4breq12d 4657 . . . 4 (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
61, 5imbi12d 334 . . 3 (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7 sseq2 3619 . . . 4 (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8 xpeq12 5124 . . . . . 6 ((𝑎 = 𝐴𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
98anidms 676 . . . . 5 (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10 id 22 . . . . 5 (𝑎 = 𝐴𝑎 = 𝐴)
119, 10breq12d 4657 . . . 4 (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
127, 11imbi12d 334 . . 3 (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13 infxpen.2 . . . . . . . 8 (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)))
14 vex 3198 . . . . . . . . . . . . 13 𝑎 ∈ V
1514, 14xpex 6947 . . . . . . . . . . . 12 (𝑎 × 𝑎) ∈ V
16 simpll 789 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ∈ On)
1713, 16sylbi 207 . . . . . . . . . . . . . . . . 17 (𝜑𝑎 ∈ On)
18 onss 6975 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ On → 𝑎 ⊆ On)
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑎 ⊆ On)
20 xpss12 5215 . . . . . . . . . . . . . . . 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 8820 . . . . . . . . . . . . . . . 16 (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
2524simpli 474 . . . . . . . . . . . . . . 15 𝑅 We (On × On)
26 wess 5091 . . . . . . . . . . . . . . 15 ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
2721, 25, 26mpisyl 21 . . . . . . . . . . . . . 14 (𝜑𝑅 We (𝑎 × 𝑎))
28 weinxp 5176 . . . . . . . . . . . . . 14 (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
2927, 28sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30 infxpen.1 . . . . . . . . . . . . . 14 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31 weeq1 5092 . . . . . . . . . . . . . 14 (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
3329, 32sylibr 224 . . . . . . . . . . . 12 (𝜑𝑄 We (𝑎 × 𝑎))
34 infxpen.4 . . . . . . . . . . . . 13 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
3534oiiso 8427 . . . . . . . . . . . 12 (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
3615, 33, 35sylancr 694 . . . . . . . . . . 11 (𝜑𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37 isof1o 6558 . . . . . . . . . . 11 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎))
38 f1ocnv 6136 . . . . . . . . . . 11 (𝐽:dom 𝐽1-1-onto→(𝑎 × 𝑎) → 𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39 f1of1 6123 . . . . . . . . . . 11 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
4036, 37, 38, 394syl 19 . . . . . . . . . 10 (𝜑𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41 f1f1orn 6135 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽)
4215f1oen 7961 . . . . . . . . . 10 (𝐽:(𝑎 × 𝑎)–1-1-onto→ran 𝐽 → (𝑎 × 𝑎) ≈ ran 𝐽)
4340, 41, 423syl 18 . . . . . . . . 9 (𝜑 → (𝑎 × 𝑎) ≈ ran 𝐽)
44 f1ofn 6125 . . . . . . . . . . 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 5473 . . . . . . . . . . . . . . . . . . 19 (𝑄 “ {𝑤}) ⊆ dom 𝑄
49 inss2 3826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
5030, 49eqsstri 3627 . . . . . . . . . . . . . . . . . . . . 21 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51 dmss 5312 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53 dmxpid 5334 . . . . . . . . . . . . . . . . . . . 20 dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
5452, 53sseqtri 3629 . . . . . . . . . . . . . . . . . . 19 dom 𝑄 ⊆ (𝑎 × 𝑎)
5548, 54sstri 3604 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56 f1ores 6138 . . . . . . . . . . . . . . . . . 18 ((𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5747, 55, 56sylancl 693 . . . . . . . . . . . . . . . . 17 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})))
5815, 15xpex 6947 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
5958inex2 4791 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
6030, 59eqeltri 2695 . . . . . . . . . . . . . . . . . . . 20 𝑄 ∈ V
6160cnvex 7098 . . . . . . . . . . . . . . . . . . 19 𝑄 ∈ V
6261imaex 7089 . . . . . . . . . . . . . . . . . 18 (𝑄 “ {𝑤}) ∈ V
6362f1oen 7961 . . . . . . . . . . . . . . . . 17 ((𝐽 ↾ (𝑄 “ {𝑤})):(𝑄 “ {𝑤})–1-1-onto→(𝐽 “ (𝑄 “ {𝑤})) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
6446, 57, 633syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽 “ (𝑄 “ {𝑤})))
65 sseqin2 3809 . . . . . . . . . . . . . . . . . . 19 ((𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤}))
6655, 65mpbi 220 . . . . . . . . . . . . . . . . . 18 ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤})) = (𝑄 “ {𝑤})
6766imaeq2i 5452 . . . . . . . . . . . . . . . . 17 (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽 “ (𝑄 “ {𝑤}))
68 isocnv 6565 . . . . . . . . . . . . . . . . . . . 20 (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
6946, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71 isoini 6573 . . . . . . . . . . . . . . . . . . 19 ((𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
7269, 70, 71syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})))
73 fvex 6188 . . . . . . . . . . . . . . . . . . . . 21 (𝐽𝑤) ∈ V
7473epini 5483 . . . . . . . . . . . . . . . . . . . 20 ( E “ {(𝐽𝑤)}) = (𝐽𝑤)
7574ineq2i 3803 . . . . . . . . . . . . . . . . . . 19 (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (dom 𝐽 ∩ (𝐽𝑤))
7634oicl 8419 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐽
77 f1of 6124 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7836, 37, 38, 774syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
7978ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ dom 𝐽)
80 ordelss 5727 . . . . . . . . . . . . . . . . . . . . 21 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ⊆ dom 𝐽)
8176, 79, 80sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ⊆ dom 𝐽)
82 sseqin2 3809 . . . . . . . . . . . . . . . . . . . 20 ((𝐽𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8381, 82sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (𝐽𝑤)) = (𝐽𝑤))
8475, 83syl5eq 2666 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ ( E “ {(𝐽𝑤)})) = (𝐽𝑤))
8572, 84eqtrd 2654 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ ((𝑎 × 𝑎) ∩ (𝑄 “ {𝑤}))) = (𝐽𝑤))
8667, 85syl5eqr 2668 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽 “ (𝑄 “ {𝑤})) = (𝐽𝑤))
8764, 86breqtrd 4670 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≈ (𝐽𝑤))
8887ensymd 7992 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≈ (𝑄 “ {𝑤}))
89 infxpen.3 . . . . . . . . . . . . . . . . . . 19 𝑀 = ((1st𝑤) ∪ (2nd𝑤))
90 fvex 6188 . . . . . . . . . . . . . . . . . . . 20 (1st𝑤) ∈ V
91 fvex 6188 . . . . . . . . . . . . . . . . . . . 20 (2nd𝑤) ∈ V
9290, 91unex 6941 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∪ (2nd𝑤)) ∈ V
9389, 92eqeltri 2695 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
9493sucex 6996 . . . . . . . . . . . . . . . . 17 suc 𝑀 ∈ V
9594, 94xpex 6947 . . . . . . . . . . . . . . . 16 (suc 𝑀 × suc 𝑀) ∈ V
96 xpss 5216 . . . . . . . . . . . . . . . . . . . 20 (𝑎 × 𝑎) ⊆ (V × V)
97 simp3 1061 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑄 “ {𝑤}))
98 vex 3198 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
99 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
10099eliniseg 5482 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ V → (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
10198, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
10297, 101sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
10330breqi 4650 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑄𝑤𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
104 brin 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105103, 104bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
106105simprbi 480 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
107 brxp 5137 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
108107simplbi 476 . . . . . . . . . . . . . . . . . . . . 21 (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤𝑧 ∈ (𝑎 × 𝑎))
109102, 106, 1083syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
11096, 109sseldi 3593 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
11117adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
1121113adant3 1079 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑎 ∈ On)
113 xp1st 7183 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (1st𝑧) ∈ 𝑎)
114 onelon 5736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (1st𝑧) ∈ 𝑎) → (1st𝑧) ∈ On)
115113, 114sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st𝑧) ∈ On)
116112, 109, 115syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ On)
117 eloni 5721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ On → Ord 𝑎)
118 elxp7 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎)))
119118simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎))
120 ordunel 7012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝑎 ∧ (1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
1211203expib 1266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑎 → (((1st𝑤) ∈ 𝑎 ∧ (2nd𝑤) ∈ 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
122117, 119, 121syl2im 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎))
123111, 70, 122sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((1st𝑤) ∪ (2nd𝑤)) ∈ 𝑎)
12489, 123syl5eqel 2703 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑀𝑎)
125 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ∀𝑚𝑎 𝑚𝑎)
12613, 125sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑎 𝑚𝑎)
127 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
12813, 127sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ω ⊆ 𝑎)
129 iscard 8786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎))
130 cardlim 8783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
131 sseq2 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
132 limeq 5723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1323 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → Lim 𝑎)
138137adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
139 limsuc 7034 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim 𝑎 → (𝑀𝑎 ↔ suc 𝑀𝑎))
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑀𝑎 ↔ suc 𝑀𝑎))
141124, 140mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
142 onelon 5736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ suc 𝑀𝑎) → suc 𝑀 ∈ On)
14317, 141, 142syl2an2r 875 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
1441433adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
145 ssun1 3768 . . . . . . . . . . . . . . . . . . . . 21 (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
146145a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
147105simplbi 476 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑤𝑧𝑅𝑤)
148 df-br 4645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
14923eleq2i 2691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st𝑧) ∪ (2nd𝑧)) ∈ ((1st𝑤) ∪ (2nd𝑤)) ∨ (((1st𝑧) ∪ (2nd𝑧)) = ((1st𝑤) ∪ (2nd𝑤)) ∧ 𝑧𝐿𝑤)))})
150 opabid 4972 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6188 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1st𝑧) ∈ V
157 fvex 6188 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd𝑧) ∈ V
158156, 157unex 6941 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∪ (2nd𝑧)) ∈ V
159158elsuc 5782 . . . . . . . . . . . . . . . . . . . . . . 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 5778 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 = ((1st𝑤) ∪ (2nd𝑤)) → suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤)))
16289, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑀 = suc ((1st𝑤) ∪ (2nd𝑤))
163160, 162syl6eleqr 2710 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑅𝑤 → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
164102, 147, 1633syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → ((1st𝑧) ∪ (2nd𝑧)) ∈ suc 𝑀)
165 ontr2 5760 . . . . . . . . . . . . . . . . . . . . 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 1325 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (1st𝑧) ∈ suc 𝑀)
168 xp2nd 7184 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑎 × 𝑎) → (2nd𝑧) ∈ 𝑎)
169 onelon 5736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ On ∧ (2nd𝑧) ∈ 𝑎) → (2nd𝑧) ∈ On)
170168, 169sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd𝑧) ∈ On)
171112, 109, 170syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ On)
172 ssun2 3769 . . . . . . . . . . . . . . . . . . . . 21 (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧))
173172a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ⊆ ((1st𝑧) ∪ (2nd𝑧)))
174 ontr2 5760 . . . . . . . . . . . . . . . . . . . . 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 1325 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → (2nd𝑧) ∈ suc 𝑀)
177 elxp7 7186 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)))
178177biimpri 218 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (V × V) ∧ ((1st𝑧) ∈ suc 𝑀 ∧ (2nd𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179110, 167, 176, 178syl12anc 1322 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
1801793expia 1265 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
181180ssrdv 3601 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
182 ssdomg 7986 . . . . . . . . . . . . . . . 16 ((suc 𝑀 × suc 𝑀) ∈ V → ((𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
18395, 181, 182mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
184128adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
185 nnfi 8138 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
186 xpfi 8216 . . . . . . . . . . . . . . . . . . . . . 22 ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
187186anidms 676 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
188 isfinite 8534 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
189187, 188sylib 208 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
190185, 189syl 17 . . . . . . . . . . . . . . . . . . 19 (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
191 ssdomg 7986 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
19214, 191ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (ω ⊆ 𝑎 → ω ≼ 𝑎)
193 sdomdomtr 8078 . . . . . . . . . . . . . . . . . . 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 4647 . . . . . . . . . . . . . . . . . . 19 (𝑚 = suc 𝑀 → (𝑚𝑎 ↔ suc 𝑀𝑎))
199198rspccv 3301 . . . . . . . . . . . . . . . . . 18 (∀𝑚𝑎 𝑚𝑎 → (suc 𝑀𝑎 → suc 𝑀𝑎))
200197, 141, 199sylc 65 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀𝑎)
201 omelon 8528 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
202 ontri1 5745 . . . . . . . . . . . . . . . . . . 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 3619 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
208 xpeq12 5124 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = suc 𝑀𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
209208anidms 676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
210 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = suc 𝑀𝑚 = suc 𝑀)
211209, 210breq12d 4657 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212207, 211imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
213212rspccv 3301 . . . . . . . . . . . . . . . . . . 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 8081 . . . . . . . . . . . . . . . . . 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 8080 . . . . . . . . . . . . . . 15 (((𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (𝑄 “ {𝑤}) ≺ 𝑎)
221183, 219, 220syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝑄 “ {𝑤}) ≺ 𝑎)
222 ensdomtr 8081 . . . . . . . . . . . . . 14 (((𝐽𝑤) ≈ (𝑄 “ {𝑤}) ∧ (𝑄 “ {𝑤}) ≺ 𝑎) → (𝐽𝑤) ≺ 𝑎)
22388, 221, 222syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ≺ 𝑎)
224 ordelon 5735 . . . . . . . . . . . . . . 15 ((Ord dom 𝐽 ∧ (𝐽𝑤) ∈ dom 𝐽) → (𝐽𝑤) ∈ On)
22576, 79, 224sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ On)
226 onenon 8760 . . . . . . . . . . . . . . 15 (𝑎 ∈ On → 𝑎 ∈ dom card)
227111, 226syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
228 cardsdomel 8785 . . . . . . . . . . . . . 14 (((𝐽𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
229225, 227, 228syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ≺ 𝑎 ↔ (𝐽𝑤) ∈ (card‘𝑎)))
230223, 229mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ (card‘𝑎))
231 eleq2 2688 . . . . . . . . . . . . . 14 ((card‘𝑎) = 𝑎 → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
232129, 231sylbir 225 . . . . . . . . . . . . 13 ((𝑎 ∈ On ∧ ∀𝑚𝑎 𝑚𝑎) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
23317, 197, 232syl2an2r 875 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → ((𝐽𝑤) ∈ (card‘𝑎) ↔ (𝐽𝑤) ∈ 𝑎))
234230, 233mpbid 222 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝑎 × 𝑎)) → (𝐽𝑤) ∈ 𝑎)
235234ralrimiva 2963 . . . . . . . . . 10 (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎)
236 fnfvrnss 6376 . . . . . . . . . . 11 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
237 ssdomg 7986 . . . . . . . . . . 11 (𝑎 ∈ V → (ran 𝐽𝑎 → ran 𝐽𝑎))
23814, 236, 237mpsyl 68 . . . . . . . . . 10 ((𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(𝐽𝑤) ∈ 𝑎) → ran 𝐽𝑎)
23945, 235, 238syl2anc 692 . . . . . . . . 9 (𝜑 → ran 𝐽𝑎)
240 endomtr 7999 . . . . . . . . 9 (((𝑎 × 𝑎) ≈ ran 𝐽 ∧ ran 𝐽𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
24143, 239, 240syl2anc 692 . . . . . . . 8 (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
24213, 241sylbir 225 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
243 df1o2 7557 . . . . . . . . . . . 12 1𝑜 = {∅}
244 1onn 7704 . . . . . . . . . . . 12 1𝑜 ∈ ω
245243, 244eqeltrri 2696 . . . . . . . . . . 11 {∅} ∈ ω
246 nnsdom 8536 . . . . . . . . . . 11 ({∅} ∈ ω → {∅} ≺ ω)
247 sdomdom 7968 . . . . . . . . . . 11 ({∅} ≺ ω → {∅} ≼ ω)
248245, 246, 247mp2b 10 . . . . . . . . . 10 {∅} ≼ ω
249 domtr 7994 . . . . . . . . . 10 (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
250248, 192, 249sylancr 694 . . . . . . . . 9 (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
251 0ex 4781 . . . . . . . . . . . 12 ∅ ∈ V
25214, 251xpsnen 8029 . . . . . . . . . . 11 (𝑎 × {∅}) ≈ 𝑎
253252ensymi 7991 . . . . . . . . . 10 𝑎 ≈ (𝑎 × {∅})
25414xpdom2 8040 . . . . . . . . . 10 ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
255 endomtr 7999 . . . . . . . . . 10 ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256253, 254, 255sylancr 694 . . . . . . . . 9 ({∅} ≼ 𝑎𝑎 ≼ (𝑎 × 𝑎))
257250, 256syl 17 . . . . . . . 8 (ω ⊆ 𝑎𝑎 ≼ (𝑎 × 𝑎))
258257ad2antrl 763 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚𝑎 𝑚𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
259 sbth 8065 . . . . . . 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 2992 . . . . . . . . . 10 (∃𝑚𝑎 ¬ 𝑚𝑎 ↔ ¬ ∀𝑚𝑎 𝑚𝑎)
266 onelss 5754 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
267 ssdomg 7986 . . . . . . . . . . . . 13 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
268266, 267syld 47 . . . . . . . . . . . 12 (𝑎 ∈ On → (𝑚𝑎𝑚𝑎))
269 bren2 7971 . . . . . . . . . . . . 13 (𝑚𝑎 ↔ (𝑚𝑎 ∧ ¬ 𝑚𝑎))
270269simplbi2 654 . . . . . . . . . . . 12 (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎))
271268, 270syl6 35 . . . . . . . . . . 11 (𝑎 ∈ On → (𝑚𝑎 → (¬ 𝑚𝑎𝑚𝑎)))
272271reximdvai 3012 . . . . . . . . . 10 (𝑎 ∈ On → (∃𝑚𝑎 ¬ 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
273265, 272syl5bir 233 . . . . . . . . 9 (𝑎 ∈ On → (¬ ∀𝑚𝑎 𝑚𝑎 → ∃𝑚𝑎 𝑚𝑎))
274263, 264, 273sylc 65 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 𝑚𝑎)
275 r19.29 3068 . . . . . . . 8 ((∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚𝑎 𝑚𝑎) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
276262, 274, 275syl2anc 692 . . . . . . 7 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ∃𝑚𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚𝑎))
277 simprl 793 . . . . . . . 8 (((𝑎 ∈ On ∧ ∀𝑚𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚𝑎 𝑚𝑎)) → ω ⊆ 𝑎)
278 onelon 5736 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ On ∧ 𝑚𝑎) → 𝑚 ∈ On)
279 ensym 7990 . . . . . . . . . . . . . . . . . 18 (𝑚𝑎𝑎𝑚)
280 domentr 8000 . . . . . . . . . . . . . . . . . 18 ((ω ≼ 𝑎𝑎𝑚) → ω ≼ 𝑚)
281192, 279, 280syl2an 494 . . . . . . . . . . . . . . . . 17 ((ω ⊆ 𝑎𝑚𝑎) → ω ≼ 𝑚)
282 domnsym 8071 . . . . . . . . . . . . . . . . . . 19 (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
283 nnsdom 8536 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ω → 𝑚 ≺ ω)
284282, 283nsyl 135 . . . . . . . . . . . . . . . . . 18 (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
285 ontri1 5745 . . . . . . . . . . . . . . . . . . 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 7993 . . . . . . . . . . . . . . . 16 (((𝑚 × 𝑚) ≈ 𝑚𝑚𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
294293ancoms 469 . . . . . . . . . . . . . . 15 ((𝑚𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
295 xpen 8108 . . . . . . . . . . . . . . . . 17 ((𝑎𝑚𝑎𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
296295anidms 676 . . . . . . . . . . . . . . . 16 (𝑎𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
297 entr 7993 . . . . . . . . . . . . . . . 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 3026 . . . . . . . 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 7042 . 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 1481  wcel 1988  wral 2909  wrex 2910  Vcvv 3195  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168  cop 4174   class class class wbr 4644  {copab 4703   E cep 5018   Se wse 5061   We wwe 5062   × cxp 5102  ccnv 5103  dom cdm 5104  ran crn 5105  cres 5106  cima 5107  Ord word 5710  Oncon0 5711  Lim wlim 5712  suc csuc 5713   Fn wfn 5871  wf 5872  1-1wf1 5873  1-1-ontowf1o 5875  cfv 5876   Isom wiso 5877  ωcom 7050  1st c1st 7151  2nd c2nd 7152  1𝑜c1o 7538  cen 7937  cdom 7938  csdm 7939  Fincfn 7940  OrdIsocoi 8399  cardccrd 8746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-oi 8400  df-card 8750
This theorem is referenced by:  infxpen  8822
  Copyright terms: Public domain W3C validator