Theorem axdc4

Description: A more general version of axdc3 that allows the function F to vary with k . (Contributed by Mario Carneiro, 31-Jan-2013)

	Ref	Expression
Hypothesis	axdc4.1	⊢ 𝐴 ∈ V
Assertion	axdc4	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

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