Metamath Proof Explorer

Theorem axdc4uzlem

Description: Lemma for axdc4uz . (Contributed by Mario Carneiro, 8-Jan-2014) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses axdc4uz.1 ⊢ 𝑀 ∈ ℤ
axdc4uz.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
axdc4uz.3 ⊢ 𝐴 ∈ V
axdc4uz.4 ⊢ 𝐺 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω )
axdc4uz.5 ⊢ 𝐻 = ( 𝑛 ∈ ω , 𝑥 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) )
Assertion axdc4uzlem ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc4uz.1 ⊢ 𝑀 ∈ ℤ
2 axdc4uz.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 axdc4uz.3 ⊢ 𝐴 ∈ V
4 axdc4uz.4 ⊢ 𝐺 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω )
5 axdc4uz.5 ⊢ 𝐻 = ( 𝑛 ∈ ω , 𝑥 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) )
6 1 4 om2uzf1oi ⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝑀 )
7 f1oeq3 ⊢ ( 𝑍 = ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 : ω –1-1-onto→ 𝑍 ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝑀 ) ) )
8 2 7 ax-mp ⊢ ( 𝐺 : ω –1-1-onto→ 𝑍 ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝑀 ) )
9 6 8 mpbir ⊢ 𝐺 : ω –1-1-onto→ 𝑍
10 f1of ⊢ ( 𝐺 : ω –1-1-onto→ 𝑍 → 𝐺 : ω ⟶ 𝑍 )
11 9 10 ax-mp ⊢ 𝐺 : ω ⟶ 𝑍
12 11 ffvelrni ⊢ ( 𝑛 ∈ ω → ( 𝐺 ‘ 𝑛 ) ∈ 𝑍 )
13 fovrn ⊢ ( ( 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝐺 ‘ 𝑛 ) ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
14 12 13 syl3an2 ⊢ ( ( 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
15 14 3expb ⊢ ( ( 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
16 15 ralrimivva ⊢ ( 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∀ 𝑛 ∈ ω ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
17 5 fmpo ⊢ ( ∀ 𝑛 ∈ ω ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ 𝐻 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
18 16 17 sylib ⊢ ( 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝐻 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
19 3 axdc4 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐻 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑓 ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) )
20 18 19 sylan2 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑓 ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) )
21 f1ocnv ⊢ ( 𝐺 : ω –1-1-onto→ 𝑍 → ◡ 𝐺 : 𝑍 –1-1-onto→ ω )
22 f1of ⊢ ( ◡ 𝐺 : 𝑍 –1-1-onto→ ω → ◡ 𝐺 : 𝑍 ⟶ ω )
23 9 21 22 mp2b ⊢ ◡ 𝐺 : 𝑍 ⟶ ω
24 fco ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ◡ 𝐺 : 𝑍 ⟶ ω ) → ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 )
25 23 24 mpan2 ⊢ ( 𝑓 : ω ⟶ 𝐴 → ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 )
26 25 3ad2ant1 ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 )
27 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
28 1 27 ax-mp ⊢ 𝑀 ∈ ( ℤ≥ ‘ 𝑀 )
29 28 2 eleqtrri ⊢ 𝑀 ∈ 𝑍
30 fvco3 ⊢ ( ( ◡ 𝐺 : 𝑍 ⟶ ω ∧ 𝑀 ∈ 𝑍 ) → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑀 ) ) )
31 23 29 30 mp2an ⊢ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑀 ) )
32 1 4 om2uz0i ⊢ ( 𝐺 ‘ ∅ ) = 𝑀
33 peano1 ⊢ ∅ ∈ ω
34 f1ocnvfv ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ ∅ ∈ ω ) → ( ( 𝐺 ‘ ∅ ) = 𝑀 → ( ◡ 𝐺 ‘ 𝑀 ) = ∅ ) )
35 9 33 34 mp2an ⊢ ( ( 𝐺 ‘ ∅ ) = 𝑀 → ( ◡ 𝐺 ‘ 𝑀 ) = ∅ )
36 32 35 ax-mp ⊢ ( ◡ 𝐺 ‘ 𝑀 ) = ∅
37 36 fveq2i ⊢ ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑀 ) ) = ( 𝑓 ‘ ∅ )
38 31 37 eqtri ⊢ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = ( 𝑓 ‘ ∅ )
39 simp2 ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ( 𝑓 ‘ ∅ ) = 𝐶 )
40 38 39 syl5eq ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = 𝐶 )
41 23 ffvelrni ⊢ ( 𝑘 ∈ 𝑍 → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω )
42 41 adantl ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω )
43 suceq ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → suc 𝑚 = suc ( ◡ 𝐺 ‘ 𝑘 ) )
44 43 fveq2d ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → ( 𝑓 ‘ suc 𝑚 ) = ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) )
45 id ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) )
46 fveq2 ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) )
47 45 46 oveq12d ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) = ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
48 44 47 eleq12d ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ 𝑘 ) → ( ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ↔ ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) ) )
49 48 rspcv ⊢ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω → ( ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) → ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) ) )
50 42 49 syl ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) → ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) ) )
51 2 peano2uzs ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑘 + 1 ) ∈ 𝑍 )
52 fvco3 ⊢ ( ( ◡ 𝐺 : 𝑍 ⟶ ω ∧ ( 𝑘 + 1 ) ∈ 𝑍 ) → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
53 23 51 52 sylancr ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
54 1 4 om2uzsuci ⊢ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) + 1 ) )
55 41 54 syl ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) + 1 ) )
56 f1ocnvfv2 ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
57 9 56 mpan ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
58 57 oveq1d ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) + 1 ) = ( 𝑘 + 1 ) )
59 55 58 eqtrd ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( 𝑘 + 1 ) )
60 peano2 ⊢ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω → suc ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω )
61 41 60 syl ⊢ ( 𝑘 ∈ 𝑍 → suc ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω )
62 f1ocnvfv ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ suc ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω ) → ( ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( 𝑘 + 1 ) → ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝑘 ) ) )
63 9 61 62 sylancr ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( 𝑘 + 1 ) → ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝑘 ) ) )
64 59 63 mpd ⊢ ( 𝑘 ∈ 𝑍 → ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝑘 ) )
65 64 fveq2d ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑓 ‘ ( ◡ 𝐺 ‘ ( 𝑘 + 1 ) ) ) = ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) )
66 53 65 eqtr2d ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) )
67 66 adantl ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) )
68 ffvelrn ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω ) → ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ 𝐴 )
69 41 68 sylan2 ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ 𝐴 )
70 fveq2 ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ 𝑘 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) )
71 70 oveq1d ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ 𝑘 ) → ( ( 𝐺 ‘ 𝑛 ) 𝐹 𝑥 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 𝑥 ) )
72 oveq2 ⊢ ( 𝑥 = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 𝑥 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
73 ovex ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) ∈ V
74 71 72 5 73 ovmpo ⊢ ( ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ω ∧ ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ 𝐴 ) → ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
75 42 69 74 syl2anc ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
76 fvco3 ⊢ ( ( ◡ 𝐺 : 𝑍 ⟶ ω ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) )
77 23 76 mpan ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) = ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) )
78 77 eqcomd ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) )
79 57 78 oveq12d ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
80 79 adantl ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) 𝐹 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
81 75 80 eqtrd ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
82 67 81 eleq12d ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑓 ‘ suc ( ◡ 𝐺 ‘ 𝑘 ) ) ∈ ( ( ◡ 𝐺 ‘ 𝑘 ) 𝐻 ( 𝑓 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) ↔ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) )
83 50 82 sylibd ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) )
84 83 impancom ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ( 𝑘 ∈ 𝑍 → ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) )
85 84 ralrimiv ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
86 85 3adant2 ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
87 vex ⊢ 𝑓 ∈ V
88 rdgfun ⊢ Fun rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 )
89 omex ⊢ ω ∈ V
90 resfunexg ⊢ ( ( Fun rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ∧ ω ∈ V ) → ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ∈ V )
91 88 89 90 mp2an ⊢ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ∈ V
92 4 91 eqeltri ⊢ 𝐺 ∈ V
93 92 cnvex ⊢ ◡ 𝐺 ∈ V
94 87 93 coex ⊢ ( 𝑓 ∘ ◡ 𝐺 ) ∈ V
95 feq1 ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( 𝑔 : 𝑍 ⟶ 𝐴 ↔ ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 ) )
96 fveq1 ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( 𝑔 ‘ 𝑀 ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) )
97 96 eqeq1d ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( ( 𝑔 ‘ 𝑀 ) = 𝐶 ↔ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = 𝐶 ) )
98 fveq1 ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) )
99 fveq1 ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) )
100 99 oveq2d ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) = ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) )
101 98 100 eleq12d ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) )
102 101 ralbidv ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝑍 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) )
103 95 97 102 3anbi123d ⊢ ( 𝑔 = ( 𝑓 ∘ ◡ 𝐺 ) → ( ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 ∧ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) ) )
104 94 103 spcev ⊢ ( ( ( 𝑓 ∘ ◡ 𝐺 ) : 𝑍 ⟶ 𝐴 ∧ ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( ( 𝑓 ∘ ◡ 𝐺 ) ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
105 26 40 86 104 syl3anc ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
106 105 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : ω ⟶ 𝐴 ∧ ( 𝑓 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑚 ∈ ω ( 𝑓 ‘ suc 𝑚 ) ∈ ( 𝑚 𝐻 ( 𝑓 ‘ 𝑚 ) ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
107 20 106 syl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )