Metamath Proof Explorer

Theorem axdc2

Description: An apparent strengthening of ax-dc (but derived from it) which shows that there is a denumerable sequence g for any function that maps elements of a set A to nonempty subsets of A such that g ( x + 1 ) e. F ( g ( x ) ) for all x e. _om . The finitistic version of this can be proven by induction, but the infinite version requires this new axiom. (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Hypothesis axdc2.1 ⊢ A ∈ V
Assertion axdc2 ⊢ A ≠ ∅ ∧ F : A ⟶ 𝒫 A ∖ ∅ → ∃ g g : ω ⟶ A ∧ ∀ k ∈ ω g ⁡ suc ⁡ k ∈ F ⁡ g ⁡ k

Proof

Step Hyp Ref Expression
1 axdc2.1 ⊢ A ∈ V
2 eleq1w ⊢ s = x → s ∈ A ↔ x ∈ A
3 2 adantr ⊢ s = x ∧ t = y → s ∈ A ↔ x ∈ A
4 fveq2 ⊢ s = x → F ⁡ s = F ⁡ x
5 4 eleq2d ⊢ s = x → t ∈ F ⁡ s ↔ t ∈ F ⁡ x
6 eleq1w ⊢ t = y → t ∈ F ⁡ x ↔ y ∈ F ⁡ x
7 5 6 sylan9bb ⊢ s = x ∧ t = y → t ∈ F ⁡ s ↔ y ∈ F ⁡ x
8 3 7 anbi12d ⊢ s = x ∧ t = y → s ∈ A ∧ t ∈ F ⁡ s ↔ x ∈ A ∧ y ∈ F ⁡ x
9 8 cbvopabv ⊢ s t | s ∈ A ∧ t ∈ F ⁡ s = x y | x ∈ A ∧ y ∈ F ⁡ x
10 fveq2 ⊢ n = x → h ⁡ n = h ⁡ x
11 10 cbvmptv ⊢ n ∈ ω ⟼ h ⁡ n = x ∈ ω ⟼ h ⁡ x
12 1 9 11 axdc2lem ⊢ A ≠ ∅ ∧ F : A ⟶ 𝒫 A ∖ ∅ → ∃ g g : ω ⟶ A ∧ ∀ k ∈ ω g ⁡ suc ⁡ k ∈ F ⁡ g ⁡ k