Metamath Proof Explorer

Theorem axdc3

Description: Dependent Choice. Axiom DC1 of Schechter p. 149, with the addition of an initial value C . This theorem is weaker than the Axiom of Choice but is stronger than Countable Choice. It shows the existence of a sequence whose values can only be shown to exist (but cannot be constructed explicitly) and also depend on earlier values in the sequence. (Contributed by Mario Carneiro, 27-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 axdc3.1 ⊢ A ∈ V
2 feq1 ⊢ t = s → t : suc ⁡ n ⟶ A ↔ s : suc ⁡ n ⟶ A
3 fveq1 ⊢ t = s → t ⁡ ∅ = s ⁡ ∅
4 3 eqeq1d ⊢ t = s → t ⁡ ∅ = C ↔ s ⁡ ∅ = C
5 fveq1 ⊢ t = s → t ⁡ suc ⁡ j = s ⁡ suc ⁡ j
6 fveq1 ⊢ t = s → t ⁡ j = s ⁡ j
7 6 fveq2d ⊢ t = s → F ⁡ t ⁡ j = F ⁡ s ⁡ j
8 5 7 eleq12d ⊢ t = s → t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ↔ s ⁡ suc ⁡ j ∈ F ⁡ s ⁡ j
9 8 ralbidv ⊢ t = s → ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ↔ ∀ j ∈ n s ⁡ suc ⁡ j ∈ F ⁡ s ⁡ j
10 suceq ⊢ j = k → suc ⁡ j = suc ⁡ k
11 10 fveq2d ⊢ j = k → s ⁡ suc ⁡ j = s ⁡ suc ⁡ k
12 2fveq3 ⊢ j = k → F ⁡ s ⁡ j = F ⁡ s ⁡ k
13 11 12 eleq12d ⊢ j = k → s ⁡ suc ⁡ j ∈ F ⁡ s ⁡ j ↔ s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
14 13 cbvralvw ⊢ ∀ j ∈ n s ⁡ suc ⁡ j ∈ F ⁡ s ⁡ j ↔ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
15 9 14 bitrdi ⊢ t = s → ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ↔ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
16 2 4 15 3anbi123d ⊢ t = s → t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ↔ s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
17 16 rexbidv ⊢ t = s → ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ↔ ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
18 17 cbvabv ⊢ t | ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j = s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
19 eqid ⊢ x ∈ t | ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ⟼ y ∈ t | ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j | dom ⁡ y = suc ⁡ dom ⁡ x ∧ y ↾ dom ⁡ x = x = x ∈ t | ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j ⟼ y ∈ t | ∃ n ∈ ω t : suc ⁡ n ⟶ A ∧ t ⁡ ∅ = C ∧ ∀ j ∈ n t ⁡ suc ⁡ j ∈ F ⁡ t ⁡ j | dom ⁡ y = suc ⁡ dom ⁡ x ∧ y ↾ dom ⁡ x = x
20 1 18 19 axdc3lem4 ⊢ C ∈ A ∧ F : A ⟶ 𝒫 A ∖ ∅ → ∃ g g : ω ⟶ A ∧ g ⁡ ∅ = C ∧ ∀ k ∈ ω g ⁡ suc ⁡ k ∈ F ⁡ g ⁡ k