Metamath Proof Explorer

Theorem cnfcomlem

Description: Lemma for cnfcom . (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 𝐺 )
cnfcom.2 ⊢ ( 𝜑 → 𝑂 ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
cnfcom.3 ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐼 ) : ( 𝐻 ‘ 𝐼 ) –1-1-onto→ 𝑂 )
Assertion cnfcomlem ( 𝜑 → ( 𝑇 ‘ 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 cnfcom.2 ⊢ ( 𝜑 → 𝑂 ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
12 cnfcom.3 ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐼 ) : ( 𝐻 ‘ 𝐼 ) –1-1-onto→ 𝑂 )
13 omelon ⊢ ω ∈ On
14 suppssdm ⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
15 13 a1i ⊢ ( 𝜑 → ω ∈ On )
16 1 15 2 cantnff1o ⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
17 f1ocnv ⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
18 f1of ⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
19 16 17 18 3syl ⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
20 19 3 ffvelrnd ⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
21 4 20 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
22 1 15 2 cantnfs ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
23 21 22 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) )
24 23 simpld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ω )
25 14 24 fssdm ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐴 )
26 5 oif ⊢ 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ )
27 26 ffvelrni ⊢ ( 𝐼 ∈ dom 𝐺 → ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) )
28 10 27 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) )
29 25 28 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 )
30 onelon ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝐼 ) ∈ On )
31 2 29 30 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ On )
32 oecl ⊢ ( ( ω ∈ On ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ) → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∈ On )
33 13 31 32 sylancr ⊢ ( 𝜑 → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∈ On )
34 24 29 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ ω )
35 nnon ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ ω → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On )
36 34 35 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On )
37 omcl ⊢ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∈ On ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On ) → ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ On )
38 33 36 37 syl2anc ⊢ ( 𝜑 → ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ On )
39 1 15 2 5 21 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
40 39 simprd ⊢ ( 𝜑 → dom 𝐺 ∈ ω )
41 elnn ⊢ ( ( 𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω ) → 𝐼 ∈ ω )
42 10 40 41 syl2anc ⊢ ( 𝜑 → 𝐼 ∈ ω )
43 6 cantnfvalf ⊢ 𝐻 : ω ⟶ On
44 43 ffvelrni ⊢ ( 𝐼 ∈ ω → ( 𝐻 ‘ 𝐼 ) ∈ On )
45 42 44 syl ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐼 ) ∈ On )
46 eqid ⊢ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) )
47 46 oacomf1o ⊢ ( ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ On ∧ ( 𝐻 ‘ 𝐼 ) ∈ On ) → ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
48 38 45 47 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
49 7 seqomsuc ⊢ ( 𝐼 ∈ ω → ( 𝑇 ‘ suc 𝐼 ) = ( 𝐼 ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) ( 𝑇 ‘ 𝐼 ) ) )
50 42 49 syl ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) = ( 𝐼 ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) ( 𝑇 ‘ 𝐼 ) ) )
51 nfcv ⊢ Ⅎ 𝑢 𝐾
52 nfcv ⊢ Ⅎ 𝑣 𝐾
53 nfcv ⊢ Ⅎ 𝑘 ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) )
54 nfcv ⊢ Ⅎ 𝑓 ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) )
55 oveq2 ⊢ ( 𝑥 = 𝑦 → ( dom 𝑓 +o 𝑥 ) = ( dom 𝑓 +o 𝑦 ) )
56 55 cbvmptv ⊢ ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) = ( 𝑦 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑦 ) )
57 simpl ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝑘 = 𝑢 )
58 57 fveq2d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑢 ) )
59 58 oveq2d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) = ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) )
60 58 fveq2d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) )
61 59 60 oveq12d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) )
62 8 61 syl5eq ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝑀 = ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) )
63 simpr ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝑓 = 𝑣 )
64 63 dmeqd ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → dom 𝑓 = dom 𝑣 )
65 64 oveq1d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( dom 𝑓 +o 𝑦 ) = ( dom 𝑣 +o 𝑦 ) )
66 62 65 mpteq12dv ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑦 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑦 ) ) = ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) )
67 56 66 syl5eq ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) = ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) )
68 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑀 +o 𝑥 ) = ( 𝑀 +o 𝑦 ) )
69 68 cbvmptv ⊢ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) = ( 𝑦 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑦 ) )
70 62 oveq1d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑀 +o 𝑦 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) )
71 64 70 mpteq12dv ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑦 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑦 ) ) = ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) )
72 69 71 syl5eq ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) = ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) )
73 72 cnveqd ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) = ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) )
74 67 73 uneq12d ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) ) )
75 9 74 syl5eq ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝐾 = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) ) )
76 51 52 53 54 75 cbvmpo ⊢ ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) ) )
77 76 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) ) ) )
78 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → 𝑢 = 𝐼 )
79 78 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝐼 ) )
80 79 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) = ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
81 79 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) )
82 80 81 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
83 simpr ⊢ ( ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) → 𝑣 = ( 𝑇 ‘ 𝐼 ) )
84 83 dmeqd ⊢ ( ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) → dom 𝑣 = dom ( 𝑇 ‘ 𝐼 ) )
85 f1odm ⊢ ( ( 𝑇 ‘ 𝐼 ) : ( 𝐻 ‘ 𝐼 ) –1-1-onto→ 𝑂 → dom ( 𝑇 ‘ 𝐼 ) = ( 𝐻 ‘ 𝐼 ) )
86 12 85 syl ⊢ ( 𝜑 → dom ( 𝑇 ‘ 𝐼 ) = ( 𝐻 ‘ 𝐼 ) )
87 84 86 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → dom 𝑣 = ( 𝐻 ‘ 𝐼 ) )
88 87 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( dom 𝑣 +o 𝑦 ) = ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) )
89 82 88 mpteq12dv ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) = ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) )
90 82 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) )
91 87 90 mpteq12dv ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) = ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) )
92 91 cnveqd ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) = ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) )
93 89 92 uneq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝐼 ∧ 𝑣 = ( 𝑇 ‘ 𝐼 ) ) ) → ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ↦ ( dom 𝑣 +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ dom 𝑣 ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑦 ) ) ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) )
94 10 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
95 fvexd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝐼 ) ∈ V )
96 ovex ⊢ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ V
97 96 mptex ⊢ ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∈ V
98 fvex ⊢ ( 𝐻 ‘ 𝐼 ) ∈ V
99 98 mptex ⊢ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ∈ V
100 99 cnvex ⊢ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ∈ V
101 97 100 unex ⊢ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) ∈ V
102 101 a1i ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) ∈ V )
103 77 93 94 95 102 ovmpod ⊢ ( 𝜑 → ( 𝐼 ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) ( 𝑇 ‘ 𝐼 ) ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) )
104 50 103 eqtrd ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) )
105 f1oeq1 ⊢ ( ( 𝑇 ‘ suc 𝐼 ) = ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) → ( ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
106 104 105 syl ⊢ ( 𝜑 → ( ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( ( 𝑦 ∈ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ↦ ( ( 𝐻 ‘ 𝐼 ) +o 𝑦 ) ) ∪ ◡ ( 𝑦 ∈ ( 𝐻 ‘ 𝐼 ) ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o 𝑦 ) ) ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
107 48 106 mpbird ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
108 13 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → ω ∈ On )
109 simpl ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → 𝐴 ∈ On )
110 simpr ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → 𝐹 ∈ 𝑆 )
111 8 oveq1i ⊢ ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 )
112 111 a1i ⊢ ( ( 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
113 112 mpoeq3ia ⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
114 eqid ⊢ ∅ = ∅
115 seqomeq12 ⊢ ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
116 113 114 115 mp2an ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
117 6 116 eqtri ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
118 1 108 109 5 110 117 cantnfsuc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ 𝐼 ∈ ω ) → ( 𝐻 ‘ suc 𝐼 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) )
119 2 21 42 118 syl21anc ⊢ ( 𝜑 → ( 𝐻 ‘ suc 𝐼 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) )
120 119 f1oeq2d ⊢ ( 𝜑 → ( ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
121 107 120 mpbird ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
122 sssucid ⊢ dom 𝐺 ⊆ suc dom 𝐺
123 122 10 sseldi ⊢ ( 𝜑 → 𝐼 ∈ suc dom 𝐺 )
124 epelg ⊢ ( 𝐼 ∈ dom 𝐺 → ( 𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
125 10 124 syl ⊢ ( 𝜑 → ( 𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
126 125 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 E 𝐼 )
127 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
128 39 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
129 5 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
130 127 128 129 syl2anc ⊢ ( 𝜑 → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
132 5 oicl ⊢ Ord dom 𝐺
133 ordelss ⊢ ( ( Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺 ) → 𝐼 ⊆ dom 𝐺 )
134 132 10 133 sylancr ⊢ ( 𝜑 → 𝐼 ⊆ dom 𝐺 )
135 134 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ dom 𝐺 )
136 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ dom 𝐺 )
137 isorel ⊢ ( ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) ∧ ( 𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺 ) ) → ( 𝑦 E 𝐼 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ) )
138 131 135 136 137 syl12anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑦 E 𝐼 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ) )
139 126 138 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) )
140 fvex ⊢ ( 𝐺 ‘ 𝐼 ) ∈ V
141 140 epeli ⊢ ( ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ↔ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
142 139 141 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
143 142 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
144 ffun ⊢ ( 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ ) → Fun 𝐺 )
145 26 144 ax-mp ⊢ Fun 𝐺
146 funimass4 ⊢ ( ( Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) ) )
147 145 134 146 sylancr ⊢ ( 𝜑 → ( ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) ) )
148 143 147 mpbird ⊢ ( 𝜑 → ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) )
149 13 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ω ∈ On )
150 simpll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐴 ∈ On )
151 simplr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐹 ∈ 𝑆 )
152 peano1 ⊢ ∅ ∈ ω
153 152 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ∅ ∈ ω )
154 simpr1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐼 ∈ suc dom 𝐺 )
155 simpr2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐺 ‘ 𝐼 ) ∈ On )
156 simpr3 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) )
157 1 149 150 5 151 117 153 154 155 156 cantnflt ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
158 2 21 123 31 148 157 syl23anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
159 24 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
160 0ex ⊢ ∅ ∈ V
161 160 a1i ⊢ ( 𝜑 → ∅ ∈ V )
162 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V ) → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) ) )
163 159 2 161 162 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) ) )
164 simpr ⊢ ( ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ )
165 163 164 syl6bi ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
166 28 165 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ )
167 on0eln0 ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On → ( ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
168 36 167 syl ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
169 166 168 mpbird ⊢ ( 𝜑 → ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) )
170 omword1 ⊢ ( ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∈ On ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On ) ∧ ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
171 33 36 169 170 syl21anc ⊢ ( 𝜑 → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
172 oaabs2 ⊢ ( ( ( ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∧ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ On ) ∧ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) → ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
173 158 38 171 172 syl21anc ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
174 173 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
175 121 174 mpbid ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )