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	⊢ 𝐴 ∈ V
Assertion	axdc3	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc3.1	⊢ 𝐴 ∈ V
2		feq1	⊢ ( 𝑡 = 𝑠 → ( 𝑡 : suc 𝑛 ⟶ 𝐴 ↔ 𝑠 : suc 𝑛 ⟶ 𝐴 ) )
3		fveq1	⊢ ( 𝑡 = 𝑠 → ( 𝑡 ‘ ∅ ) = ( 𝑠 ‘ ∅ ) )
4	3	eqeq1d	⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 ‘ ∅ ) = 𝐶 ↔ ( 𝑠 ‘ ∅ ) = 𝐶 ) )
5		fveq1	⊢ ( 𝑡 = 𝑠 → ( 𝑡 ‘ suc 𝑗 ) = ( 𝑠 ‘ suc 𝑗 ) )
6		fveq1	⊢ ( 𝑡 = 𝑠 → ( 𝑡 ‘ 𝑗 ) = ( 𝑠 ‘ 𝑗 ) )
7	6	fveq2d	⊢ ( 𝑡 = 𝑠 → ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) )
8	5 7	eleq12d	⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ↔ ( 𝑠 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) ) )
9	8	ralbidv	⊢ ( 𝑡 = 𝑠 → ( ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑠 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) ) )
10		suceq	⊢ ( 𝑗 = 𝑘 → suc 𝑗 = suc 𝑘 )
11	10	fveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑠 ‘ suc 𝑗 ) = ( 𝑠 ‘ suc 𝑘 ) )
12		2fveq3	⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) )
13	11 12	eleq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑠 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) ↔ ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
14	13	cbvralvw	⊢ ( ∀ 𝑗 ∈ 𝑛 ( 𝑠 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) )
15	9 14	bitrdi	⊢ ( 𝑡 = 𝑠 → ( ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
16	2 4 15	3anbi123d	⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) ↔ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
17	16	rexbidv	⊢ ( 𝑡 = 𝑠 → ( ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) ↔ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
18	17	cbvabv	⊢ { 𝑡 ∣ ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) } = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
19		eqid	⊢ ( 𝑥 ∈ { 𝑡 ∣ ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) } ↦ { 𝑦 ∈ { 𝑡 ∣ ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) } ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ) = ( 𝑥 ∈ { 𝑡 ∣ ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) } ↦ { 𝑦 ∈ { 𝑡 ∣ ∃ 𝑛 ∈ ω ( 𝑡 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑡 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑗 ∈ 𝑛 ( 𝑡 ‘ suc 𝑗 ) ∈ ( 𝐹 ‘ ( 𝑡 ‘ 𝑗 ) ) ) } ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } )
20	1 18 19	axdc3lem4	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )