Metamath Proof Explorer

Theorem sdclem2

Description: Lemma for sdc . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses sdc.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
sdc.2 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
sdc.3 ⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
sdc.4 ⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
sdc.5 ⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
sdc.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sdc.7 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sdc.8 ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
sdc.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
sdc.10 ⊢ 𝐽 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) }
sdc.11 ⊢ 𝐹 = ( 𝑤 ∈ 𝑍 , 𝑥 ∈ 𝐽 ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
sdc.12 ⊢ Ⅎ 𝑘 𝜑
sdc.13 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝐽 )
sdc.14 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
sdc.15 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) ∈ ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) )
Assertion sdclem2 ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )

Proof

Step Hyp Ref Expression
1 sdc.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 sdc.2 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
3 sdc.3 ⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
4 sdc.4 ⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
5 sdc.5 ⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
6 sdc.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 sdc.7 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 sdc.8 ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
9 sdc.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
10 sdc.10 ⊢ 𝐽 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) }
11 sdc.11 ⊢ 𝐹 = ( 𝑤 ∈ 𝑍 , 𝑥 ∈ 𝐽 ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
12 sdc.12 ⊢ Ⅎ 𝑘 𝜑
13 sdc.13 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝐽 )
14 sdc.14 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
15 sdc.15 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) ∈ ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) )
16 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐽 )
17 10 eleq2i ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐽 ↔ ( 𝐺 ‘ 𝑘 ) ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } )
18 nfcv ⊢ Ⅎ 𝑔 𝑍
19 nfv ⊢ Ⅎ 𝑔 ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴
20 nfsbc1v ⊢ Ⅎ 𝑔 [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓
21 19 20 nfan ⊢ Ⅎ 𝑔 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 )
22 18 21 nfrexw ⊢ Ⅎ 𝑔 ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 )
23 fvex ⊢ ( 𝐺 ‘ 𝑘 ) ∈ V
24 feq1 ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑘 ) → ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ) )
25 sbceq1a ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑘 ) → ( 𝜓 ↔ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) )
26 24 25 anbi12d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) ) )
27 26 rexbidv ⊢ ( 𝑔 = ( 𝐺 ‘ 𝑘 ) → ( ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) ) )
28 22 23 27 elabf ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↔ ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) )
29 17 28 bitri ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐽 ↔ ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) )
30 16 29 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) )
31 fdm ⊢ ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 → dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑛 ) )
32 31 adantr ⊢ ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) → dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑛 ) )
33 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑀 ) )
34 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑀 ) )
35 34 mpteq1d ⊢ ( 𝑥 = 𝑀 → ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
36 33 35 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
37 36 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
38 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑤 ) )
39 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑤 ) )
40 39 mpteq1d ⊢ ( 𝑥 = 𝑤 → ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
41 38 40 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
42 41 imbi2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 → ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
43 fveq2 ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝑤 + 1 ) ) )
44 oveq2 ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... ( 𝑤 + 1 ) ) )
45 44 mpteq1d ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
46 43 45 eqeq12d ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
47 46 imbi2d ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ( 𝜑 → ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
48 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
49 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑘 ) )
50 49 mpteq1d ⊢ ( 𝑥 = 𝑘 → ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
51 48 50 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑘 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
52 51 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝐺 ‘ 𝑥 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑥 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ( 𝐺 ‘ 𝑘 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
53 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) )
54 id ⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 )
55 53 54 fveq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) = ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) )
56 eqid ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) )
57 fvex ⊢ ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) ∈ V
58 55 56 57 fvmpt ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) )
60 elfz1eq ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → 𝑘 = 𝑀 )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → 𝑘 = 𝑀 )
62 61 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑀 ) )
63 62 fveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) )
64 59 63 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) )
65 64 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) ) )
66 12 65 ralrimi ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) )
67 14 ffnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) Fn ( 𝑀 ... 𝑀 ) )
68 fvex ⊢ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ∈ V
69 68 56 fnmpti ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... 𝑀 )
70 eqfnfv ⊢ ( ( ( 𝐺 ‘ 𝑀 ) Fn ( 𝑀 ... 𝑀 ) ∧ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) ) )
71 67 69 70 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑘 ) ) )
72 66 71 mpbird ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
73 72 a1i ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
74 1 eleq2i ⊢ ( 𝑤 ∈ 𝑍 ↔ 𝑤 ∈ ( ℤ≥ ‘ 𝑀 ) )
75 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝐽 )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑍 )
77 3simpa ⊢ ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) → ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) )
78 77 reximi ⊢ ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) → ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) )
79 78 ss2abi ⊢ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) }
80 1 fvexi ⊢ 𝑍 ∈ V
81 nfv ⊢ Ⅎ 𝑘 𝑤 ∈ 𝑍
82 12 81 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑤 ∈ 𝑍 )
83 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝐴 ∈ 𝑉 )
84 simpl ⊢ ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) → ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 )
85 ovex ⊢ ( 𝑀 ... ( 𝑘 + 1 ) ) ∈ V
86 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑀 ... ( 𝑘 + 1 ) ) ∈ V ) → ( ℎ ∈ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ↔ ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) )
87 85 86 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ( ℎ ∈ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ↔ ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) )
88 84 87 imbitrrid ⊢ ( 𝐴 ∈ 𝑉 → ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) → ℎ ∈ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ) )
89 88 abssdv ⊢ ( 𝐴 ∈ 𝑉 → { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ⊆ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) )
90 83 89 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ⊆ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) )
91 ovex ⊢ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ∈ V
92 ssexg ⊢ ( ( { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ⊆ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ∧ ( 𝐴 ↑m ( 𝑀 ... ( 𝑘 + 1 ) ) ) ∈ V ) → { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V )
93 90 91 92 sylancl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V )
94 93 a1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑘 ∈ 𝑍 → { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V ) )
95 82 94 ralrimi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ∀ 𝑘 ∈ 𝑍 { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V )
96 abrexex2g ⊢ ( ( 𝑍 ∈ V ∧ ∀ 𝑘 ∈ 𝑍 { ℎ ∣ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V )
97 80 95 96 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V )
98 ssexg ⊢ ( ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ⊆ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∧ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ∈ V ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V )
99 79 97 98 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V )
100 eqeq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) )
101 100 3anbi2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
102 101 rexbidv ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
103 102 abbidv ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
104 103 eleq1d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V ↔ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V ) )
105 oveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( 𝑤 𝐹 𝑥 ) = ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) )
106 105 103 eqeq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ↔ ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) )
107 104 106 imbi12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ↔ ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ) )
108 107 imbi2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑤 ∈ 𝑍 → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ) ↔ ( 𝑤 ∈ 𝑍 → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ) ) )
109 11 ovmpt4g ⊢ ( ( 𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V ) → ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
110 109 3com12 ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V ) → ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
111 110 3exp ⊢ ( 𝑥 ∈ 𝐽 → ( 𝑤 ∈ 𝑍 → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 𝑥 ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ) )
112 108 111 vtoclga ⊢ ( ( 𝐺 ‘ 𝑤 ) ∈ 𝐽 → ( 𝑤 ∈ 𝑍 → ( { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ∈ V → ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) ) )
113 75 76 99 112 syl3c ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
114 113 79 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑤 𝐹 ( 𝐺 ‘ 𝑤 ) ) ⊆ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } )
115 114 15 sseldd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) ∈ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } )
116 fvex ⊢ ( 𝐺 ‘ ( 𝑤 + 1 ) ) ∈ V
117 feq1 ⊢ ( ℎ = ( 𝐺 ‘ ( 𝑤 + 1 ) ) → ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ↔ ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) )
118 reseq1 ⊢ ( ℎ = ( 𝐺 ‘ ( 𝑤 + 1 ) ) → ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) )
119 118 eqeq2d ⊢ ( ℎ = ( 𝐺 ‘ ( 𝑤 + 1 ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) )
120 117 119 anbi12d ⊢ ( ℎ = ( 𝐺 ‘ ( 𝑤 + 1 ) ) → ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) ↔ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) ) )
121 120 rexbidv ⊢ ( ℎ = ( 𝐺 ‘ ( 𝑤 + 1 ) ) → ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 𝑍 ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) ) )
122 116 121 elab ⊢ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ∈ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) } ↔ ∃ 𝑘 ∈ 𝑍 ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) )
123 115 122 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ∃ 𝑘 ∈ 𝑍 ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) )
124 nfv ⊢ Ⅎ 𝑘 ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
125 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 )
126 fzssp1 ⊢ ( 𝑀 ... 𝑘 ) ⊆ ( 𝑀 ... ( 𝑘 + 1 ) )
127 fssres ⊢ ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝑀 ... 𝑘 ) ⊆ ( 𝑀 ... ( 𝑘 + 1 ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 )
128 125 126 127 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 )
129 128 fdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → dom ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑀 ... 𝑘 ) )
130 eqid ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) )
131 68 130 fnmpti ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... 𝑤 )
132 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
133 132 fneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) Fn ( 𝑀 ... 𝑤 ) ↔ ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... 𝑤 ) ) )
134 131 133 mpbiri ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) Fn ( 𝑀 ... 𝑤 ) )
135 134 fndmd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → dom ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑀 ... 𝑤 ) )
136 129 135 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑤 ) )
137 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → 𝑘 ∈ 𝑍 )
138 137 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
139 fzopth ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑤 ) ↔ ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑤 ) ) )
140 138 139 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑤 ) ↔ ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑤 ) ) )
141 136 140 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑤 ) )
142 141 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → 𝑘 = 𝑤 )
143 142 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑘 + 1 ) = ( 𝑤 + 1 ) )
144 143 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑀 ... ( 𝑘 + 1 ) ) = ( 𝑀 ... ( 𝑤 + 1 ) ) )
145 elfzp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) ∨ 𝑥 = ( 𝑘 + 1 ) ) ) )
146 138 145 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) ∨ 𝑥 = ( 𝑘 + 1 ) ) ) )
147 136 reseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑤 ) ) )
148 fzssp1 ⊢ ( 𝑀 ... 𝑤 ) ⊆ ( 𝑀 ... ( 𝑤 + 1 ) )
149 resmpt ⊢ ( ( 𝑀 ... 𝑤 ) ⊆ ( 𝑀 ... ( 𝑤 + 1 ) ) → ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑤 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
150 148 149 ax-mp ⊢ ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑤 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) )
151 147 150 eqtr2di ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) )
152 132 151 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) )
153 152 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) = ( ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) )
154 fvres ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) )
155 fvres ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) → ( ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) )
156 154 155 eqeq12d ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) → ( ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) = ( ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ‘ 𝑥 ) ↔ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
157 153 156 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
158 143 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 = ( 𝑘 + 1 ) ↔ 𝑥 = ( 𝑤 + 1 ) ) )
159 142 138 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → 𝑤 ∈ ( ℤ≥ ‘ 𝑀 ) )
160 peano2uz ⊢ ( 𝑤 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑤 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
161 eluzfz2 ⊢ ( ( 𝑤 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑤 + 1 ) ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) )
162 fveq2 ⊢ ( 𝑚 = ( 𝑤 + 1 ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ ( 𝑤 + 1 ) ) )
163 id ⊢ ( 𝑚 = ( 𝑤 + 1 ) → 𝑚 = ( 𝑤 + 1 ) )
164 162 163 fveq12d ⊢ ( 𝑚 = ( 𝑤 + 1 ) → ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) )
165 eqid ⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) )
166 fvex ⊢ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) ∈ V
167 164 165 166 fvmpt ⊢ ( ( 𝑤 + 1 ) ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) → ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ ( 𝑤 + 1 ) ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) )
168 159 160 161 167 4syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ ( 𝑤 + 1 ) ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) )
169 168 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ ( 𝑤 + 1 ) ) )
170 fveq2 ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) )
171 fveq2 ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ ( 𝑤 + 1 ) ) )
172 170 171 eqeq12d ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ↔ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ ( 𝑤 + 1 ) ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ ( 𝑤 + 1 ) ) ) )
173 169 172 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 = ( 𝑤 + 1 ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
174 158 173 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
175 157 174 jaod ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑘 ) ∨ 𝑥 = ( 𝑘 + 1 ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
176 146 175 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
177 176 ralrimiv ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) )
178 ffn ⊢ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 → ( 𝐺 ‘ ( 𝑤 + 1 ) ) Fn ( 𝑀 ... ( 𝑘 + 1 ) ) )
179 178 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) Fn ( 𝑀 ... ( 𝑘 + 1 ) ) )
180 68 165 fnmpti ⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... ( 𝑤 + 1 ) )
181 eqfnfv2 ⊢ ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) Fn ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) Fn ( 𝑀 ... ( 𝑤 + 1 ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( ( 𝑀 ... ( 𝑘 + 1 ) ) = ( 𝑀 ... ( 𝑤 + 1 ) ) ∧ ∀ 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) )
182 179 180 181 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( ( 𝑀 ... ( 𝑘 + 1 ) ) = ( 𝑀 ... ( 𝑤 + 1 ) ) ∧ ∀ 𝑥 ∈ ( 𝑀 ... ( 𝑘 + 1 ) ) ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) )
183 144 177 182 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
184 183 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
185 eqeq1 ⊢ ( ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↔ ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
186 185 imbi1d ⊢ ( ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) → ( ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ↔ ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
187 184 186 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
188 187 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
189 188 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( 𝑘 ∈ 𝑍 → ( ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) ) )
190 82 124 189 rexlimd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ∃ 𝑘 ∈ 𝑍 ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) = ( ( 𝐺 ‘ ( 𝑤 + 1 ) ) ↾ ( 𝑀 ... 𝑘 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
191 123 190 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
192 191 expcom ⊢ ( 𝑤 ∈ 𝑍 → ( 𝜑 → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
193 74 192 sylbir ⊢ ( 𝑤 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
194 193 a2d ⊢ ( 𝑤 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝐺 ‘ 𝑤 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑤 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) → ( 𝜑 → ( 𝐺 ‘ ( 𝑤 + 1 ) ) = ( 𝑚 ∈ ( 𝑀 ... ( 𝑤 + 1 ) ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) ) )
195 37 42 47 52 73 194 uzind4 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝐺 ‘ 𝑘 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
196 195 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → ( 𝜑 → ( 𝐺 ‘ 𝑘 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ) )
197 196 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
198 197 dmeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝐺 ‘ 𝑘 ) = dom ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
199 dmmptg ⊢ ( ∀ 𝑚 ∈ ( 𝑀 ... 𝑘 ) ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ∈ V → dom ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑀 ... 𝑘 ) )
200 68 a1i ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) → ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ∈ V )
201 199 200 mprg ⊢ dom ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑀 ... 𝑘 )
202 198 201 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑘 ) )
203 202 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑛 ) ↔ ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑛 ) ) )
204 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
205 204 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
206 fzopth ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑛 ) ↔ ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑛 ) ) )
207 205 206 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑛 ) ↔ ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑛 ) ) )
208 203 207 bitrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑛 ) ↔ ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑛 ) ) )
209 simpr ⊢ ( ( 𝑀 = 𝑀 ∧ 𝑘 = 𝑛 ) → 𝑘 = 𝑛 )
210 208 209 biimtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( dom ( 𝐺 ‘ 𝑘 ) = ( 𝑀 ... 𝑛 ) → 𝑘 = 𝑛 ) )
211 32 210 syl5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) → 𝑘 = 𝑛 ) )
212 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑘 ) )
213 212 feq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ) )
214 4 sbcbidv ⊢ ( 𝑛 = 𝑘 → ( [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ↔ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) )
215 213 214 anbi12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) ↔ ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) ) )
216 215 equcoms ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) ↔ ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) ) )
217 216 biimpcd ⊢ ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) → ( 𝑘 = 𝑛 → ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) ) )
218 211 217 sylcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) → ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) ) )
219 218 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑛 ∈ 𝑍 ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜓 ) → ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) ) )
220 30 219 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 ) )
221 220 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 )
222 eluzfz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
223 205 222 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
224 221 223 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) ∈ 𝐴 )
225 55 cbvmptv ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑘 ) )
226 12 224 225 fmptdf ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) : 𝑍 ⟶ 𝐴 )
227 220 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → [ ( 𝐺 ‘ 𝑘 ) / 𝑔 ] 𝜃 )
228 197 227 sbceq1dd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 )
229 228 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 → [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 ) )
230 12 229 ralrimi ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 )
231 mpteq1 ⊢ ( ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑘 ) → ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
232 dfsbcq ⊢ ( ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) )
233 212 231 232 3syl ⊢ ( 𝑛 = 𝑘 → ( [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) )
234 4 sbcbidv ⊢ ( 𝑛 = 𝑘 → ( [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 ) )
235 233 234 bitrd ⊢ ( 𝑛 = 𝑘 → ( [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 ) )
236 235 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ↔ ∀ 𝑘 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑘 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜃 )
237 230 236 sylibr ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 )
238 80 mptex ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ∈ V
239 feq1 ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝑓 : 𝑍 ⟶ 𝐴 ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) : 𝑍 ⟶ 𝐴 ) )
240 vex ⊢ 𝑓 ∈ V
241 240 resex ⊢ ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) ∈ V
242 241 2 sbcie ⊢ ( [ ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) / 𝑔 ] 𝜓 ↔ 𝜒 )
243 reseq1 ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑛 ) ) )
244 fzssuz ⊢ ( 𝑀 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑀 )
245 244 1 sseqtrri ⊢ ( 𝑀 ... 𝑛 ) ⊆ 𝑍
246 resmpt ⊢ ( ( 𝑀 ... 𝑛 ) ⊆ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑛 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
247 245 246 ax-mp ⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) ↾ ( 𝑀 ... 𝑛 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) )
248 243 247 eqtrdi ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) = ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) )
249 248 sbceq1d ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( [ ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) / 𝑔 ] 𝜓 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) )
250 242 249 bitr3id ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( 𝜒 ↔ [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) )
251 250 ralbidv ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( ∀ 𝑛 ∈ 𝑍 𝜒 ↔ ∀ 𝑛 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) )
252 239 251 anbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) → ( ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) ↔ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) ) )
253 238 252 spcev ⊢ ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 [ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) ↦ ( ( 𝐺 ‘ 𝑚 ) ‘ 𝑚 ) ) / 𝑔 ] 𝜓 ) → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )
254 226 237 253 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )