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∖∅→∃gg:ω⟶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∈nt⁡suc⁡j∈F⁡t⁡j↔∀j∈ns⁡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∈ns⁡suc⁡j∈F⁡s⁡j↔∀k∈ns⁡suc⁡k∈F⁡s⁡k
15 9 14 bitrdi ⊢t=s→∀j∈nt⁡suc⁡j∈F⁡t⁡j↔∀k∈ns⁡suc⁡k∈F⁡s⁡k
16 2 4 15 3anbi123d ⊢t=s→t:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j↔s:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k
17 16 rexbidv ⊢t=s→∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j↔∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k
18 17 cbvabv ⊢t|∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j=s|∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k
19 eqid ⊢x∈t|∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j⟼y∈t|∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j|dom⁡y=suc⁡dom⁡x∧y↾dom⁡x=x=x∈t|∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j⟼y∈t|∃n∈ωt:suc⁡n⟶A∧t⁡∅=C∧∀j∈nt⁡suc⁡j∈F⁡t⁡j|dom⁡y=suc⁡dom⁡x∧y↾dom⁡x=x
20 1 18 19 axdc3lem4 ⊢C∈A∧F:A⟶𝒫A∖∅→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈F⁡g⁡k