Metamath Proof Explorer

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 ⊢ A ∈ V
Assertion axdc4 ⊢ C ∈ A ∧ F : ω × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : ω ⟶ A ∧ g ⁡ ∅ = C ∧ ∀ k ∈ ω g ⁡ suc ⁡ k ∈ k F g ⁡ k

Proof

Step Hyp Ref Expression
1 axdc4.1 ⊢ A ∈ V
2 eqid ⊢ n ∈ ω , x ∈ A ⟼ suc ⁡ n × n F x = n ∈ ω , x ∈ A ⟼ suc ⁡ n × n F x
3 1 2 axdc4lem ⊢ C ∈ A ∧ F : ω × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : ω ⟶ A ∧ g ⁡ ∅ = C ∧ ∀ k ∈ ω g ⁡ suc ⁡ k ∈ k F g ⁡ k