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 e. _V
Assertion	axdc3	|- ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc3.1	|- A e. _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 ) e. ( F ` ( t ` j ) ) <-> ( s ` suc j ) e. ( F ` ( s ` j ) ) ) )
9	8	ralbidv	|- ( t = s -> ( A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) <-> A. j e. n ( s ` suc j ) e. ( 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 ) e. ( F ` ( s ` j ) ) <-> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
14	13	cbvralvw	|- ( A. j e. n ( s ` suc j ) e. ( F ` ( s ` j ) ) <-> A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) )
15	9 14	bitrdi	|- ( t = s -> ( A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) <-> A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
16	2 4 15	3anbi123d	|- ( t = s -> ( ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) <-> ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
17	16	rexbidv	|- ( t = s -> ( E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) <-> E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
18	17	cbvabv	|- { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
19		eqid	|- ( x e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } |-> { y e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } ) = ( x e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } |-> { y e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
20	1 18 19	axdc3lem4	|- ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )