Metamath Proof Explorer

Theorem cnfcom

Description: Any ordinal B is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses cnfcom.s ⊢ 𝑆 = dom ( ω CNF 𝐴 )
cnfcom.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cnfcom.b ⊢ ( 𝜑 → 𝐵 ∈ ( ω ↑o 𝐴 ) )
cnfcom.f ⊢ 𝐹 = ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 )
cnfcom.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
cnfcom.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ )
cnfcom.t ⊢ 𝑇 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
cnfcom.m ⊢ 𝑀 = ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
cnfcom.k ⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) )
cnfcom.1 ⊢ ( 𝜑 → 𝐼 ∈ dom 𝐺 )
Assertion cnfcom ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnfcom.s ⊢ 𝑆 = dom ( ω CNF 𝐴 )
2 cnfcom.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cnfcom.b ⊢ ( 𝜑 → 𝐵 ∈ ( ω ↑o 𝐴 ) )
4 cnfcom.f ⊢ 𝐹 = ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 )
5 cnfcom.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
6 cnfcom.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ )
7 cnfcom.t ⊢ 𝑇 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
8 cnfcom.m ⊢ 𝑀 = ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
9 cnfcom.k ⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) )
10 cnfcom.1 ⊢ ( 𝜑 → 𝐼 ∈ dom 𝐺 )
11 omelon ⊢ ω ∈ On
12 11 a1i ⊢ ( 𝜑 → ω ∈ On )
13 1 12 2 cantnff1o ⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
14 f1ocnv ⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
15 f1of ⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
16 13 14 15 3syl ⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
17 16 3 ffvelcdmd ⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
18 4 17 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
19 1 12 2 5 18 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
20 19 simprd ⊢ ( 𝜑 → dom 𝐺 ∈ ω )
21 elnn ⊢ ( ( 𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω ) → 𝐼 ∈ ω )
22 10 20 21 syl2anc ⊢ ( 𝜑 → 𝐼 ∈ ω )
23 eleq1 ⊢ ( 𝑤 = 𝐼 → ( 𝑤 ∈ dom 𝐺 ↔ 𝐼 ∈ dom 𝐺 ) )
24 suceq ⊢ ( 𝑤 = 𝐼 → suc 𝑤 = suc 𝐼 )
25 24 fveq2d ⊢ ( 𝑤 = 𝐼 → ( 𝑇 ‘ suc 𝑤 ) = ( 𝑇 ‘ suc 𝐼 ) )
26 24 fveq2d ⊢ ( 𝑤 = 𝐼 → ( 𝐻 ‘ suc 𝑤 ) = ( 𝐻 ‘ suc 𝐼 ) )
27 fveq2 ⊢ ( 𝑤 = 𝐼 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝐼 ) )
28 27 oveq2d ⊢ ( 𝑤 = 𝐼 → ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) = ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
29 2fveq3 ⊢ ( 𝑤 = 𝐼 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) )
30 28 29 oveq12d ⊢ ( 𝑤 = 𝐼 → ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
31 25 26 30 f1oeq123d ⊢ ( 𝑤 = 𝐼 → ( ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ↔ ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
32 23 31 imbi12d ⊢ ( 𝑤 = 𝐼 → ( ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ↔ ( 𝐼 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
33 32 imbi2d ⊢ ( 𝑤 = 𝐼 → ( ( 𝜑 → ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ) ↔ ( 𝜑 → ( 𝐼 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) ) )
34 eleq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺 ) )
35 suceq ⊢ ( 𝑤 = ∅ → suc 𝑤 = suc ∅ )
36 35 fveq2d ⊢ ( 𝑤 = ∅ → ( 𝑇 ‘ suc 𝑤 ) = ( 𝑇 ‘ suc ∅ ) )
37 35 fveq2d ⊢ ( 𝑤 = ∅ → ( 𝐻 ‘ suc 𝑤 ) = ( 𝐻 ‘ suc ∅ ) )
38 fveq2 ⊢ ( 𝑤 = ∅ → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ ∅ ) )
39 38 oveq2d ⊢ ( 𝑤 = ∅ → ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) = ( ω ↑o ( 𝐺 ‘ ∅ ) ) )
40 2fveq3 ⊢ ( 𝑤 = ∅ → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) )
41 39 40 oveq12d ⊢ ( 𝑤 = ∅ → ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ ∅ ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) ) )
42 36 37 41 f1oeq123d ⊢ ( 𝑤 = ∅ → ( ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ↔ ( 𝑇 ‘ suc ∅ ) : ( 𝐻 ‘ suc ∅ ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ ∅ ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) ) ) )
43 34 42 imbi12d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ↔ ( ∅ ∈ dom 𝐺 → ( 𝑇 ‘ suc ∅ ) : ( 𝐻 ‘ suc ∅ ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ ∅ ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) ) ) ) )
44 eleq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ dom 𝐺 ↔ 𝑦 ∈ dom 𝐺 ) )
45 suceq ⊢ ( 𝑤 = 𝑦 → suc 𝑤 = suc 𝑦 )
46 45 fveq2d ⊢ ( 𝑤 = 𝑦 → ( 𝑇 ‘ suc 𝑤 ) = ( 𝑇 ‘ suc 𝑦 ) )
47 45 fveq2d ⊢ ( 𝑤 = 𝑦 → ( 𝐻 ‘ suc 𝑤 ) = ( 𝐻 ‘ suc 𝑦 ) )
48 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑦 ) )
49 48 oveq2d ⊢ ( 𝑤 = 𝑦 → ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) = ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) )
50 2fveq3 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
51 49 50 oveq12d ⊢ ( 𝑤 = 𝑦 → ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
52 46 47 51 f1oeq123d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ↔ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) )
53 44 52 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ↔ ( 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) )
54 eleq1 ⊢ ( 𝑤 = suc 𝑦 → ( 𝑤 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺 ) )
55 suceq ⊢ ( 𝑤 = suc 𝑦 → suc 𝑤 = suc suc 𝑦 )
56 55 fveq2d ⊢ ( 𝑤 = suc 𝑦 → ( 𝑇 ‘ suc 𝑤 ) = ( 𝑇 ‘ suc suc 𝑦 ) )
57 55 fveq2d ⊢ ( 𝑤 = suc 𝑦 → ( 𝐻 ‘ suc 𝑤 ) = ( 𝐻 ‘ suc suc 𝑦 ) )
58 fveq2 ⊢ ( 𝑤 = suc 𝑦 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ suc 𝑦 ) )
59 58 oveq2d ⊢ ( 𝑤 = suc 𝑦 → ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) = ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) )
60 2fveq3 ⊢ ( 𝑤 = suc 𝑦 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) )
61 59 60 oveq12d ⊢ ( 𝑤 = suc 𝑦 → ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) )
62 56 57 61 f1oeq123d ⊢ ( 𝑤 = suc 𝑦 → ( ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ↔ ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
63 54 62 imbi12d ⊢ ( 𝑤 = suc 𝑦 → ( ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ↔ ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) )
64 2 adantr ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → 𝐴 ∈ On )
65 3 adantr ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → 𝐵 ∈ ( ω ↑o 𝐴 ) )
66 simpr ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ∅ ∈ dom 𝐺 )
67 11 a1i ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ω ∈ On )
68 suppssdm ⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
69 1 12 2 cantnfs ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
70 18 69 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) )
71 70 simpld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ω )
72 68 71 fssdm ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐴 )
73 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
74 2 73 syl ⊢ ( 𝜑 → 𝐴 ⊆ On )
75 72 74 sstrd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ On )
76 5 oif ⊢ 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ )
77 76 ffvelcdmi ⊢ ( ∅ ∈ dom 𝐺 → ( 𝐺 ‘ ∅ ) ∈ ( 𝐹 supp ∅ ) )
78 ssel2 ⊢ ( ( ( 𝐹 supp ∅ ) ⊆ On ∧ ( 𝐺 ‘ ∅ ) ∈ ( 𝐹 supp ∅ ) ) → ( 𝐺 ‘ ∅ ) ∈ On )
79 75 77 78 syl2an ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ( 𝐺 ‘ ∅ ) ∈ On )
80 peano1 ⊢ ∅ ∈ ω
81 80 a1i ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ∅ ∈ ω )
82 oen0 ⊢ ( ( ( ω ∈ On ∧ ( 𝐺 ‘ ∅ ) ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o ( 𝐺 ‘ ∅ ) ) )
83 67 79 81 82 syl21anc ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ∅ ∈ ( ω ↑o ( 𝐺 ‘ ∅ ) ) )
84 0ex ⊢ ∅ ∈ V
85 7 seqom0g ⊢ ( ∅ ∈ V → ( 𝑇 ‘ ∅ ) = ∅ )
86 84 85 ax-mp ⊢ ( 𝑇 ‘ ∅ ) = ∅
87 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
88 6 seqom0g ⊢ ( ∅ ∈ V → ( 𝐻 ‘ ∅ ) = ∅ )
89 f1oeq2 ⊢ ( ( 𝐻 ‘ ∅ ) = ∅ → ( ∅ : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
90 84 88 89 mp2b ⊢ ( ∅ : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ ↔ ∅ : ∅ –1-1-onto→ ∅ )
91 87 90 mpbir ⊢ ∅ : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅
92 f1oeq1 ⊢ ( ( 𝑇 ‘ ∅ ) = ∅ → ( ( 𝑇 ‘ ∅ ) : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ ↔ ∅ : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ ) )
93 91 92 mpbiri ⊢ ( ( 𝑇 ‘ ∅ ) = ∅ → ( 𝑇 ‘ ∅ ) : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ )
94 86 93 mp1i ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ( 𝑇 ‘ ∅ ) : ( 𝐻 ‘ ∅ ) –1-1-onto→ ∅ )
95 1 64 65 4 5 6 7 8 9 66 83 94 cnfcomlem ⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ( 𝑇 ‘ suc ∅ ) : ( 𝐻 ‘ suc ∅ ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ ∅ ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) ) )
96 95 ex ⊢ ( 𝜑 → ( ∅ ∈ dom 𝐺 → ( 𝑇 ‘ suc ∅ ) : ( 𝐻 ‘ suc ∅ ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ ∅ ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) ) ) )
97 5 oicl ⊢ Ord dom 𝐺
98 ordtr ⊢ ( Ord dom 𝐺 → Tr dom 𝐺 )
99 97 98 ax-mp ⊢ Tr dom 𝐺
100 trsuc ⊢ ( ( Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺 ) → 𝑦 ∈ dom 𝐺 )
101 99 100 mpan ⊢ ( suc 𝑦 ∈ dom 𝐺 → 𝑦 ∈ dom 𝐺 )
102 101 imim1i ⊢ ( ( 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) → ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) )
103 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝐴 ∈ On )
104 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝐵 ∈ ( ω ↑o 𝐴 ) )
105 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → suc 𝑦 ∈ dom 𝐺 )
106 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝐴 ⊆ On )
107 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐹 supp ∅ ) ⊆ 𝐴 )
108 76 ffvelcdmi ⊢ ( suc 𝑦 ∈ dom 𝐺 → ( 𝐺 ‘ suc 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
109 108 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ suc 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
110 107 109 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ suc 𝑦 ) ∈ 𝐴 )
111 106 110 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ suc 𝑦 ) ∈ On )
112 eloni ⊢ ( ( 𝐺 ‘ suc 𝑦 ) ∈ On → Ord ( 𝐺 ‘ suc 𝑦 ) )
113 111 112 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → Ord ( 𝐺 ‘ suc 𝑦 ) )
114 vex ⊢ 𝑦 ∈ V
115 114 sucid ⊢ 𝑦 ∈ suc 𝑦
116 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
117 19 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
118 5 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
119 116 117 118 syl2anc ⊢ ( 𝜑 → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
121 101 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝑦 ∈ dom 𝐺 )
122 isorel ⊢ ( ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) ∧ ( 𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺 ) ) → ( 𝑦 E suc 𝑦 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ suc 𝑦 ) ) )
123 120 121 105 122 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝑦 E suc 𝑦 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ suc 𝑦 ) ) )
124 114 sucex ⊢ suc 𝑦 ∈ V
125 124 epeli ⊢ ( 𝑦 E suc 𝑦 ↔ 𝑦 ∈ suc 𝑦 )
126 fvex ⊢ ( 𝐺 ‘ suc 𝑦 ) ∈ V
127 126 epeli ⊢ ( ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ suc 𝑦 ) ↔ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ suc 𝑦 ) )
128 123 125 127 3bitr3g ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝑦 ∈ suc 𝑦 ↔ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ suc 𝑦 ) ) )
129 115 128 mpbii ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ suc 𝑦 ) )
130 ordsucss ⊢ ( Ord ( 𝐺 ‘ suc 𝑦 ) → ( ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ suc 𝑦 ) → suc ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) )
131 113 129 130 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → suc ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) )
132 76 ffvelcdmi ⊢ ( 𝑦 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
133 121 132 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
134 107 133 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 )
135 106 134 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ On )
136 onsuc ⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ On → suc ( 𝐺 ‘ 𝑦 ) ∈ On )
137 135 136 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → suc ( 𝐺 ‘ 𝑦 ) ∈ On )
138 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ω ∈ On )
139 80 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ∅ ∈ ω )
140 oewordi ⊢ ( ( ( suc ( 𝐺 ‘ 𝑦 ) ∈ On ∧ ( 𝐺 ‘ suc 𝑦 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( suc ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) → ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) ⊆ ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ) )
141 137 111 138 139 140 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( suc ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) → ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) ⊆ ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ) )
142 131 141 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) ⊆ ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) )
143 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → 𝐹 : 𝐴 ⟶ ω )
144 143 134 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ ω )
145 nnon ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ ω → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On )
146 144 145 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On )
147 oecl ⊢ ( ( ω ∈ On ∧ ( 𝐺 ‘ 𝑦 ) ∈ On ) → ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On )
148 138 135 147 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On )
149 oen0 ⊢ ( ( ( ω ∈ On ∧ ( 𝐺 ‘ 𝑦 ) ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) )
150 138 135 139 149 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ∅ ∈ ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) )
151 omord2 ⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ On ∧ ω ∈ On ∧ ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ∈ On ) ∧ ∅ ∈ ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ ω ↔ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ω ) ) )
152 146 138 148 150 151 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ ω ↔ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ω ) ) )
153 144 152 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ω ) )
154 oesuc ⊢ ( ( ω ∈ On ∧ ( 𝐺 ‘ 𝑦 ) ∈ On ) → ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ω ) )
155 138 135 154 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ω ) )
156 153 155 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ ( ω ↑o suc ( 𝐺 ‘ 𝑦 ) ) )
157 142 156 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) )
158 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
159 1 103 104 4 5 6 7 8 9 105 157 158 cnfcomlem ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) ) → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) )
160 159 exp32 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( suc 𝑦 ∈ dom 𝐺 → ( ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) )
161 160 a2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) → ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) )
162 102 161 syl5 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) → ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) )
163 162 expcom ⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( ( 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑦 ) : ( 𝐻 ‘ suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) → ( suc 𝑦 ∈ dom 𝐺 → ( 𝑇 ‘ suc suc 𝑦 ) : ( 𝐻 ‘ suc suc 𝑦 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ suc 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) ) )
164 43 53 63 96 163 finds2 ⊢ ( 𝑤 ∈ ω → ( 𝜑 → ( 𝑤 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝑤 ) : ( 𝐻 ‘ suc 𝑤 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝑤 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) ) )
165 33 164 vtoclga ⊢ ( 𝐼 ∈ ω → ( 𝜑 → ( 𝐼 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
166 22 165 mpcom ⊢ ( 𝜑 → ( 𝐼 ∈ dom 𝐺 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
167 10 166 mpd ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )