Metamath Proof Explorer

Theorem axcc3

Description: A possibly more useful version of ax-cc using sequences F ( n ) instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses axcc3.1 ⊢ 𝐹 ∈ V
axcc3.2 ⊢ 𝑁 ≈ ω
Assertion axcc3 ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 axcc3.1 ⊢ 𝐹 ∈ V
2 axcc3.2 ⊢ 𝑁 ≈ ω
3 relen ⊢ Rel ≈
4 3 brrelex1i ⊢ ( 𝑁 ≈ ω → 𝑁 ∈ V )
5 mptexg ⊢ ( 𝑁 ∈ V → ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∈ V )
6 2 4 5 mp2b ⊢ ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∈ V
7 bren ⊢ ( 𝑁 ≈ ω ↔ ∃ ℎ ℎ : 𝑁 –1-1-onto→ ω )
8 2 7 mpbi ⊢ ∃ ℎ ℎ : 𝑁 –1-1-onto→ ω
9 axcc2 ⊢ ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) )
10 f1of ⊢ ( ℎ : 𝑁 –1-1-onto→ ω → ℎ : 𝑁 ⟶ ω )
11 fnfco ⊢ ( ( 𝑔 Fn ω ∧ ℎ : 𝑁 ⟶ ω ) → ( 𝑔 ∘ ℎ ) Fn 𝑁 )
12 10 11 sylan2 ⊢ ( ( 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( 𝑔 ∘ ℎ ) Fn 𝑁 )
13 12 adantlr ⊢ ( ( ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( 𝑔 ∘ ℎ ) Fn 𝑁 )
14 13 3adant1 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( 𝑔 ∘ ℎ ) Fn 𝑁 )
15 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑁 ↦ 𝐹 )
16 15 nfeq2 ⊢ Ⅎ 𝑛 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 )
17 nfv ⊢ Ⅎ 𝑛 ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) )
18 nfv ⊢ Ⅎ 𝑛 ℎ : 𝑁 –1-1-onto→ ω
19 16 17 18 nf3an ⊢ Ⅎ 𝑛 ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω )
20 10 ffvelrnda ⊢ ( ( ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ℎ ‘ 𝑛 ) ∈ ω )
21 fveq2 ⊢ ( 𝑚 = ( ℎ ‘ 𝑛 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) = ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) )
22 21 neeq1d ⊢ ( 𝑚 = ( ℎ ‘ 𝑛 ) → ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ ↔ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ ) )
23 fveq2 ⊢ ( 𝑚 = ( ℎ ‘ 𝑛 ) → ( 𝑔 ‘ 𝑚 ) = ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) )
24 23 21 eleq12d ⊢ ( 𝑚 = ( ℎ ‘ 𝑛 ) → ( ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ↔ ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) )
25 22 24 imbi12d ⊢ ( 𝑚 = ( ℎ ‘ 𝑛 ) → ( ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ↔ ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ → ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) ) )
26 25 rspcv ⊢ ( ( ℎ ‘ 𝑛 ) ∈ ω → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ → ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) ) )
27 20 26 syl ⊢ ( ( ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ → ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) ) )
28 27 3ad2antl3 ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ → ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) ) )
29 f1ocnv ⊢ ( ℎ : 𝑁 –1-1-onto→ ω → ◡ ℎ : ω –1-1-onto→ 𝑁 )
30 f1of ⊢ ( ◡ ℎ : ω –1-1-onto→ 𝑁 → ◡ ℎ : ω ⟶ 𝑁 )
31 29 30 syl ⊢ ( ℎ : 𝑁 –1-1-onto→ ω → ◡ ℎ : ω ⟶ 𝑁 )
32 fvco3 ⊢ ( ( ◡ ℎ : ω ⟶ 𝑁 ∧ ( ℎ ‘ 𝑛 ) ∈ ω ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = ( 𝑘 ‘ ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) ) )
33 31 20 32 syl2an2r ⊢ ( ( ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = ( 𝑘 ‘ ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) ) )
34 33 3adant1 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = ( 𝑘 ‘ ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) ) )
35 f1ocnvfv1 ⊢ ( ( ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) = 𝑛 )
36 35 fveq2d ⊢ ( ( ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( 𝑘 ‘ ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
37 36 3adant1 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( 𝑘 ‘ ( ◡ ℎ ‘ ( ℎ ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
38 fveq1 ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( 𝑘 ‘ 𝑛 ) = ( ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ‘ 𝑛 ) )
39 eqid ⊢ ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) = ( 𝑛 ∈ 𝑁 ↦ 𝐹 )
40 39 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V ) → ( ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ‘ 𝑛 ) = 𝐹 )
41 1 40 mpan2 ⊢ ( 𝑛 ∈ 𝑁 → ( ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ‘ 𝑛 ) = 𝐹 )
42 38 41 sylan9eq ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝑘 ‘ 𝑛 ) = 𝐹 )
43 42 3adant2 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( 𝑘 ‘ 𝑛 ) = 𝐹 )
44 34 37 43 3eqtrd ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ℎ : 𝑁 –1-1-onto→ ω ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = 𝐹 )
45 44 3expa ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = 𝐹 )
46 45 3adantl2 ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) = 𝐹 )
47 46 neeq1d ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
48 10 3ad2ant3 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ℎ : 𝑁 ⟶ ω )
49 fvco3 ⊢ ( ( ℎ : 𝑁 ⟶ ω ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) = ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) )
50 48 49 sylan ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) = ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) )
51 50 eleq1d ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ↔ ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) )
52 46 eleq2d ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ↔ ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) )
53 51 52 bitr3d ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ↔ ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) )
54 47 53 imbi12d ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ≠ ∅ → ( 𝑔 ‘ ( ℎ ‘ 𝑛 ) ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ ( ℎ ‘ 𝑛 ) ) ) ↔ ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) )
55 28 54 sylibd ⊢ ( ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) )
56 55 ex ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( 𝑛 ∈ 𝑁 → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
57 56 com23 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ 𝑔 Fn ω ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
58 57 3exp ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( 𝑔 Fn ω → ( ℎ : 𝑁 –1-1-onto→ ω → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) ) ) )
59 58 com34 ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( 𝑔 Fn ω → ( ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) → ( ℎ : 𝑁 –1-1-onto→ ω → ( 𝑛 ∈ 𝑁 → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) ) ) )
60 59 imp32 ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ) → ( ℎ : 𝑁 –1-1-onto→ ω → ( 𝑛 ∈ 𝑁 → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
61 60 3impia ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) )
62 19 61 ralrimi ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) )
63 vex ⊢ 𝑔 ∈ V
64 vex ⊢ ℎ ∈ V
65 63 64 coex ⊢ ( 𝑔 ∘ ℎ ) ∈ V
66 fneq1 ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( 𝑓 Fn 𝑁 ↔ ( 𝑔 ∘ ℎ ) Fn 𝑁 ) )
67 fveq1 ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( 𝑓 ‘ 𝑛 ) = ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) )
68 67 eleq1d ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ↔ ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) )
69 68 imbi2d ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ↔ ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) )
70 69 ralbidv ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ↔ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) )
71 66 70 anbi12d ⊢ ( 𝑓 = ( 𝑔 ∘ ℎ ) → ( ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) ↔ ( ( 𝑔 ∘ ℎ ) Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
72 65 71 spcev ⊢ ( ( ( 𝑔 ∘ ℎ ) Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( ( 𝑔 ∘ ℎ ) ‘ 𝑛 ) ∈ 𝐹 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) )
73 14 62 72 syl2anc ⊢ ( ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) ∧ ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) ∧ ℎ : 𝑁 –1-1-onto→ ω ) → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) )
74 73 3exp ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) → ( ℎ : 𝑁 –1-1-onto→ ω → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) ) ) )
75 74 exlimdv ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑚 ∈ ω ( ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ≠ ∅ → ( 𝑔 ‘ 𝑚 ) ∈ ( ( 𝑘 ∘ ◡ ℎ ) ‘ 𝑚 ) ) ) → ( ℎ : 𝑁 –1-1-onto→ ω → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) ) ) )
76 9 75 mpi ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( ℎ : 𝑁 –1-1-onto→ ω → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
77 76 exlimdv ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ( ∃ ℎ ℎ : 𝑁 –1-1-onto→ ω → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) ) )
78 8 77 mpi ⊢ ( 𝑘 = ( 𝑛 ∈ 𝑁 ↦ 𝐹 ) → ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) ) )
79 6 78 vtocle ⊢ ∃ 𝑓 ( 𝑓 Fn 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝐹 ≠ ∅ → ( 𝑓 ‘ 𝑛 ) ∈ 𝐹 ) )