Metamath Proof Explorer

Theorem infxpenc

Description: A canonical version of infxpen , by a completely different approach (although it uses infxpen via xpomen ). Using Cantor's normal form, we can show that A ^o B respects equinumerosity ( oef1o ), so that all the steps of (om ^ W ) x. ( om ^ W ) ~_om ^ ( 2 W ) ~ (om ^ 2 ) ^ W ~_om ^ W can be verified using bijections to do the ordinal commutations. (The assumption on N can be satisfied using cnfcom3c .) (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
infxpenc.2 ⊢ ( 𝜑 → ω ⊆ 𝐴 )
infxpenc.3 ⊢ ( 𝜑 → 𝑊 ∈ ( On ∖ 1o ) )
infxpenc.4 ⊢ ( 𝜑 → 𝐹 : ( ω ↑o 2o ) –1-1-onto→ ω )
infxpenc.5 ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
infxpenc.6 ⊢ ( 𝜑 → 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) )
infxpenc.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) )
infxpenc.h ⊢ 𝐻 = ( ( ( ω CNF 𝑊 ) ∘ 𝐾 ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) )
infxpenc.l ⊢ 𝐿 = ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( 𝑌 ∘ ◡ 𝑋 ) ) ) )
infxpenc.x ⊢ 𝑋 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) )
infxpenc.y ⊢ 𝑌 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) )
infxpenc.j ⊢ 𝐽 = ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ 𝐿 ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) )
infxpenc.z ⊢ 𝑍 = ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) )
infxpenc.t ⊢ 𝑇 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ )
infxpenc.g ⊢ 𝐺 = ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) )
Assertion infxpenc ( 𝜑 → 𝐺 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )

Proof

Step Hyp Ref Expression
1 infxpenc.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 infxpenc.2 ⊢ ( 𝜑 → ω ⊆ 𝐴 )
3 infxpenc.3 ⊢ ( 𝜑 → 𝑊 ∈ ( On ∖ 1o ) )
4 infxpenc.4 ⊢ ( 𝜑 → 𝐹 : ( ω ↑o 2o ) –1-1-onto→ ω )
5 infxpenc.5 ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
6 infxpenc.6 ⊢ ( 𝜑 → 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) )
7 infxpenc.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) )
8 infxpenc.h ⊢ 𝐻 = ( ( ( ω CNF 𝑊 ) ∘ 𝐾 ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) )
9 infxpenc.l ⊢ 𝐿 = ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( 𝑌 ∘ ◡ 𝑋 ) ) ) )
10 infxpenc.x ⊢ 𝑋 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) )
11 infxpenc.y ⊢ 𝑌 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) )
12 infxpenc.j ⊢ 𝐽 = ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ 𝐿 ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) )
13 infxpenc.z ⊢ 𝑍 = ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) )
14 infxpenc.t ⊢ 𝑇 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ )
15 infxpenc.g ⊢ 𝐺 = ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) )
16 f1ocnv ⊢ ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) → ◡ 𝑁 : ( ω ↑o 𝑊 ) –1-1-onto→ 𝐴 )
17 6 16 syl ⊢ ( 𝜑 → ◡ 𝑁 : ( ω ↑o 𝑊 ) –1-1-onto→ 𝐴 )
18 f1oi ⊢ ( I ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝑊
19 18 a1i ⊢ ( 𝜑 → ( I ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝑊 )
20 omelon ⊢ ω ∈ On
21 20 a1i ⊢ ( 𝜑 → ω ∈ On )
22 2on ⊢ 2o ∈ On
23 oecl ⊢ ( ( ω ∈ On ∧ 2o ∈ On ) → ( ω ↑o 2o ) ∈ On )
24 21 22 23 sylancl ⊢ ( 𝜑 → ( ω ↑o 2o ) ∈ On )
25 22 a1i ⊢ ( 𝜑 → 2o ∈ On )
26 peano1 ⊢ ∅ ∈ ω
27 26 a1i ⊢ ( 𝜑 → ∅ ∈ ω )
28 oen0 ⊢ ( ( ( ω ∈ On ∧ 2o ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 2o ) )
29 21 25 27 28 syl21anc ⊢ ( 𝜑 → ∅ ∈ ( ω ↑o 2o ) )
30 ondif1 ⊢ ( ( ω ↑o 2o ) ∈ ( On ∖ 1o ) ↔ ( ( ω ↑o 2o ) ∈ On ∧ ∅ ∈ ( ω ↑o 2o ) ) )
31 24 29 30 sylanbrc ⊢ ( 𝜑 → ( ω ↑o 2o ) ∈ ( On ∖ 1o ) )
32 3 eldifad ⊢ ( 𝜑 → 𝑊 ∈ On )
33 4 19 31 32 21 32 5 7 8 oef1o ⊢ ( 𝜑 → 𝐻 : ( ( ω ↑o 2o ) ↑o 𝑊 ) –1-1-onto→ ( ω ↑o 𝑊 ) )
34 f1oi ⊢ ( I ↾ ω ) : ω –1-1-onto→ ω
35 34 a1i ⊢ ( 𝜑 → ( I ↾ ω ) : ω –1-1-onto→ ω )
36 10 11 omf1o ⊢ ( ( 𝑊 ∈ On ∧ 2o ∈ On ) → ( 𝑌 ∘ ◡ 𝑋 ) : ( 𝑊 ·o 2o ) –1-1-onto→ ( 2o ·o 𝑊 ) )
37 32 22 36 sylancl ⊢ ( 𝜑 → ( 𝑌 ∘ ◡ 𝑋 ) : ( 𝑊 ·o 2o ) –1-1-onto→ ( 2o ·o 𝑊 ) )
38 ondif1 ⊢ ( ω ∈ ( On ∖ 1o ) ↔ ( ω ∈ On ∧ ∅ ∈ ω ) )
39 20 26 38 mpbir2an ⊢ ω ∈ ( On ∖ 1o )
40 39 a1i ⊢ ( 𝜑 → ω ∈ ( On ∖ 1o ) )
41 omcl ⊢ ( ( 𝑊 ∈ On ∧ 2o ∈ On ) → ( 𝑊 ·o 2o ) ∈ On )
42 32 22 41 sylancl ⊢ ( 𝜑 → ( 𝑊 ·o 2o ) ∈ On )
43 omcl ⊢ ( ( 2o ∈ On ∧ 𝑊 ∈ On ) → ( 2o ·o 𝑊 ) ∈ On )
44 25 32 43 syl2anc ⊢ ( 𝜑 → ( 2o ·o 𝑊 ) ∈ On )
45 fvresi ⊢ ( ∅ ∈ ω → ( ( I ↾ ω ) ‘ ∅ ) = ∅ )
46 26 45 mp1i ⊢ ( 𝜑 → ( ( I ↾ ω ) ‘ ∅ ) = ∅ )
47 35 37 40 42 21 44 46 9 12 oef1o ⊢ ( 𝜑 → 𝐽 : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ω ↑o ( 2o ·o 𝑊 ) ) )
48 oeoe ⊢ ( ( ω ∈ On ∧ 2o ∈ On ∧ 𝑊 ∈ On ) → ( ( ω ↑o 2o ) ↑o 𝑊 ) = ( ω ↑o ( 2o ·o 𝑊 ) ) )
49 20 25 32 48 mp3an2i ⊢ ( 𝜑 → ( ( ω ↑o 2o ) ↑o 𝑊 ) = ( ω ↑o ( 2o ·o 𝑊 ) ) )
50 49 f1oeq3d ⊢ ( 𝜑 → ( 𝐽 : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ( ω ↑o 2o ) ↑o 𝑊 ) ↔ 𝐽 : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ω ↑o ( 2o ·o 𝑊 ) ) ) )
51 47 50 mpbird ⊢ ( 𝜑 → 𝐽 : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ( ω ↑o 2o ) ↑o 𝑊 ) )
52 f1oco ⊢ ( ( 𝐻 : ( ( ω ↑o 2o ) ↑o 𝑊 ) –1-1-onto→ ( ω ↑o 𝑊 ) ∧ 𝐽 : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ( ω ↑o 2o ) ↑o 𝑊 ) ) → ( 𝐻 ∘ 𝐽 ) : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
53 33 51 52 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐽 ) : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
54 df-2o ⊢ 2o = suc 1o
55 54 oveq2i ⊢ ( 𝑊 ·o 2o ) = ( 𝑊 ·o suc 1o )
56 1on ⊢ 1o ∈ On
57 omsuc ⊢ ( ( 𝑊 ∈ On ∧ 1o ∈ On ) → ( 𝑊 ·o suc 1o ) = ( ( 𝑊 ·o 1o ) +o 𝑊 ) )
58 32 56 57 sylancl ⊢ ( 𝜑 → ( 𝑊 ·o suc 1o ) = ( ( 𝑊 ·o 1o ) +o 𝑊 ) )
59 55 58 syl5eq ⊢ ( 𝜑 → ( 𝑊 ·o 2o ) = ( ( 𝑊 ·o 1o ) +o 𝑊 ) )
60 om1 ⊢ ( 𝑊 ∈ On → ( 𝑊 ·o 1o ) = 𝑊 )
61 32 60 syl ⊢ ( 𝜑 → ( 𝑊 ·o 1o ) = 𝑊 )
62 61 oveq1d ⊢ ( 𝜑 → ( ( 𝑊 ·o 1o ) +o 𝑊 ) = ( 𝑊 +o 𝑊 ) )
63 59 62 eqtrd ⊢ ( 𝜑 → ( 𝑊 ·o 2o ) = ( 𝑊 +o 𝑊 ) )
64 63 oveq2d ⊢ ( 𝜑 → ( ω ↑o ( 𝑊 ·o 2o ) ) = ( ω ↑o ( 𝑊 +o 𝑊 ) ) )
65 oeoa ⊢ ( ( ω ∈ On ∧ 𝑊 ∈ On ∧ 𝑊 ∈ On ) → ( ω ↑o ( 𝑊 +o 𝑊 ) ) = ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
66 20 32 32 65 mp3an2i ⊢ ( 𝜑 → ( ω ↑o ( 𝑊 +o 𝑊 ) ) = ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
67 64 66 eqtrd ⊢ ( 𝜑 → ( ω ↑o ( 𝑊 ·o 2o ) ) = ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
68 67 f1oeq2d ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐽 ) : ( ω ↑o ( 𝑊 ·o 2o ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝐻 ∘ 𝐽 ) : ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ) )
69 53 68 mpbid ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐽 ) : ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
70 oecl ⊢ ( ( ω ∈ On ∧ 𝑊 ∈ On ) → ( ω ↑o 𝑊 ) ∈ On )
71 21 32 70 syl2anc ⊢ ( 𝜑 → ( ω ↑o 𝑊 ) ∈ On )
72 13 omxpenlem ⊢ ( ( ( ω ↑o 𝑊 ) ∈ On ∧ ( ω ↑o 𝑊 ) ∈ On ) → 𝑍 : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
73 71 71 72 syl2anc ⊢ ( 𝜑 → 𝑍 : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
74 f1oco ⊢ ( ( ( 𝐻 ∘ 𝐽 ) : ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ∧ 𝑍 : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( ω ↑o 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
75 69 73 74 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
76 f1of ⊢ ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) → 𝑁 : 𝐴 ⟶ ( ω ↑o 𝑊 ) )
77 6 76 syl ⊢ ( 𝜑 → 𝑁 : 𝐴 ⟶ ( ω ↑o 𝑊 ) )
78 77 feqmptd ⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑥 ) ) )
79 f1oeq1 ⊢ ( 𝑁 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑥 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
80 78 79 syl ⊢ ( 𝜑 → ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑥 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
81 6 80 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑥 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) )
82 77 feqmptd ⊢ ( 𝜑 → 𝑁 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑦 ) ) )
83 f1oeq1 ⊢ ( 𝑁 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑦 ) ) → ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑦 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
84 82 83 syl ⊢ ( 𝜑 → ( 𝑁 : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑦 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
85 6 84 mpbid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( 𝑁 ‘ 𝑦 ) ) : 𝐴 –1-1-onto→ ( ω ↑o 𝑊 ) )
86 81 85 xpf1o ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) )
87 f1oeq1 ⊢ ( 𝑇 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ ) → ( 𝑇 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) ) )
88 14 87 ax-mp ⊢ ( 𝑇 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝑁 ‘ 𝑥 ) , ( 𝑁 ‘ 𝑦 ) ⟩ ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) )
89 86 88 sylibr ⊢ ( 𝜑 → 𝑇 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) )
90 f1oco ⊢ ( ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) : ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ∧ 𝑇 : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) × ( ω ↑o 𝑊 ) ) ) → ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ω ↑o 𝑊 ) )
91 75 89 90 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ω ↑o 𝑊 ) )
92 f1oco ⊢ ( ( ◡ 𝑁 : ( ω ↑o 𝑊 ) –1-1-onto→ 𝐴 ∧ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) : ( 𝐴 × 𝐴 ) –1-1-onto→ ( ω ↑o 𝑊 ) ) → ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) ) : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
93 17 91 92 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) ) : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
94 f1oeq1 ⊢ ( 𝐺 = ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) ) → ( 𝐺 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ↔ ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) ) : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ) )
95 15 94 ax-mp ⊢ ( 𝐺 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 ↔ ( ◡ 𝑁 ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) ) : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
96 93 95 sylibr ⊢ ( 𝜑 → 𝐺 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )