Metamath Proof Explorer

Theorem fseqenlem1

Description: Lemma for fseqen . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses fseqenlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fseqenlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
fseqenlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
fseqenlem.g ⊢ 𝐺 = seqω ( ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) , { ⟨ ∅ , 𝐵 ⟩ } )
Assertion fseqenlem1 ( ( 𝜑 ∧ 𝐶 ∈ ω ) → ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 fseqenlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 fseqenlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 fseqenlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
4 fseqenlem.g ⊢ 𝐺 = seqω ( ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) , { ⟨ ∅ , 𝐵 ⟩ } )
5 fveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝐶 ) )
6 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝐶 ) → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
7 5 6 syl ⊢ ( 𝑦 = 𝐶 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
8 oveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m 𝐶 ) )
9 f1eq2 ⊢ ( ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m 𝐶 ) → ( ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 ) )
10 8 9 syl ⊢ ( 𝑦 = 𝐶 → ( ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 ) )
11 7 10 bitrd ⊢ ( 𝑦 = 𝐶 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 ) )
12 11 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( 𝜑 → ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) ↔ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 ) ) )
13 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ∅ ) )
14 snex ⊢ { ⟨ ∅ , 𝐵 ⟩ } ∈ V
15 4 seqom0g ⊢ ( { ⟨ ∅ , 𝐵 ⟩ } ∈ V → ( 𝐺 ‘ ∅ ) = { ⟨ ∅ , 𝐵 ⟩ } )
16 14 15 ax-mp ⊢ ( 𝐺 ‘ ∅ ) = { ⟨ ∅ , 𝐵 ⟩ }
17 13 16 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝐺 ‘ 𝑦 ) = { ⟨ ∅ , 𝐵 ⟩ } )
18 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑦 ) = { ⟨ ∅ , 𝐵 ⟩ } → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
19 17 18 syl ⊢ ( 𝑦 = ∅ → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
20 oveq2 ⊢ ( 𝑦 = ∅ → ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m ∅ ) )
21 f1eq2 ⊢ ( ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m ∅ ) → ( { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 ) )
22 20 21 syl ⊢ ( 𝑦 = ∅ → ( { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 ) )
23 19 22 bitrd ⊢ ( 𝑦 = ∅ → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 ) )
24 fveq2 ⊢ ( 𝑦 = 𝑚 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑚 ) )
25 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑚 ) → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
26 24 25 syl ⊢ ( 𝑦 = 𝑚 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
27 oveq2 ⊢ ( 𝑦 = 𝑚 → ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m 𝑚 ) )
28 f1eq2 ⊢ ( ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m 𝑚 ) → ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) )
29 27 28 syl ⊢ ( 𝑦 = 𝑚 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) )
30 26 29 bitrd ⊢ ( 𝑦 = 𝑚 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) )
31 fveq2 ⊢ ( 𝑦 = suc 𝑚 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ suc 𝑚 ) )
32 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ suc 𝑚 ) → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
33 31 32 syl ⊢ ( 𝑦 = suc 𝑚 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
34 oveq2 ⊢ ( 𝑦 = suc 𝑚 → ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m suc 𝑚 ) )
35 f1eq2 ⊢ ( ( 𝐴 ↑m 𝑦 ) = ( 𝐴 ↑m suc 𝑚 ) → ( ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ) )
36 34 35 syl ⊢ ( 𝑦 = suc 𝑚 → ( ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ) )
37 33 36 bitrd ⊢ ( 𝑦 = suc 𝑚 → ( ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ↔ ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ) )
38 0ex ⊢ ∅ ∈ V
39 f1osng ⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝐴 ) → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1-onto→ { 𝐵 } )
40 38 2 39 sylancr ⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1-onto→ { 𝐵 } )
41 f1of1 ⊢ ( { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1-onto→ { 𝐵 } → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ { 𝐵 } )
42 40 41 syl ⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ { 𝐵 } )
43 2 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝐴 )
44 f1ss ⊢ ( ( { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ { 𝐵 } ∧ { 𝐵 } ⊆ 𝐴 ) → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ 𝐴 )
45 42 43 44 syl2anc ⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ 𝐴 )
46 map0e ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m ∅ ) = 1o )
47 1 46 syl ⊢ ( 𝜑 → ( 𝐴 ↑m ∅ ) = 1o )
48 df1o2 ⊢ 1o = { ∅ }
49 47 48 eqtrdi ⊢ ( 𝜑 → ( 𝐴 ↑m ∅ ) = { ∅ } )
50 f1eq2 ⊢ ( ( 𝐴 ↑m ∅ ) = { ∅ } → ( { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ 𝐴 ) )
51 49 50 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 ↔ { ⟨ ∅ , 𝐵 ⟩ } : { ∅ } –1-1→ 𝐴 ) )
52 45 51 mpbird ⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ } : ( 𝐴 ↑m ∅ ) –1-1→ 𝐴 )
53 4 seqomsuc ⊢ ( 𝑚 ∈ ω → ( 𝐺 ‘ suc 𝑚 ) = ( 𝑚 ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) ( 𝐺 ‘ 𝑚 ) ) )
54 53 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ( 𝐺 ‘ suc 𝑚 ) = ( 𝑚 ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) ( 𝐺 ‘ 𝑚 ) ) )
55 vex ⊢ 𝑚 ∈ V
56 fvex ⊢ ( 𝐺 ‘ 𝑚 ) ∈ V
57 reseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ↾ 𝑎 ) = ( 𝑧 ↾ 𝑎 ) )
58 57 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) = ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) )
59 fveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑎 ) )
60 58 59 oveq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) = ( ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) 𝐹 ( 𝑧 ‘ 𝑎 ) ) )
61 60 cbvmptv ⊢ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) 𝐹 ( 𝑧 ‘ 𝑎 ) ) )
62 suceq ⊢ ( 𝑎 = 𝑚 → suc 𝑎 = suc 𝑚 )
63 62 adantr ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → suc 𝑎 = suc 𝑚 )
64 63 oveq2d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝐴 ↑m suc 𝑎 ) = ( 𝐴 ↑m suc 𝑚 ) )
65 simpr ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → 𝑏 = ( 𝐺 ‘ 𝑚 ) )
66 reseq2 ⊢ ( 𝑎 = 𝑚 → ( 𝑧 ↾ 𝑎 ) = ( 𝑧 ↾ 𝑚 ) )
67 66 adantr ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝑧 ↾ 𝑎 ) = ( 𝑧 ↾ 𝑚 ) )
68 65 67 fveq12d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) )
69 simpl ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → 𝑎 = 𝑚 )
70 69 fveq2d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑚 ) )
71 68 70 oveq12d ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) 𝐹 ( 𝑧 ‘ 𝑎 ) ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) )
72 64 71 mpteq12dv ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑧 ↾ 𝑎 ) ) 𝐹 ( 𝑧 ‘ 𝑎 ) ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) )
73 61 72 eqtrid ⊢ ( ( 𝑎 = 𝑚 ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) )
74 nfcv ⊢ Ⅎ 𝑎 ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) )
75 nfcv ⊢ Ⅎ 𝑏 ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) )
76 nfcv ⊢ Ⅎ 𝑛 ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) )
77 nfcv ⊢ Ⅎ 𝑓 ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) )
78 suceq ⊢ ( 𝑛 = 𝑎 → suc 𝑛 = suc 𝑎 )
79 78 adantr ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → suc 𝑛 = suc 𝑎 )
80 79 oveq2d ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( 𝐴 ↑m suc 𝑛 ) = ( 𝐴 ↑m suc 𝑎 ) )
81 simpr ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → 𝑓 = 𝑏 )
82 reseq2 ⊢ ( 𝑛 = 𝑎 → ( 𝑥 ↾ 𝑛 ) = ( 𝑥 ↾ 𝑎 ) )
83 82 adantr ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( 𝑥 ↾ 𝑛 ) = ( 𝑥 ↾ 𝑎 ) )
84 81 83 fveq12d ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) = ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) )
85 simpl ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → 𝑛 = 𝑎 )
86 85 fveq2d ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( 𝑥 ‘ 𝑛 ) = ( 𝑥 ‘ 𝑎 ) )
87 84 86 oveq12d ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) = ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) )
88 80 87 mpteq12dv ⊢ ( ( 𝑛 = 𝑎 ∧ 𝑓 = 𝑏 ) → ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) ) )
89 74 75 76 77 88 cbvmpo ⊢ ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑎 ) ↦ ( ( 𝑏 ‘ ( 𝑥 ↾ 𝑎 ) ) 𝐹 ( 𝑥 ‘ 𝑎 ) ) ) )
90 ovex ⊢ ( 𝐴 ↑m suc 𝑚 ) ∈ V
91 90 mptex ⊢ ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ∈ V
92 73 89 91 ovmpoa ⊢ ( ( 𝑚 ∈ V ∧ ( 𝐺 ‘ 𝑚 ) ∈ V ) → ( 𝑚 ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) ( 𝐺 ‘ 𝑚 ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) )
93 55 56 92 mp2an ⊢ ( 𝑚 ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) ( 𝐺 ‘ 𝑚 ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) )
94 54 93 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ( 𝐺 ‘ suc 𝑚 ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) )
95 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
96 f1of ⊢ ( 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 → 𝐹 : ( 𝐴 × 𝐴 ) ⟶ 𝐴 )
97 95 96 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → 𝐹 : ( 𝐴 × 𝐴 ) ⟶ 𝐴 )
98 f1f ⊢ ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) ⟶ 𝐴 )
99 98 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) ⟶ 𝐴 )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) ⟶ 𝐴 )
101 elmapi ⊢ ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) → 𝑧 : suc 𝑚 ⟶ 𝐴 )
102 101 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → 𝑧 : suc 𝑚 ⟶ 𝐴 )
103 sssucid ⊢ 𝑚 ⊆ suc 𝑚
104 fssres ⊢ ( ( 𝑧 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ⊆ suc 𝑚 ) → ( 𝑧 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
105 102 103 104 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( 𝑧 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
106 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → 𝐴 ∈ 𝑉 )
107 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V ) → ( ( 𝑧 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑧 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
108 106 55 107 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( ( 𝑧 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑧 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
109 105 108 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( 𝑧 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) )
110 100 109 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) ∈ 𝐴 )
111 55 sucid ⊢ 𝑚 ∈ suc 𝑚
112 ffvelrn ⊢ ( ( 𝑧 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ suc 𝑚 ) → ( 𝑧 ‘ 𝑚 ) ∈ 𝐴 )
113 102 111 112 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( 𝑧 ‘ 𝑚 ) ∈ 𝐴 )
114 97 110 113 fovrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ) → ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ∈ 𝐴 )
115 94 114 fmpt3d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) ⟶ 𝐴 )
116 elmapi ⊢ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) → 𝑎 : suc 𝑚 ⟶ 𝐴 )
117 116 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝑎 : suc 𝑚 ⟶ 𝐴 )
118 117 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝑎 Fn suc 𝑚 )
119 elmapi ⊢ ( 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) → 𝑏 : suc 𝑚 ⟶ 𝐴 )
120 119 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝑏 : suc 𝑚 ⟶ 𝐴 )
121 120 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝑏 Fn suc 𝑚 )
122 103 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝑚 ⊆ suc 𝑚 )
123 fvreseq ⊢ ( ( ( 𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚 ) ∧ 𝑚 ⊆ suc 𝑚 ) → ( ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
124 118 121 122 123 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
125 fveq2 ⊢ ( 𝑥 = 𝑚 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑚 ) )
126 fveq2 ⊢ ( 𝑥 = 𝑚 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑚 ) )
127 125 126 eqeq12d ⊢ ( 𝑥 = 𝑚 → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) )
128 55 127 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) )
129 128 bicomi ⊢ ( ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ↔ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
130 129 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ↔ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
131 124 130 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) ↔ ( ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
132 94 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝐺 ‘ suc 𝑚 ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) )
133 132 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑎 ) )
134 reseq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ↾ 𝑚 ) = ( 𝑎 ↾ 𝑚 ) )
135 134 fveq2d ⊢ ( 𝑧 = 𝑎 → ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) )
136 fveq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ‘ 𝑚 ) = ( 𝑎 ‘ 𝑚 ) )
137 135 136 oveq12d ⊢ ( 𝑧 = 𝑎 → ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) )
138 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) = ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) )
139 ovex ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) ∈ V
140 137 138 139 fvmpt ⊢ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) → ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑎 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) )
141 140 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑎 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) )
142 133 141 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) )
143 df-ov ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) 𝐹 ( 𝑎 ‘ 𝑚 ) ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ )
144 142 143 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ) )
145 132 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑏 ) )
146 reseq1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) )
147 146 fveq2d ⊢ ( 𝑧 = 𝑏 → ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) )
148 fveq1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) )
149 147 148 oveq12d ⊢ ( 𝑧 = 𝑏 → ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) )
150 ovex ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) ∈ V
151 149 138 150 fvmpt ⊢ ( 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) → ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑏 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) )
152 151 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑧 ∈ ( 𝐴 ↑m suc 𝑚 ) ↦ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑧 ↾ 𝑚 ) ) 𝐹 ( 𝑧 ‘ 𝑚 ) ) ) ‘ 𝑏 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) )
153 145 152 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) = ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) )
154 df-ov ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) 𝐹 ( 𝑏 ‘ 𝑚 ) ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ )
155 153 154 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) )
156 144 155 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) ↔ ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) ) )
157 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
158 f1of1 ⊢ ( 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 → 𝐹 : ( 𝐴 × 𝐴 ) –1-1→ 𝐴 )
159 157 158 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝐹 : ( 𝐴 × 𝐴 ) –1-1→ 𝐴 )
160 99 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) ⟶ 𝐴 )
161 fssres ⊢ ( ( 𝑎 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ⊆ suc 𝑚 ) → ( 𝑎 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
162 117 103 161 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑎 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
163 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → 𝐴 ∈ 𝑉 )
164 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V ) → ( ( 𝑎 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑎 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
165 163 55 164 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑎 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑎 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
166 162 165 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑎 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) )
167 160 166 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) ∈ 𝐴 )
168 ffvelrn ⊢ ( ( 𝑎 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ suc 𝑚 ) → ( 𝑎 ‘ 𝑚 ) ∈ 𝐴 )
169 117 111 168 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑎 ‘ 𝑚 ) ∈ 𝐴 )
170 167 169 opelxpd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ∈ ( 𝐴 × 𝐴 ) )
171 fssres ⊢ ( ( 𝑏 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ⊆ suc 𝑚 ) → ( 𝑏 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
172 120 103 171 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑏 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 )
173 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V ) → ( ( 𝑏 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑏 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
174 163 55 173 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝑏 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ↔ ( 𝑏 ↾ 𝑚 ) : 𝑚 ⟶ 𝐴 ) )
175 172 174 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑏 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) )
176 160 175 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ∈ 𝐴 )
177 ffvelrn ⊢ ( ( 𝑏 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ suc 𝑚 ) → ( 𝑏 ‘ 𝑚 ) ∈ 𝐴 )
178 120 111 177 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑏 ‘ 𝑚 ) ∈ 𝐴 )
179 176 178 opelxpd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ∈ ( 𝐴 × 𝐴 ) )
180 f1fveq ⊢ ( ( 𝐹 : ( 𝐴 × 𝐴 ) –1-1→ 𝐴 ∧ ( ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ∈ ( 𝐴 × 𝐴 ) ∧ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ∈ ( 𝐴 × 𝐴 ) ) ) → ( ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) ↔ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) )
181 159 170 179 180 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) ↔ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) )
182 fvex ⊢ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) ∈ V
183 fvex ⊢ ( 𝑎 ‘ 𝑚 ) ∈ V
184 182 183 opth ⊢ ( ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ↔ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) )
185 181 184 bitrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) , ( 𝑎 ‘ 𝑚 ) ⟩ ) = ( 𝐹 ‘ ⟨ ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) , ( 𝑏 ‘ 𝑚 ) ⟩ ) ↔ ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) ) )
186 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 )
187 f1fveq ⊢ ( ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ∧ ( ( 𝑎 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ∧ ( 𝑏 ↾ 𝑚 ) ∈ ( 𝐴 ↑m 𝑚 ) ) ) → ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ↔ ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ) )
188 186 166 175 187 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ↔ ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ) )
189 188 anbi1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑎 ↾ 𝑚 ) ) = ( ( 𝐺 ‘ 𝑚 ) ‘ ( 𝑏 ↾ 𝑚 ) ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) ↔ ( ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) ) )
190 156 185 189 3bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) ↔ ( ( 𝑎 ↾ 𝑚 ) = ( 𝑏 ↾ 𝑚 ) ∧ ( 𝑎 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑚 ) ) ) )
191 eqfnfv ⊢ ( ( 𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚 ) → ( 𝑎 = 𝑏 ↔ ∀ 𝑥 ∈ suc 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
192 118 121 191 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑎 = 𝑏 ↔ ∀ 𝑥 ∈ suc 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
193 df-suc ⊢ suc 𝑚 = ( 𝑚 ∪ { 𝑚 } )
194 193 raleqi ⊢ ( ∀ 𝑥 ∈ suc 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑚 } ) ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
195 ralunb ⊢ ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑚 } ) ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
196 194 195 bitri ⊢ ( ∀ 𝑥 ∈ suc 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
197 192 196 bitrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( 𝑎 = 𝑏 ↔ ( ∀ 𝑥 ∈ 𝑚 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ { 𝑚 } ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
198 131 190 197 3bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
199 198 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) ∧ ( 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∧ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ) ) → ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
200 199 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ∀ 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∀ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
201 dff13 ⊢ ( ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ↔ ( ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) ⟶ 𝐴 ∧ ∀ 𝑎 ∈ ( 𝐴 ↑m suc 𝑚 ) ∀ 𝑏 ∈ ( 𝐴 ↑m suc 𝑚 ) ( ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ suc 𝑚 ) ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
202 115 200 201 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ω ∧ ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 ) ) → ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 )
203 202 expr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ω ) → ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 → ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ) )
204 203 expcom ⊢ ( 𝑚 ∈ ω → ( 𝜑 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝐴 ↑m 𝑚 ) –1-1→ 𝐴 → ( 𝐺 ‘ suc 𝑚 ) : ( 𝐴 ↑m suc 𝑚 ) –1-1→ 𝐴 ) ) )
205 23 30 37 52 204 finds2 ⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( 𝐺 ‘ 𝑦 ) : ( 𝐴 ↑m 𝑦 ) –1-1→ 𝐴 ) )
206 12 205 vtoclga ⊢ ( 𝐶 ∈ ω → ( 𝜑 → ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 ) )
207 206 impcom ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ω ) → ( 𝐺 ‘ 𝐶 ) : ( 𝐴 ↑m 𝐶 ) –1-1→ 𝐴 )