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 eqtrid ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝑀 = ( ( ω ↑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 eqtrid ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑥 ∈ 𝑀 ↦ ( 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 eqtrid ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → ( 𝑥 ∈ 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 eqtrid ⊢ ( ( 𝑘 = 𝑢 ∧ 𝑓 = 𝑣 ) → 𝐾 = ( ( 𝑦 ∈ ( ( ω ↑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 104 f1oeq1d ⊢ ( 𝜑 → ( ( 𝑇 ‘ 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 48 105 mpbird ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
107 13 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → ω ∈ On )
108 simpl ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → 𝐴 ∈ On )
109 simpr ⊢ ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) → 𝐹 ∈ 𝑆 )
110 8 oveq1i ⊢ ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 )
111 110 a1i ⊢ ( ( 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
112 111 mpoeq3ia ⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
113 eqid ⊢ ∅ = ∅
114 seqomeq12 ⊢ ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
115 112 113 114 mp2an ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
116 6 115 eqtri ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
117 1 107 108 5 109 116 cantnfsuc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ 𝐼 ∈ ω ) → ( 𝐻 ‘ suc 𝐼 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) )
118 2 21 42 117 syl21anc ⊢ ( 𝜑 → ( 𝐻 ‘ suc 𝐼 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) )
119 118 f1oeq2d ⊢ ( 𝜑 → ( ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( 𝑇 ‘ suc 𝐼 ) : ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) +o ( 𝐻 ‘ 𝐼 ) ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ) )
120 106 119 mpbird ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
121 sssucid ⊢ dom 𝐺 ⊆ suc dom 𝐺
122 121 10 sselid ⊢ ( 𝜑 → 𝐼 ∈ suc dom 𝐺 )
123 epelg ⊢ ( 𝐼 ∈ dom 𝐺 → ( 𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
124 10 123 syl ⊢ ( 𝜑 → ( 𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
125 124 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 E 𝐼 )
126 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
127 39 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
128 5 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
129 126 127 128 syl2anc ⊢ ( 𝜑 → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
131 5 oicl ⊢ Ord dom 𝐺
132 ordelss ⊢ ( ( Ord dom 𝐺 ∧ 𝐼 ∈ dom 𝐺 ) → 𝐼 ⊆ dom 𝐺 )
133 131 10 132 sylancr ⊢ ( 𝜑 → 𝐼 ⊆ dom 𝐺 )
134 133 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ dom 𝐺 )
135 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ dom 𝐺 )
136 isorel ⊢ ( ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) ∧ ( 𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺 ) ) → ( 𝑦 E 𝐼 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ) )
137 130 134 135 136 syl12anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑦 E 𝐼 ↔ ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ) )
138 125 137 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) )
139 fvex ⊢ ( 𝐺 ‘ 𝐼 ) ∈ V
140 139 epeli ⊢ ( ( 𝐺 ‘ 𝑦 ) E ( 𝐺 ‘ 𝐼 ) ↔ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
141 138 140 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
142 141 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) )
143 ffun ⊢ ( 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ ) → Fun 𝐺 )
144 26 143 ax-mp ⊢ Fun 𝐺
145 funimass4 ⊢ ( ( Fun 𝐺 ∧ 𝐼 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) ) )
146 144 133 145 sylancr ⊢ ( 𝜑 → ( ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐺 ‘ 𝐼 ) ) )
147 142 146 mpbird ⊢ ( 𝜑 → ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) )
148 13 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ω ∈ On )
149 simpll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐴 ∈ On )
150 simplr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐹 ∈ 𝑆 )
151 peano1 ⊢ ∅ ∈ ω
152 151 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ∅ ∈ ω )
153 simpr1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → 𝐼 ∈ suc dom 𝐺 )
154 simpr2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐺 ‘ 𝐼 ) ∈ On )
155 simpr3 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) )
156 1 148 149 5 150 116 152 153 154 155 cantnflt ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝐼 ∈ suc dom 𝐺 ∧ ( 𝐺 ‘ 𝐼 ) ∈ On ∧ ( 𝐺 “ 𝐼 ) ⊆ ( 𝐺 ‘ 𝐼 ) ) ) → ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
157 2 21 122 31 147 156 syl23anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) )
158 24 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
159 0ex ⊢ ∅ ∈ V
160 159 a1i ⊢ ( 𝜑 → ∅ ∈ V )
161 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V ) → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) ) )
162 158 2 160 161 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) ) )
163 simpr ⊢ ( ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ )
164 162 163 syl6bi ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐼 ) ∈ ( 𝐹 supp ∅ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
165 28 164 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ )
166 on0eln0 ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On → ( ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
167 36 166 syl ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ≠ ∅ ) )
168 165 167 mpbird ⊢ ( 𝜑 → ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) )
169 omword1 ⊢ ( ( ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∈ On ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ∈ On ) ∧ ∅ ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
170 33 36 168 169 syl21anc ⊢ ( 𝜑 → ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
171 oaabs2 ⊢ ( ( ( ( 𝐻 ‘ 𝐼 ) ∈ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ∧ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ∈ On ) ∧ ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ⊆ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) → ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
172 157 38 170 171 syl21anc ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) = ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )
173 172 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( 𝐻 ‘ 𝐼 ) +o ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) ↔ ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) ) )
174 120 173 mpbid ⊢ ( 𝜑 → ( 𝑇 ‘ suc 𝐼 ) : ( 𝐻 ‘ suc 𝐼 ) –1-1-onto→ ( ( ω ↑o ( 𝐺 ‘ 𝐼 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐼 ) ) ) )