Metamath Proof Explorer

Theorem infxpenlem

Description: Lemma for infxpen . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses 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 infxpenlem ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 leweon.1 ⊢ 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) }
2 r0weon.1 ⊢ 𝑅 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) }
3 infxpen.1 ⊢ 𝑄 = ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) )
4 infxpen.2 ⊢ ( 𝜑 ↔ ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) )
5 infxpen.3 ⊢ 𝑀 = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) )
6 infxpen.4 ⊢ 𝐽 = OrdIso ( 𝑄 , ( 𝑎 × 𝑎 ) )
7 sseq2 ⊢ ( 𝑎 = 𝑚 → ( ω ⊆ 𝑎 ↔ ω ⊆ 𝑚 ) )
8 xpeq12 ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑎 = 𝑚 ) → ( 𝑎 × 𝑎 ) = ( 𝑚 × 𝑚 ) )
9 8 anidms ⊢ ( 𝑎 = 𝑚 → ( 𝑎 × 𝑎 ) = ( 𝑚 × 𝑚 ) )
10 id ⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 )
11 9 10 breq12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑎 × 𝑎 ) ≈ 𝑎 ↔ ( 𝑚 × 𝑚 ) ≈ 𝑚 ) )
12 7 11 imbi12d ⊢ ( 𝑎 = 𝑚 → ( ( ω ⊆ 𝑎 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) ↔ ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) )
13 sseq2 ⊢ ( 𝑎 = 𝐴 → ( ω ⊆ 𝑎 ↔ ω ⊆ 𝐴 ) )
14 xpeq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑎 = 𝐴 ) → ( 𝑎 × 𝑎 ) = ( 𝐴 × 𝐴 ) )
15 14 anidms ⊢ ( 𝑎 = 𝐴 → ( 𝑎 × 𝑎 ) = ( 𝐴 × 𝐴 ) )
16 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
17 15 16 breq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 × 𝑎 ) ≈ 𝑎 ↔ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) )
18 13 17 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ω ⊆ 𝑎 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) ↔ ( ω ⊆ 𝐴 → ( 𝐴 × 𝐴 ) ≈ 𝐴 ) ) )
19 vex ⊢ 𝑎 ∈ V
20 19 19 xpex ⊢ ( 𝑎 × 𝑎 ) ∈ V
21 simpll ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → 𝑎 ∈ On )
22 4 21 sylbi ⊢ ( 𝜑 → 𝑎 ∈ On )
23 onss ⊢ ( 𝑎 ∈ On → 𝑎 ⊆ On )
24 22 23 syl ⊢ ( 𝜑 → 𝑎 ⊆ On )
25 xpss12 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ⊆ On ) → ( 𝑎 × 𝑎 ) ⊆ ( On × On ) )
26 24 24 25 syl2anc ⊢ ( 𝜑 → ( 𝑎 × 𝑎 ) ⊆ ( On × On ) )
27 1 2 r0weon ⊢ ( 𝑅 We ( On × On ) ∧ 𝑅 Se ( On × On ) )
28 27 simpli ⊢ 𝑅 We ( On × On )
29 wess ⊢ ( ( 𝑎 × 𝑎 ) ⊆ ( On × On ) → ( 𝑅 We ( On × On ) → 𝑅 We ( 𝑎 × 𝑎 ) ) )
30 26 28 29 mpisyl ⊢ ( 𝜑 → 𝑅 We ( 𝑎 × 𝑎 ) )
31 weinxp ⊢ ( 𝑅 We ( 𝑎 × 𝑎 ) ↔ ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) We ( 𝑎 × 𝑎 ) )
32 30 31 sylib ⊢ ( 𝜑 → ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) We ( 𝑎 × 𝑎 ) )
33 weeq1 ⊢ ( 𝑄 = ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) → ( 𝑄 We ( 𝑎 × 𝑎 ) ↔ ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) We ( 𝑎 × 𝑎 ) ) )
34 3 33 ax-mp ⊢ ( 𝑄 We ( 𝑎 × 𝑎 ) ↔ ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) We ( 𝑎 × 𝑎 ) )
35 32 34 sylibr ⊢ ( 𝜑 → 𝑄 We ( 𝑎 × 𝑎 ) )
36 6 oiiso ⊢ ( ( ( 𝑎 × 𝑎 ) ∈ V ∧ 𝑄 We ( 𝑎 × 𝑎 ) ) → 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) )
37 20 35 36 sylancr ⊢ ( 𝜑 → 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) )
38 isof1o ⊢ ( 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) → 𝐽 : dom 𝐽 –1-1-onto→ ( 𝑎 × 𝑎 ) )
39 f1ocnv ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ ( 𝑎 × 𝑎 ) → ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ dom 𝐽 )
40 f1of1 ⊢ ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ dom 𝐽 → ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1→ dom 𝐽 )
41 37 38 39 40 4syl ⊢ ( 𝜑 → ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1→ dom 𝐽 )
42 f1f1orn ⊢ ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1→ dom 𝐽 → ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ ran ◡ 𝐽 )
43 20 f1oen ⊢ ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ ran ◡ 𝐽 → ( 𝑎 × 𝑎 ) ≈ ran ◡ 𝐽 )
44 41 42 43 3syl ⊢ ( 𝜑 → ( 𝑎 × 𝑎 ) ≈ ran ◡ 𝐽 )
45 f1ofn ⊢ ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ dom 𝐽 → ◡ 𝐽 Fn ( 𝑎 × 𝑎 ) )
46 37 38 39 45 4syl ⊢ ( 𝜑 → ◡ 𝐽 Fn ( 𝑎 × 𝑎 ) )
47 37 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) )
48 38 39 40 3syl ⊢ ( 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) → ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1→ dom 𝐽 )
49 cnvimass ⊢ ( ◡ 𝑄 “ { 𝑤 } ) ⊆ dom 𝑄
50 inss2 ⊢ ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) ⊆ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) )
51 3 50 eqsstri ⊢ 𝑄 ⊆ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) )
52 dmss ⊢ ( 𝑄 ⊆ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) → dom 𝑄 ⊆ dom ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) )
53 51 52 ax-mp ⊢ dom 𝑄 ⊆ dom ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) )
54 dmxpid ⊢ dom ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) = ( 𝑎 × 𝑎 )
55 53 54 sseqtri ⊢ dom 𝑄 ⊆ ( 𝑎 × 𝑎 )
56 49 55 sstri ⊢ ( ◡ 𝑄 “ { 𝑤 } ) ⊆ ( 𝑎 × 𝑎 )
57 f1ores ⊢ ( ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1→ dom 𝐽 ∧ ( ◡ 𝑄 “ { 𝑤 } ) ⊆ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ↾ ( ◡ 𝑄 “ { 𝑤 } ) ) : ( ◡ 𝑄 “ { 𝑤 } ) –1-1-onto→ ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) )
58 48 56 57 sylancl ⊢ ( 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ↾ ( ◡ 𝑄 “ { 𝑤 } ) ) : ( ◡ 𝑄 “ { 𝑤 } ) –1-1-onto→ ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) )
59 20 20 xpex ⊢ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ∈ V
60 59 inex2 ⊢ ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) ∈ V
61 3 60 eqeltri ⊢ 𝑄 ∈ V
62 61 cnvex ⊢ ◡ 𝑄 ∈ V
63 62 imaex ⊢ ( ◡ 𝑄 “ { 𝑤 } ) ∈ V
64 63 f1oen ⊢ ( ( ◡ 𝐽 ↾ ( ◡ 𝑄 “ { 𝑤 } ) ) : ( ◡ 𝑄 “ { 𝑤 } ) –1-1-onto→ ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ≈ ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) )
65 47 58 64 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ≈ ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) )
66 sseqin2 ⊢ ( ( ◡ 𝑄 “ { 𝑤 } ) ⊆ ( 𝑎 × 𝑎 ) ↔ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) = ( ◡ 𝑄 “ { 𝑤 } ) )
67 56 66 mpbi ⊢ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) = ( ◡ 𝑄 “ { 𝑤 } )
68 67 imaeq2i ⊢ ( ◡ 𝐽 “ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) ) = ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) )
69 isocnv ⊢ ( 𝐽 Isom E , 𝑄 ( dom 𝐽 , ( 𝑎 × 𝑎 ) ) → ◡ 𝐽 Isom 𝑄 , E ( ( 𝑎 × 𝑎 ) , dom 𝐽 ) )
70 47 69 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ◡ 𝐽 Isom 𝑄 , E ( ( 𝑎 × 𝑎 ) , dom 𝐽 ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → 𝑤 ∈ ( 𝑎 × 𝑎 ) )
72 isoini ⊢ ( ( ◡ 𝐽 Isom 𝑄 , E ( ( 𝑎 × 𝑎 ) , dom 𝐽 ) ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 “ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) ) = ( dom 𝐽 ∩ ( ◡ E “ { ( ◡ 𝐽 ‘ 𝑤 ) } ) ) )
73 70 71 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 “ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) ) = ( dom 𝐽 ∩ ( ◡ E “ { ( ◡ 𝐽 ‘ 𝑤 ) } ) ) )
74 fvex ⊢ ( ◡ 𝐽 ‘ 𝑤 ) ∈ V
75 74 epini ⊢ ( ◡ E “ { ( ◡ 𝐽 ‘ 𝑤 ) } ) = ( ◡ 𝐽 ‘ 𝑤 )
76 75 ineq2i ⊢ ( dom 𝐽 ∩ ( ◡ E “ { ( ◡ 𝐽 ‘ 𝑤 ) } ) ) = ( dom 𝐽 ∩ ( ◡ 𝐽 ‘ 𝑤 ) )
77 6 oicl ⊢ Ord dom 𝐽
78 f1of ⊢ ( ◡ 𝐽 : ( 𝑎 × 𝑎 ) –1-1-onto→ dom 𝐽 → ◡ 𝐽 : ( 𝑎 × 𝑎 ) ⟶ dom 𝐽 )
79 37 38 39 78 4syl ⊢ ( 𝜑 → ◡ 𝐽 : ( 𝑎 × 𝑎 ) ⟶ dom 𝐽 )
80 79 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ∈ dom 𝐽 )
81 ordelss ⊢ ( ( Ord dom 𝐽 ∧ ( ◡ 𝐽 ‘ 𝑤 ) ∈ dom 𝐽 ) → ( ◡ 𝐽 ‘ 𝑤 ) ⊆ dom 𝐽 )
82 77 80 81 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ⊆ dom 𝐽 )
83 sseqin2 ⊢ ( ( ◡ 𝐽 ‘ 𝑤 ) ⊆ dom 𝐽 ↔ ( dom 𝐽 ∩ ( ◡ 𝐽 ‘ 𝑤 ) ) = ( ◡ 𝐽 ‘ 𝑤 ) )
84 82 83 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( dom 𝐽 ∩ ( ◡ 𝐽 ‘ 𝑤 ) ) = ( ◡ 𝐽 ‘ 𝑤 ) )
85 76 84 syl5eq ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( dom 𝐽 ∩ ( ◡ E “ { ( ◡ 𝐽 ‘ 𝑤 ) } ) ) = ( ◡ 𝐽 ‘ 𝑤 ) )
86 73 85 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 “ ( ( 𝑎 × 𝑎 ) ∩ ( ◡ 𝑄 “ { 𝑤 } ) ) ) = ( ◡ 𝐽 ‘ 𝑤 ) )
87 68 86 syl5eqr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 “ ( ◡ 𝑄 “ { 𝑤 } ) ) = ( ◡ 𝐽 ‘ 𝑤 ) )
88 65 87 breqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ≈ ( ◡ 𝐽 ‘ 𝑤 ) )
89 88 ensymd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ≈ ( ◡ 𝑄 “ { 𝑤 } ) )
90 fvex ⊢ ( 1st ‘ 𝑤 ) ∈ V
91 fvex ⊢ ( 2nd ‘ 𝑤 ) ∈ V
92 90 91 unex ⊢ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∈ V
93 5 92 eqeltri ⊢ 𝑀 ∈ V
94 93 sucex ⊢ suc 𝑀 ∈ V
95 94 94 xpex ⊢ ( suc 𝑀 × suc 𝑀 ) ∈ V
96 xpss ⊢ ( 𝑎 × 𝑎 ) ⊆ ( V × V )
97 simp3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) )
98 vex ⊢ 𝑧 ∈ V
99 98 eliniseg ⊢ ( 𝑤 ∈ V → ( 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ↔ 𝑧 𝑄 𝑤 ) )
100 99 elv ⊢ ( 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ↔ 𝑧 𝑄 𝑤 )
101 97 100 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑧 𝑄 𝑤 )
102 3 breqi ⊢ ( 𝑧 𝑄 𝑤 ↔ 𝑧 ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) 𝑤 )
103 brin ⊢ ( 𝑧 ( 𝑅 ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) 𝑤 ↔ ( 𝑧 𝑅 𝑤 ∧ 𝑧 ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) 𝑤 ) )
104 102 103 bitri ⊢ ( 𝑧 𝑄 𝑤 ↔ ( 𝑧 𝑅 𝑤 ∧ 𝑧 ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) 𝑤 ) )
105 104 simprbi ⊢ ( 𝑧 𝑄 𝑤 → 𝑧 ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) 𝑤 )
106 brxp ⊢ ( 𝑧 ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) 𝑤 ↔ ( 𝑧 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) )
107 106 simplbi ⊢ ( 𝑧 ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) 𝑤 → 𝑧 ∈ ( 𝑎 × 𝑎 ) )
108 101 105 107 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑧 ∈ ( 𝑎 × 𝑎 ) )
109 96 108 sseldi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑧 ∈ ( V × V ) )
110 22 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → 𝑎 ∈ On )
111 110 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑎 ∈ On )
112 xp1st ⊢ ( 𝑧 ∈ ( 𝑎 × 𝑎 ) → ( 1st ‘ 𝑧 ) ∈ 𝑎 )
113 onelon ⊢ ( ( 𝑎 ∈ On ∧ ( 1st ‘ 𝑧 ) ∈ 𝑎 ) → ( 1st ‘ 𝑧 ) ∈ On )
114 112 113 sylan2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑧 ∈ ( 𝑎 × 𝑎 ) ) → ( 1st ‘ 𝑧 ) ∈ On )
115 111 108 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 1st ‘ 𝑧 ) ∈ On )
116 eloni ⊢ ( 𝑎 ∈ On → Ord 𝑎 )
117 elxp7 ⊢ ( 𝑤 ∈ ( 𝑎 × 𝑎 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝑎 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝑎 ) ) )
118 117 simprbi ⊢ ( 𝑤 ∈ ( 𝑎 × 𝑎 ) → ( ( 1st ‘ 𝑤 ) ∈ 𝑎 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝑎 ) )
119 ordunel ⊢ ( ( Ord 𝑎 ∧ ( 1st ‘ 𝑤 ) ∈ 𝑎 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝑎 ) → ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∈ 𝑎 )
120 119 3expib ⊢ ( Ord 𝑎 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝑎 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝑎 ) → ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∈ 𝑎 ) )
121 116 118 120 syl2im ⊢ ( 𝑎 ∈ On → ( 𝑤 ∈ ( 𝑎 × 𝑎 ) → ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∈ 𝑎 ) )
122 110 71 121 sylc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∈ 𝑎 )
123 5 122 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → 𝑀 ∈ 𝑎 )
124 simprr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 )
125 4 124 sylbi ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 )
126 simprl ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ω ⊆ 𝑎 )
127 4 126 sylbi ⊢ ( 𝜑 → ω ⊆ 𝑎 )
128 iscard ⊢ ( ( card ‘ 𝑎 ) = 𝑎 ↔ ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) )
129 cardlim ⊢ ( ω ⊆ ( card ‘ 𝑎 ) ↔ Lim ( card ‘ 𝑎 ) )
130 sseq2 ⊢ ( ( card ‘ 𝑎 ) = 𝑎 → ( ω ⊆ ( card ‘ 𝑎 ) ↔ ω ⊆ 𝑎 ) )
131 limeq ⊢ ( ( card ‘ 𝑎 ) = 𝑎 → ( Lim ( card ‘ 𝑎 ) ↔ Lim 𝑎 ) )
132 130 131 bibi12d ⊢ ( ( card ‘ 𝑎 ) = 𝑎 → ( ( ω ⊆ ( card ‘ 𝑎 ) ↔ Lim ( card ‘ 𝑎 ) ) ↔ ( ω ⊆ 𝑎 ↔ Lim 𝑎 ) ) )
133 129 132 mpbii ⊢ ( ( card ‘ 𝑎 ) = 𝑎 → ( ω ⊆ 𝑎 ↔ Lim 𝑎 ) )
134 128 133 sylbir ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) → ( ω ⊆ 𝑎 ↔ Lim 𝑎 ) )
135 134 biimpa ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ∧ ω ⊆ 𝑎 ) → Lim 𝑎 )
136 22 125 127 135 syl21anc ⊢ ( 𝜑 → Lim 𝑎 )
137 136 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → Lim 𝑎 )
138 limsuc ⊢ ( Lim 𝑎 → ( 𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎 ) )
139 137 138 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( 𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎 ) )
140 123 139 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → suc 𝑀 ∈ 𝑎 )
141 onelon ⊢ ( ( 𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎 ) → suc 𝑀 ∈ On )
142 22 140 141 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → suc 𝑀 ∈ On )
143 142 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → suc 𝑀 ∈ On )
144 ssun1 ⊢ ( 1st ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) )
145 144 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 1st ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) )
146 104 simplbi ⊢ ( 𝑧 𝑄 𝑤 → 𝑧 𝑅 𝑤 )
147 df-br ⊢ ( 𝑧 𝑅 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑅 )
148 2 eleq2i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑅 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) } )
149 opabidw ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) } ↔ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) )
150 147 148 149 3bitri ⊢ ( 𝑧 𝑅 𝑤 ↔ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) )
151 150 simprbi ⊢ ( 𝑧 𝑅 𝑤 → ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) )
152 simpl ⊢ ( ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) )
153 152 orim2i ⊢ ( ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) → ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) )
154 151 153 syl ⊢ ( 𝑧 𝑅 𝑤 → ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) )
155 fvex ⊢ ( 1st ‘ 𝑧 ) ∈ V
156 fvex ⊢ ( 2nd ‘ 𝑧 ) ∈ V
157 155 156 unex ⊢ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ V
158 157 elsuc ⊢ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ↔ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ) )
159 154 158 sylibr ⊢ ( 𝑧 𝑅 𝑤 → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) )
160 suceq ⊢ ( 𝑀 = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) → suc 𝑀 = suc ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) )
161 5 160 ax-mp ⊢ suc 𝑀 = suc ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) )
162 159 161 eleqtrrdi ⊢ ( 𝑧 𝑅 𝑤 → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 )
163 101 146 162 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 )
164 ontr2 ⊢ ( ( ( 1st ‘ 𝑧 ) ∈ On ∧ suc 𝑀 ∈ On ) → ( ( ( 1st ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∧ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 ) → ( 1st ‘ 𝑧 ) ∈ suc 𝑀 ) )
165 164 imp ⊢ ( ( ( ( 1st ‘ 𝑧 ) ∈ On ∧ suc 𝑀 ∈ On ) ∧ ( ( 1st ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∧ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 ) ) → ( 1st ‘ 𝑧 ) ∈ suc 𝑀 )
166 115 143 145 163 165 syl22anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 1st ‘ 𝑧 ) ∈ suc 𝑀 )
167 xp2nd ⊢ ( 𝑧 ∈ ( 𝑎 × 𝑎 ) → ( 2nd ‘ 𝑧 ) ∈ 𝑎 )
168 onelon ⊢ ( ( 𝑎 ∈ On ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑎 ) → ( 2nd ‘ 𝑧 ) ∈ On )
169 167 168 sylan2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑧 ∈ ( 𝑎 × 𝑎 ) ) → ( 2nd ‘ 𝑧 ) ∈ On )
170 111 108 169 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 2nd ‘ 𝑧 ) ∈ On )
171 ssun2 ⊢ ( 2nd ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) )
172 171 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 2nd ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) )
173 ontr2 ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ On ∧ suc 𝑀 ∈ On ) → ( ( ( 2nd ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∧ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 ) → ( 2nd ‘ 𝑧 ) ∈ suc 𝑀 ) )
174 173 imp ⊢ ( ( ( ( 2nd ‘ 𝑧 ) ∈ On ∧ suc 𝑀 ∈ On ) ∧ ( ( 2nd ‘ 𝑧 ) ⊆ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∧ ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ suc 𝑀 ) ) → ( 2nd ‘ 𝑧 ) ∈ suc 𝑀 )
175 170 143 172 163 174 syl22anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → ( 2nd ‘ 𝑧 ) ∈ suc 𝑀 )
176 elxp7 ⊢ ( 𝑧 ∈ ( suc 𝑀 × suc 𝑀 ) ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ suc 𝑀 ∧ ( 2nd ‘ 𝑧 ) ∈ suc 𝑀 ) ) )
177 176 biimpri ⊢ ( ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) ∈ suc 𝑀 ∧ ( 2nd ‘ 𝑧 ) ∈ suc 𝑀 ) ) → 𝑧 ∈ ( suc 𝑀 × suc 𝑀 ) )
178 109 166 175 177 syl12anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ∧ 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) ) → 𝑧 ∈ ( suc 𝑀 × suc 𝑀 ) )
179 178 3expia ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( 𝑧 ∈ ( ◡ 𝑄 “ { 𝑤 } ) → 𝑧 ∈ ( suc 𝑀 × suc 𝑀 ) ) )
180 179 ssrdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ⊆ ( suc 𝑀 × suc 𝑀 ) )
181 ssdomg ⊢ ( ( suc 𝑀 × suc 𝑀 ) ∈ V → ( ( ◡ 𝑄 “ { 𝑤 } ) ⊆ ( suc 𝑀 × suc 𝑀 ) → ( ◡ 𝑄 “ { 𝑤 } ) ≼ ( suc 𝑀 × suc 𝑀 ) ) )
182 95 180 181 mpsyl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ≼ ( suc 𝑀 × suc 𝑀 ) )
183 127 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ω ⊆ 𝑎 )
184 nnfi ⊢ ( suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin )
185 xpfi ⊢ ( ( suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin ) → ( suc 𝑀 × suc 𝑀 ) ∈ Fin )
186 185 anidms ⊢ ( suc 𝑀 ∈ Fin → ( suc 𝑀 × suc 𝑀 ) ∈ Fin )
187 isfinite ⊢ ( ( suc 𝑀 × suc 𝑀 ) ∈ Fin ↔ ( suc 𝑀 × suc 𝑀 ) ≺ ω )
188 186 187 sylib ⊢ ( suc 𝑀 ∈ Fin → ( suc 𝑀 × suc 𝑀 ) ≺ ω )
189 184 188 syl ⊢ ( suc 𝑀 ∈ ω → ( suc 𝑀 × suc 𝑀 ) ≺ ω )
190 ssdomg ⊢ ( 𝑎 ∈ V → ( ω ⊆ 𝑎 → ω ≼ 𝑎 ) )
191 190 elv ⊢ ( ω ⊆ 𝑎 → ω ≼ 𝑎 )
192 sdomdomtr ⊢ ( ( ( suc 𝑀 × suc 𝑀 ) ≺ ω ∧ ω ≼ 𝑎 ) → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 )
193 189 191 192 syl2an ⊢ ( ( suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎 ) → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 )
194 193 expcom ⊢ ( ω ⊆ 𝑎 → ( suc 𝑀 ∈ ω → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 ) )
195 183 194 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( suc 𝑀 ∈ ω → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 ) )
196 breq1 ⊢ ( 𝑚 = suc 𝑀 → ( 𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎 ) )
197 125 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 )
198 196 197 140 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → suc 𝑀 ≺ 𝑎 )
199 omelon ⊢ ω ∈ On
200 ontri1 ⊢ ( ( ω ∈ On ∧ suc 𝑀 ∈ On ) → ( ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω ) )
201 199 142 200 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω ) )
202 sseq2 ⊢ ( 𝑚 = suc 𝑀 → ( ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀 ) )
203 xpeq12 ⊢ ( ( 𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀 ) → ( 𝑚 × 𝑚 ) = ( suc 𝑀 × suc 𝑀 ) )
204 203 anidms ⊢ ( 𝑚 = suc 𝑀 → ( 𝑚 × 𝑚 ) = ( suc 𝑀 × suc 𝑀 ) )
205 id ⊢ ( 𝑚 = suc 𝑀 → 𝑚 = suc 𝑀 )
206 204 205 breq12d ⊢ ( 𝑚 = suc 𝑀 → ( ( 𝑚 × 𝑚 ) ≈ 𝑚 ↔ ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 ) )
207 202 206 imbi12d ⊢ ( 𝑚 = suc 𝑀 → ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ↔ ( ω ⊆ suc 𝑀 → ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 ) ) )
208 simplr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) )
209 4 208 sylbi ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) )
211 207 210 140 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ω ⊆ suc 𝑀 → ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 ) )
212 201 211 sylbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ¬ suc 𝑀 ∈ ω → ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 ) )
213 ensdomtr ⊢ ( ( ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎 ) → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 )
214 213 expcom ⊢ ( suc 𝑀 ≺ 𝑎 → ( ( suc 𝑀 × suc 𝑀 ) ≈ suc 𝑀 → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 ) )
215 198 212 214 sylsyld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ¬ suc 𝑀 ∈ ω → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 ) )
216 195 215 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 )
217 domsdomtr ⊢ ( ( ( ◡ 𝑄 “ { 𝑤 } ) ≼ ( suc 𝑀 × suc 𝑀 ) ∧ ( suc 𝑀 × suc 𝑀 ) ≺ 𝑎 ) → ( ◡ 𝑄 “ { 𝑤 } ) ≺ 𝑎 )
218 182 216 217 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝑄 “ { 𝑤 } ) ≺ 𝑎 )
219 ensdomtr ⊢ ( ( ( ◡ 𝐽 ‘ 𝑤 ) ≈ ( ◡ 𝑄 “ { 𝑤 } ) ∧ ( ◡ 𝑄 “ { 𝑤 } ) ≺ 𝑎 ) → ( ◡ 𝐽 ‘ 𝑤 ) ≺ 𝑎 )
220 89 218 219 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ≺ 𝑎 )
221 ordelon ⊢ ( ( Ord dom 𝐽 ∧ ( ◡ 𝐽 ‘ 𝑤 ) ∈ dom 𝐽 ) → ( ◡ 𝐽 ‘ 𝑤 ) ∈ On )
222 77 80 221 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ∈ On )
223 onenon ⊢ ( 𝑎 ∈ On → 𝑎 ∈ dom card )
224 110 223 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → 𝑎 ∈ dom card )
225 cardsdomel ⊢ ( ( ( ◡ 𝐽 ‘ 𝑤 ) ∈ On ∧ 𝑎 ∈ dom card ) → ( ( ◡ 𝐽 ‘ 𝑤 ) ≺ 𝑎 ↔ ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) ) )
226 222 224 225 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ( ◡ 𝐽 ‘ 𝑤 ) ≺ 𝑎 ↔ ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) ) )
227 220 226 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) )
228 eleq2 ⊢ ( ( card ‘ 𝑎 ) = 𝑎 → ( ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) ↔ ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 ) )
229 128 228 sylbir ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) → ( ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) ↔ ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 ) )
230 22 197 229 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ( ◡ 𝐽 ‘ 𝑤 ) ∈ ( card ‘ 𝑎 ) ↔ ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 ) )
231 227 230 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑎 × 𝑎 ) ) → ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 )
232 231 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝑎 × 𝑎 ) ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 )
233 fnfvrnss ⊢ ( ( ◡ 𝐽 Fn ( 𝑎 × 𝑎 ) ∧ ∀ 𝑤 ∈ ( 𝑎 × 𝑎 ) ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 ) → ran ◡ 𝐽 ⊆ 𝑎 )
234 ssdomg ⊢ ( 𝑎 ∈ V → ( ran ◡ 𝐽 ⊆ 𝑎 → ran ◡ 𝐽 ≼ 𝑎 ) )
235 19 233 234 mpsyl ⊢ ( ( ◡ 𝐽 Fn ( 𝑎 × 𝑎 ) ∧ ∀ 𝑤 ∈ ( 𝑎 × 𝑎 ) ( ◡ 𝐽 ‘ 𝑤 ) ∈ 𝑎 ) → ran ◡ 𝐽 ≼ 𝑎 )
236 46 232 235 syl2anc ⊢ ( 𝜑 → ran ◡ 𝐽 ≼ 𝑎 )
237 endomtr ⊢ ( ( ( 𝑎 × 𝑎 ) ≈ ran ◡ 𝐽 ∧ ran ◡ 𝐽 ≼ 𝑎 ) → ( 𝑎 × 𝑎 ) ≼ 𝑎 )
238 44 236 237 syl2anc ⊢ ( 𝜑 → ( 𝑎 × 𝑎 ) ≼ 𝑎 )
239 4 238 sylbir ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ( 𝑎 × 𝑎 ) ≼ 𝑎 )
240 df1o2 ⊢ 1o = { ∅ }
241 1onn ⊢ 1o ∈ ω
242 240 241 eqeltrri ⊢ { ∅ } ∈ ω
243 nnsdom ⊢ ( { ∅ } ∈ ω → { ∅ } ≺ ω )
244 sdomdom ⊢ ( { ∅ } ≺ ω → { ∅ } ≼ ω )
245 242 243 244 mp2b ⊢ { ∅ } ≼ ω
246 domtr ⊢ ( ( { ∅ } ≼ ω ∧ ω ≼ 𝑎 ) → { ∅ } ≼ 𝑎 )
247 245 191 246 sylancr ⊢ ( ω ⊆ 𝑎 → { ∅ } ≼ 𝑎 )
248 0ex ⊢ ∅ ∈ V
249 19 248 xpsnen ⊢ ( 𝑎 × { ∅ } ) ≈ 𝑎
250 249 ensymi ⊢ 𝑎 ≈ ( 𝑎 × { ∅ } )
251 19 xpdom2 ⊢ ( { ∅ } ≼ 𝑎 → ( 𝑎 × { ∅ } ) ≼ ( 𝑎 × 𝑎 ) )
252 endomtr ⊢ ( ( 𝑎 ≈ ( 𝑎 × { ∅ } ) ∧ ( 𝑎 × { ∅ } ) ≼ ( 𝑎 × 𝑎 ) ) → 𝑎 ≼ ( 𝑎 × 𝑎 ) )
253 250 251 252 sylancr ⊢ ( { ∅ } ≼ 𝑎 → 𝑎 ≼ ( 𝑎 × 𝑎 ) )
254 247 253 syl ⊢ ( ω ⊆ 𝑎 → 𝑎 ≼ ( 𝑎 × 𝑎 ) )
255 254 ad2antrl ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → 𝑎 ≼ ( 𝑎 × 𝑎 ) )
256 sbth ⊢ ( ( ( 𝑎 × 𝑎 ) ≼ 𝑎 ∧ 𝑎 ≼ ( 𝑎 × 𝑎 ) ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
257 239 255 256 syl2anc ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
258 257 expr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ω ⊆ 𝑎 ) → ( ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
259 simplr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) )
260 simpll ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → 𝑎 ∈ On )
261 simprr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 )
262 rexnal ⊢ ( ∃ 𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 )
263 onelss ⊢ ( 𝑎 ∈ On → ( 𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎 ) )
264 ssdomg ⊢ ( 𝑎 ∈ On → ( 𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎 ) )
265 263 264 syld ⊢ ( 𝑎 ∈ On → ( 𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎 ) )
266 bren2 ⊢ ( 𝑚 ≈ 𝑎 ↔ ( 𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎 ) )
267 266 simplbi2 ⊢ ( 𝑚 ≼ 𝑎 → ( ¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎 ) )
268 265 267 syl6 ⊢ ( 𝑎 ∈ On → ( 𝑚 ∈ 𝑎 → ( ¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎 ) ) )
269 268 reximdvai ⊢ ( 𝑎 ∈ On → ( ∃ 𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃ 𝑚 ∈ 𝑎 𝑚 ≈ 𝑎 ) )
270 262 269 syl5bir ⊢ ( 𝑎 ∈ On → ( ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃ 𝑚 ∈ 𝑎 𝑚 ≈ 𝑎 ) )
271 260 261 270 sylc ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ∃ 𝑚 ∈ 𝑎 𝑚 ≈ 𝑎 )
272 r19.29 ⊢ ( ( ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ ∃ 𝑚 ∈ 𝑎 𝑚 ≈ 𝑎 ) → ∃ 𝑚 ∈ 𝑎 ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) )
273 259 271 272 syl2anc ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ∃ 𝑚 ∈ 𝑎 ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) )
274 simprl ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ω ⊆ 𝑎 )
275 onelon ⊢ ( ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) → 𝑚 ∈ On )
276 ensym ⊢ ( 𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚 )
277 domentr ⊢ ( ( ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚 ) → ω ≼ 𝑚 )
278 191 276 277 syl2an ⊢ ( ( ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎 ) → ω ≼ 𝑚 )
279 domnsym ⊢ ( ω ≼ 𝑚 → ¬ 𝑚 ≺ ω )
280 nnsdom ⊢ ( 𝑚 ∈ ω → 𝑚 ≺ ω )
281 279 280 nsyl ⊢ ( ω ≼ 𝑚 → ¬ 𝑚 ∈ ω )
282 ontri1 ⊢ ( ( ω ∈ On ∧ 𝑚 ∈ On ) → ( ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω ) )
283 199 282 mpan ⊢ ( 𝑚 ∈ On → ( ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω ) )
284 281 283 syl5ibr ⊢ ( 𝑚 ∈ On → ( ω ≼ 𝑚 → ω ⊆ 𝑚 ) )
285 275 278 284 syl2im ⊢ ( ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) → ( ( ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎 ) → ω ⊆ 𝑚 ) )
286 285 expd ⊢ ( ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) → ( ω ⊆ 𝑎 → ( 𝑚 ≈ 𝑎 → ω ⊆ 𝑚 ) ) )
287 286 impcom ⊢ ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) → ( 𝑚 ≈ 𝑎 → ω ⊆ 𝑚 ) )
288 287 imim1d ⊢ ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) → ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) → ( 𝑚 ≈ 𝑎 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) )
289 288 imp32 ⊢ ( ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) ∧ ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) ) → ( 𝑚 × 𝑚 ) ≈ 𝑚 )
290 entr ⊢ ( ( ( 𝑚 × 𝑚 ) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎 ) → ( 𝑚 × 𝑚 ) ≈ 𝑎 )
291 290 ancoms ⊢ ( ( 𝑚 ≈ 𝑎 ∧ ( 𝑚 × 𝑚 ) ≈ 𝑚 ) → ( 𝑚 × 𝑚 ) ≈ 𝑎 )
292 xpen ⊢ ( ( 𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚 ) → ( 𝑎 × 𝑎 ) ≈ ( 𝑚 × 𝑚 ) )
293 292 anidms ⊢ ( 𝑎 ≈ 𝑚 → ( 𝑎 × 𝑎 ) ≈ ( 𝑚 × 𝑚 ) )
294 entr ⊢ ( ( ( 𝑎 × 𝑎 ) ≈ ( 𝑚 × 𝑚 ) ∧ ( 𝑚 × 𝑚 ) ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
295 293 294 sylan ⊢ ( ( 𝑎 ≈ 𝑚 ∧ ( 𝑚 × 𝑚 ) ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
296 276 291 295 syl2an2r ⊢ ( ( 𝑚 ≈ 𝑎 ∧ ( 𝑚 × 𝑚 ) ≈ 𝑚 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
297 296 ex ⊢ ( 𝑚 ≈ 𝑎 → ( ( 𝑚 × 𝑚 ) ≈ 𝑚 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
298 297 ad2antll ⊢ ( ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) ∧ ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) ) → ( ( 𝑚 × 𝑚 ) ≈ 𝑚 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
299 289 298 mpd ⊢ ( ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) ∧ ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
300 299 ex ⊢ ( ( ω ⊆ 𝑎 ∧ ( 𝑎 ∈ On ∧ 𝑚 ∈ 𝑎 ) ) → ( ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
301 300 expr ⊢ ( ( ω ⊆ 𝑎 ∧ 𝑎 ∈ On ) → ( 𝑚 ∈ 𝑎 → ( ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) ) )
302 301 rexlimdv ⊢ ( ( ω ⊆ 𝑎 ∧ 𝑎 ∈ On ) → ( ∃ 𝑚 ∈ 𝑎 ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
303 274 260 302 syl2anc ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ( ∃ 𝑚 ∈ 𝑎 ( ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ∧ 𝑚 ≈ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
304 273 303 mpd ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
305 304 expr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ω ⊆ 𝑎 ) → ( ¬ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) )
306 258 305 pm2.61d ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ω ⊆ 𝑎 ) → ( 𝑎 × 𝑎 ) ≈ 𝑎 )
307 306 exp31 ⊢ ( 𝑎 ∈ On → ( ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) → ( ω ⊆ 𝑎 → ( 𝑎 × 𝑎 ) ≈ 𝑎 ) ) )
308 12 18 307 tfis3 ⊢ ( 𝐴 ∈ On → ( ω ⊆ 𝐴 → ( 𝐴 × 𝐴 ) ≈ 𝐴 ) )
309 308 imp ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )