Metamath Proof Explorer

Theorem axdc4lem

Description: Lemma for axdc4 . (Contributed by Mario Carneiro, 31-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axdc4lem.1 ⊢ 𝐴 ∈ V
axdc4lem.2 ⊢ 𝐺 = ( 𝑛 ∈ ω , 𝑥 ∈ 𝐴 ↦ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) )
Assertion axdc4lem ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc4lem.1 ⊢ 𝐴 ∈ V
2 axdc4lem.2 ⊢ 𝐺 = ( 𝑛 ∈ ω , 𝑥 ∈ 𝐴 ↦ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) )
3 peano1 ⊢ ∅ ∈ ω
4 opelxpi ⊢ ( ( ∅ ∈ ω ∧ 𝐶 ∈ 𝐴 ) → ⟨ ∅ , 𝐶 ⟩ ∈ ( ω × 𝐴 ) )
5 3 4 mpan ⊢ ( 𝐶 ∈ 𝐴 → ⟨ ∅ , 𝐶 ⟩ ∈ ( ω × 𝐴 ) )
6 simp2 ⊢ ( ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ∈ ω )
7 fovcdm ⊢ ( ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
8 peano2 ⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
9 8 snssd ⊢ ( 𝑛 ∈ ω → { suc 𝑛 } ⊆ ω )
10 eldifi ⊢ ( ( 𝑛 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝑛 𝐹 𝑥 ) ∈ 𝒫 𝐴 )
11 1 elpw2 ⊢ ( ( 𝑛 𝐹 𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝑛 𝐹 𝑥 ) ⊆ 𝐴 )
12 xpss12 ⊢ ( ( { suc 𝑛 } ⊆ ω ∧ ( 𝑛 𝐹 𝑥 ) ⊆ 𝐴 ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ⊆ ( ω × 𝐴 ) )
13 11 12 sylan2b ⊢ ( ( { suc 𝑛 } ⊆ ω ∧ ( 𝑛 𝐹 𝑥 ) ∈ 𝒫 𝐴 ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ⊆ ( ω × 𝐴 ) )
14 9 10 13 syl2an ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑛 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ⊆ ( ω × 𝐴 ) )
15 snex ⊢ { suc 𝑛 } ∈ V
16 ovex ⊢ ( 𝑛 𝐹 𝑥 ) ∈ V
17 15 16 xpex ⊢ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ V
18 17 elpw ⊢ ( ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ 𝒫 ( ω × 𝐴 ) ↔ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ⊆ ( ω × 𝐴 ) )
19 14 18 sylibr ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑛 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ 𝒫 ( ω × 𝐴 ) )
20 6 7 19 syl2anc ⊢ ( ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ 𝒫 ( ω × 𝐴 ) )
21 eldifn ⊢ ( ( 𝑛 𝐹 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ¬ ( 𝑛 𝐹 𝑥 ) ∈ { ∅ } )
22 16 elsn ⊢ ( ( 𝑛 𝐹 𝑥 ) ∈ { ∅ } ↔ ( 𝑛 𝐹 𝑥 ) = ∅ )
23 22 necon3bbii ⊢ ( ¬ ( 𝑛 𝐹 𝑥 ) ∈ { ∅ } ↔ ( 𝑛 𝐹 𝑥 ) ≠ ∅ )
24 vex ⊢ 𝑛 ∈ V
25 24 sucex ⊢ suc 𝑛 ∈ V
26 25 snnz ⊢ { suc 𝑛 } ≠ ∅
27 xpnz ⊢ ( ( { suc 𝑛 } ≠ ∅ ∧ ( 𝑛 𝐹 𝑥 ) ≠ ∅ ) ↔ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ≠ ∅ )
28 27 biimpi ⊢ ( ( { suc 𝑛 } ≠ ∅ ∧ ( 𝑛 𝐹 𝑥 ) ≠ ∅ ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ≠ ∅ )
29 26 28 mpan ⊢ ( ( 𝑛 𝐹 𝑥 ) ≠ ∅ → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ≠ ∅ )
30 23 29 sylbi ⊢ ( ¬ ( 𝑛 𝐹 𝑥 ) ∈ { ∅ } → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ≠ ∅ )
31 17 elsn ⊢ ( ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ { ∅ } ↔ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) = ∅ )
32 31 necon3bbii ⊢ ( ¬ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ { ∅ } ↔ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ≠ ∅ )
33 30 32 sylibr ⊢ ( ¬ ( 𝑛 𝐹 𝑥 ) ∈ { ∅ } → ¬ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ { ∅ } )
34 7 21 33 3syl ⊢ ( ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ¬ ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ { ∅ } )
35 20 34 eldifd ⊢ ( ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) )
36 35 3expib ⊢ ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ( 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) ) )
37 36 ralrimivv ⊢ ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∀ 𝑛 ∈ ω ∀ 𝑥 ∈ 𝐴 ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) )
38 2 fmpo ⊢ ( ∀ 𝑛 ∈ ω ∀ 𝑥 ∈ 𝐴 ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) ∈ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) ↔ 𝐺 : ( ω × 𝐴 ) ⟶ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) )
39 37 38 sylib ⊢ ( 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝐺 : ( ω × 𝐴 ) ⟶ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) )
40 dcomex ⊢ ω ∈ V
41 40 1 xpex ⊢ ( ω × 𝐴 ) ∈ V
42 41 axdc3 ⊢ ( ( ⟨ ∅ , 𝐶 ⟩ ∈ ( ω × 𝐴 ) ∧ 𝐺 : ( ω × 𝐴 ) ⟶ ( 𝒫 ( ω × 𝐴 ) ∖ { ∅ } ) ) → ∃ ℎ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) )
43 5 39 42 syl2an ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ ℎ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) )
44 2ndcof ⊢ ( ℎ : ω ⟶ ( ω × 𝐴 ) → ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 )
45 44 3ad2ant1 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 )
46 45 adantl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 )
47 fex2 ⊢ ( ( ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V ) → ( 2nd ∘ ℎ ) ∈ V )
48 40 1 47 mp3an23 ⊢ ( ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 → ( 2nd ∘ ℎ ) ∈ V )
49 46 48 syl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 2nd ∘ ℎ ) ∈ V )
50 fvco3 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ∅ ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ ∅ ) = ( 2nd ‘ ( ℎ ‘ ∅ ) ) )
51 3 50 mpan2 ⊢ ( ℎ : ω ⟶ ( ω × 𝐴 ) → ( ( 2nd ∘ ℎ ) ‘ ∅ ) = ( 2nd ‘ ( ℎ ‘ ∅ ) ) )
52 51 3ad2ant1 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( 2nd ∘ ℎ ) ‘ ∅ ) = ( 2nd ‘ ( ℎ ‘ ∅ ) ) )
53 fveq2 ⊢ ( ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ → ( 2nd ‘ ( ℎ ‘ ∅ ) ) = ( 2nd ‘ ⟨ ∅ , 𝐶 ⟩ ) )
54 53 3ad2ant2 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 2nd ‘ ( ℎ ‘ ∅ ) ) = ( 2nd ‘ ⟨ ∅ , 𝐶 ⟩ ) )
55 52 54 eqtrd ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( 2nd ∘ ℎ ) ‘ ∅ ) = ( 2nd ‘ ⟨ ∅ , 𝐶 ⟩ ) )
56 op2ndg ⊢ ( ( ∅ ∈ ω ∧ 𝐶 ∈ 𝐴 ) → ( 2nd ‘ ⟨ ∅ , 𝐶 ⟩ ) = 𝐶 )
57 3 56 mpan ⊢ ( 𝐶 ∈ 𝐴 → ( 2nd ‘ ⟨ ∅ , 𝐶 ⟩ ) = 𝐶 )
58 55 57 sylan9eqr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ( 2nd ∘ ℎ ) ‘ ∅ ) = 𝐶 )
59 nfv ⊢ Ⅎ 𝑘 𝐶 ∈ 𝐴
60 nfv ⊢ Ⅎ 𝑘 ℎ : ω ⟶ ( ω × 𝐴 )
61 nfv ⊢ Ⅎ 𝑘 ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩
62 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) )
63 60 61 62 nf3an ⊢ Ⅎ 𝑘 ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) )
64 59 63 nfan ⊢ Ⅎ 𝑘 ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) )
65 fveq2 ⊢ ( 𝑚 = ∅ → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ ∅ ) )
66 opeq1 ⊢ ( 𝑚 = ∅ → ⟨ 𝑚 , 𝑧 ⟩ = ⟨ ∅ , 𝑧 ⟩ )
67 65 66 eqeq12d ⊢ ( 𝑚 = ∅ → ( ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ ) )
68 67 exbidv ⊢ ( 𝑚 = ∅ → ( ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ∃ 𝑧 ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ ) )
69 fveq2 ⊢ ( 𝑚 = 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑖 ) )
70 opeq1 ⊢ ( 𝑚 = 𝑖 → ⟨ 𝑚 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑧 ⟩ )
71 69 70 eqeq12d ⊢ ( 𝑚 = 𝑖 → ( ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) )
72 71 exbidv ⊢ ( 𝑚 = 𝑖 → ( ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) )
73 fveq2 ⊢ ( 𝑚 = suc 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ suc 𝑖 ) )
74 opeq1 ⊢ ( 𝑚 = suc 𝑖 → ⟨ 𝑚 , 𝑧 ⟩ = ⟨ suc 𝑖 , 𝑧 ⟩ )
75 73 74 eqeq12d ⊢ ( 𝑚 = suc 𝑖 → ( ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) )
76 75 exbidv ⊢ ( 𝑚 = suc 𝑖 → ( ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) )
77 opeq2 ⊢ ( 𝑧 = 𝐶 → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , 𝐶 ⟩ )
78 77 eqeq2d ⊢ ( 𝑧 = 𝐶 → ( ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ ↔ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ) )
79 78 spcegv ⊢ ( 𝐶 ∈ 𝐴 → ( ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ → ∃ 𝑧 ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ ) )
80 79 imp ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ) → ∃ 𝑧 ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ )
81 80 3ad2antr2 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ∃ 𝑧 ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝑧 ⟩ )
82 fveq2 ⊢ ( ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( 𝐺 ‘ ⟨ 𝑖 , 𝑧 ⟩ ) )
83 df-ov ⊢ ( 𝑖 𝐺 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑖 , 𝑧 ⟩ )
84 82 83 eqtr4di ⊢ ( ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( 𝑖 𝐺 𝑧 ) )
85 84 adantl ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( 𝑖 𝐺 𝑧 ) )
86 simplr ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → 𝑖 ∈ ω )
87 ffvelcdm ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) → ( ℎ ‘ 𝑖 ) ∈ ( ω × 𝐴 ) )
88 eleq1 ⊢ ( ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( ( ℎ ‘ 𝑖 ) ∈ ( ω × 𝐴 ) ↔ ⟨ 𝑖 , 𝑧 ⟩ ∈ ( ω × 𝐴 ) ) )
89 opelxp2 ⊢ ( ⟨ 𝑖 , 𝑧 ⟩ ∈ ( ω × 𝐴 ) → 𝑧 ∈ 𝐴 )
90 88 89 biimtrdi ⊢ ( ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( ( ℎ ‘ 𝑖 ) ∈ ( ω × 𝐴 ) → 𝑧 ∈ 𝐴 ) )
91 87 90 mpan9 ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → 𝑧 ∈ 𝐴 )
92 suceq ⊢ ( 𝑛 = 𝑖 → suc 𝑛 = suc 𝑖 )
93 92 sneqd ⊢ ( 𝑛 = 𝑖 → { suc 𝑛 } = { suc 𝑖 } )
94 oveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 𝐹 𝑥 ) = ( 𝑖 𝐹 𝑥 ) )
95 93 94 xpeq12d ⊢ ( 𝑛 = 𝑖 → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑥 ) ) )
96 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑖 𝐹 𝑥 ) = ( 𝑖 𝐹 𝑧 ) )
97 96 xpeq2d ⊢ ( 𝑥 = 𝑧 → ( { suc 𝑖 } × ( 𝑖 𝐹 𝑥 ) ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) )
98 snex ⊢ { suc 𝑖 } ∈ V
99 ovex ⊢ ( 𝑖 𝐹 𝑧 ) ∈ V
100 98 99 xpex ⊢ ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) ∈ V
101 95 97 2 100 ovmpo ⊢ ( ( 𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴 ) → ( 𝑖 𝐺 𝑧 ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) )
102 86 91 101 syl2anc ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → ( 𝑖 𝐺 𝑧 ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) )
103 85 102 eqtrd ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) )
104 suceq ⊢ ( 𝑘 = 𝑖 → suc 𝑘 = suc 𝑖 )
105 104 fveq2d ⊢ ( 𝑘 = 𝑖 → ( ℎ ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑖 ) )
106 2fveq3 ⊢ ( 𝑘 = 𝑖 → ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) = ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) )
107 105 106 eleq12d ⊢ ( 𝑘 = 𝑖 → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) )
108 107 rspcv ⊢ ( 𝑖 ∈ ω → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) )
109 108 ad2antlr ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) )
110 eleq2 ⊢ ( ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) ) )
111 elxp ⊢ ( ( ℎ ‘ suc 𝑖 ) ∈ ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) ↔ ∃ 𝑠 ∃ 𝑡 ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑖 } ∧ 𝑡 ∈ ( 𝑖 𝐹 𝑧 ) ) ) )
112 velsn ⊢ ( 𝑠 ∈ { suc 𝑖 } ↔ 𝑠 = suc 𝑖 )
113 opeq1 ⊢ ( 𝑠 = suc 𝑖 → ⟨ 𝑠 , 𝑡 ⟩ = ⟨ suc 𝑖 , 𝑡 ⟩ )
114 112 113 sylbi ⊢ ( 𝑠 ∈ { suc 𝑖 } → ⟨ 𝑠 , 𝑡 ⟩ = ⟨ suc 𝑖 , 𝑡 ⟩ )
115 114 eqeq2d ⊢ ( 𝑠 ∈ { suc 𝑖 } → ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ↔ ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) )
116 115 biimpac ⊢ ( ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ 𝑠 ∈ { suc 𝑖 } ) → ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ )
117 116 adantrr ⊢ ( ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑖 } ∧ 𝑡 ∈ ( 𝑖 𝐹 𝑧 ) ) ) → ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ )
118 117 eximi ⊢ ( ∃ 𝑡 ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑖 } ∧ 𝑡 ∈ ( 𝑖 𝐹 𝑧 ) ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ )
119 118 exlimiv ⊢ ( ∃ 𝑠 ∃ 𝑡 ( ( ℎ ‘ suc 𝑖 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑖 } ∧ 𝑡 ∈ ( 𝑖 𝐹 𝑧 ) ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ )
120 111 119 sylbi ⊢ ( ( ℎ ‘ suc 𝑖 ) ∈ ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ )
121 110 120 biimtrdi ⊢ ( ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = ( { suc 𝑖 } × ( 𝑖 𝐹 𝑧 ) ) → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) )
122 103 109 121 sylsyld ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) )
123 122 expcom ⊢ ( ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) ) )
124 123 exlimiv ⊢ ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) ) )
125 124 com3l ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ) ) )
126 opeq2 ⊢ ( 𝑡 = 𝑧 → ⟨ suc 𝑖 , 𝑡 ⟩ = ⟨ suc 𝑖 , 𝑧 ⟩ )
127 126 eqeq2d ⊢ ( 𝑡 = 𝑧 → ( ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ↔ ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) )
128 127 cbvexvw ⊢ ( ∃ 𝑡 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑡 ⟩ ↔ ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ )
129 125 128 syl8ib ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) ) )
130 129 impancom ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑖 ∈ ω → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) ) )
131 130 3adant2 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑖 ∈ ω → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) ) )
132 131 adantl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑖 ∈ ω → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) ) )
133 132 com12 ⊢ ( 𝑖 ∈ ω → ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ∃ 𝑧 ( ℎ ‘ 𝑖 ) = ⟨ 𝑖 , 𝑧 ⟩ → ∃ 𝑧 ( ℎ ‘ suc 𝑖 ) = ⟨ suc 𝑖 , 𝑧 ⟩ ) ) )
134 68 72 76 81 133 finds2 ⊢ ( 𝑚 ∈ ω → ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ) )
135 134 com12 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑚 ∈ ω → ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ) )
136 135 ralrimiv ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ∀ 𝑚 ∈ ω ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ )
137 fveq2 ⊢ ( 𝑚 = 𝑘 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑘 ) )
138 opeq1 ⊢ ( 𝑚 = 𝑘 → ⟨ 𝑚 , 𝑧 ⟩ = ⟨ 𝑘 , 𝑧 ⟩ )
139 137 138 eqeq12d ⊢ ( 𝑚 = 𝑘 → ( ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) )
140 139 exbidv ⊢ ( 𝑚 = 𝑘 → ( ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ ↔ ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) )
141 140 rspccv ⊢ ( ∀ 𝑚 ∈ ω ∃ 𝑧 ( ℎ ‘ 𝑚 ) = ⟨ 𝑚 , 𝑧 ⟩ → ( 𝑘 ∈ ω → ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) )
142 136 141 syl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑘 ∈ ω → ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) )
143 142 3impia ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ )
144 simp21 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ℎ : ω ⟶ ( ω × 𝐴 ) )
145 simp3 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → 𝑘 ∈ ω )
146 rspa ⊢ ( ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) )
147 146 3ad2antl3 ⊢ ( ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) )
148 147 3adant1 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) )
149 simpl ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ )
150 149 fveq2d ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) = ( 𝐺 ‘ ⟨ 𝑘 , 𝑧 ⟩ ) )
151 simprr ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → 𝑘 ∈ ω )
152 eleq1 ⊢ ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ ‘ 𝑘 ) ∈ ( ω × 𝐴 ) ↔ ⟨ 𝑘 , 𝑧 ⟩ ∈ ( ω × 𝐴 ) ) )
153 opelxp2 ⊢ ( ⟨ 𝑘 , 𝑧 ⟩ ∈ ( ω × 𝐴 ) → 𝑧 ∈ 𝐴 )
154 152 153 biimtrdi ⊢ ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ ‘ 𝑘 ) ∈ ( ω × 𝐴 ) → 𝑧 ∈ 𝐴 ) )
155 ffvelcdm ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ 𝑘 ) ∈ ( ω × 𝐴 ) )
156 154 155 impel ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → 𝑧 ∈ 𝐴 )
157 df-ov ⊢ ( 𝑘 𝐺 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑘 , 𝑧 ⟩ )
158 suceq ⊢ ( 𝑛 = 𝑘 → suc 𝑛 = suc 𝑘 )
159 158 sneqd ⊢ ( 𝑛 = 𝑘 → { suc 𝑛 } = { suc 𝑘 } )
160 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 𝐹 𝑥 ) = ( 𝑘 𝐹 𝑥 ) )
161 159 160 xpeq12d ⊢ ( 𝑛 = 𝑘 → ( { suc 𝑛 } × ( 𝑛 𝐹 𝑥 ) ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑥 ) ) )
162 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑘 𝐹 𝑥 ) = ( 𝑘 𝐹 𝑧 ) )
163 162 xpeq2d ⊢ ( 𝑥 = 𝑧 → ( { suc 𝑘 } × ( 𝑘 𝐹 𝑥 ) ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) )
164 snex ⊢ { suc 𝑘 } ∈ V
165 ovex ⊢ ( 𝑘 𝐹 𝑧 ) ∈ V
166 164 165 xpex ⊢ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) ∈ V
167 161 163 2 166 ovmpo ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴 ) → ( 𝑘 𝐺 𝑧 ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) )
168 157 167 eqtr3id ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ ⟨ 𝑘 , 𝑧 ⟩ ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) )
169 151 156 168 syl2anc ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 𝐺 ‘ ⟨ 𝑘 , 𝑧 ⟩ ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) )
170 150 169 eqtrd ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) = ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) )
171 170 eleq2d ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ↔ ( ℎ ‘ suc 𝑘 ) ∈ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) ) )
172 elxp ⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) ↔ ∃ 𝑠 ∃ 𝑡 ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑘 } ∧ 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) ) ) )
173 peano2 ⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω )
174 fvco3 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ suc 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) = ( 2nd ‘ ( ℎ ‘ suc 𝑘 ) ) )
175 173 174 sylan2 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) = ( 2nd ‘ ( ℎ ‘ suc 𝑘 ) ) )
176 175 adantl ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) = ( 2nd ‘ ( ℎ ‘ suc 𝑘 ) ) )
177 simpll ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ )
178 177 fveq2d ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 2nd ‘ ( ℎ ‘ suc 𝑘 ) ) = ( 2nd ‘ ⟨ 𝑠 , 𝑡 ⟩ ) )
179 176 178 eqtrd ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) = ( 2nd ‘ ⟨ 𝑠 , 𝑡 ⟩ ) )
180 vex ⊢ 𝑠 ∈ V
181 vex ⊢ 𝑡 ∈ V
182 180 181 op2nd ⊢ ( 2nd ‘ ⟨ 𝑠 , 𝑡 ⟩ ) = 𝑡
183 179 182 eqtrdi ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) = 𝑡 )
184 fvco3 ⊢ ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) = ( 2nd ‘ ( ℎ ‘ 𝑘 ) ) )
185 184 adantl ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) = ( 2nd ‘ ( ℎ ‘ 𝑘 ) ) )
186 simplr ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ )
187 186 fveq2d ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 2nd ‘ ( ℎ ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ 𝑘 , 𝑧 ⟩ ) )
188 185 187 eqtrd ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) = ( 2nd ‘ ⟨ 𝑘 , 𝑧 ⟩ ) )
189 vex ⊢ 𝑘 ∈ V
190 vex ⊢ 𝑧 ∈ V
191 189 190 op2nd ⊢ ( 2nd ‘ ⟨ 𝑘 , 𝑧 ⟩ ) = 𝑧
192 188 191 eqtrdi ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) = 𝑧 )
193 192 oveq2d ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) = ( 𝑘 𝐹 𝑧 ) )
194 183 193 eleq12d ⊢ ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ↔ 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) ) )
195 194 biimprcd ⊢ ( 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) → ( ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ) ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
196 195 exp4c ⊢ ( 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) → ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ → ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) ) )
197 196 adantl ⊢ ( ( 𝑠 ∈ { suc 𝑘 } ∧ 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) ) → ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ → ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) ) )
198 197 impcom ⊢ ( ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑘 } ∧ 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) ) ) → ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
199 198 exlimivv ⊢ ( ∃ 𝑠 ∃ 𝑡 ( ( ℎ ‘ suc 𝑘 ) = ⟨ 𝑠 , 𝑡 ⟩ ∧ ( 𝑠 ∈ { suc 𝑘 } ∧ 𝑡 ∈ ( 𝑘 𝐹 𝑧 ) ) ) → ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
200 172 199 sylbi ⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) → ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
201 200 com3l ⊢ ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
202 201 imp ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( { suc 𝑘 } × ( 𝑘 𝐹 𝑧 ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
203 171 202 sylbid ⊢ ( ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
204 203 ex ⊢ ( ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
205 204 exlimiv ⊢ ( ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
206 205 3imp ⊢ ( ( ∃ 𝑧 ( ℎ ‘ 𝑘 ) = ⟨ 𝑘 , 𝑧 ⟩ ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ 𝑘 ∈ ω ) ∧ ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) )
207 143 144 145 148 206 syl121anc ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) )
208 207 3expia ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑘 ∈ ω → ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
209 64 208 ralrimi ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ω ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) )
210 46 58 209 3jca ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 ∧ ( ( 2nd ∘ ℎ ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
211 feq1 ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( 𝑔 : ω ⟶ 𝐴 ↔ ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 ) )
212 fveq1 ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( 𝑔 ‘ ∅ ) = ( ( 2nd ∘ ℎ ) ‘ ∅ ) )
213 212 eqeq1d ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( ( 𝑔 ‘ ∅ ) = 𝐶 ↔ ( ( 2nd ∘ ℎ ) ‘ ∅ ) = 𝐶 ) )
214 fveq1 ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( 𝑔 ‘ suc 𝑘 ) = ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) )
215 fveq1 ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( 𝑔 ‘ 𝑘 ) = ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) )
216 215 oveq2d ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) = ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) )
217 214 216 eleq12d ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
218 217 ralbidv ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ω ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) )
219 211 213 218 3anbi123d ⊢ ( 𝑔 = ( 2nd ∘ ℎ ) → ( ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( ( 2nd ∘ ℎ ) : ω ⟶ 𝐴 ∧ ( ( 2nd ∘ ℎ ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ( 2nd ∘ ℎ ) ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ( 2nd ∘ ℎ ) ‘ 𝑘 ) ) ) ) )
220 49 210 219 spcedv ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
221 220 ex ⊢ ( 𝐶 ∈ 𝐴 → ( ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
222 221 exlimdv ⊢ ( 𝐶 ∈ 𝐴 → ( ∃ ℎ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
223 222 adantr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ∃ ℎ ( ℎ : ω ⟶ ( ω × 𝐴 ) ∧ ( ℎ ‘ ∅ ) = ⟨ ∅ , 𝐶 ⟩ ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
224 43 223 mpd ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )