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

Proof

Step	Hyp	Ref	Expression
1		axdc2.1	|- A e. _V
2		eleq1w	|- ( s = x -> ( s e. A <-> x e. A ) )
3	2	adantr	|- ( ( s = x /\ t = y ) -> ( s e. A <-> x e. A ) )
4		fveq2	|- ( s = x -> ( F ` s ) = ( F ` x ) )
5	4	eleq2d	|- ( s = x -> ( t e. ( F ` s ) <-> t e. ( F ` x ) ) )
6		eleq1w	|- ( t = y -> ( t e. ( F ` x ) <-> y e. ( F ` x ) ) )
7	5 6	sylan9bb	|- ( ( s = x /\ t = y ) -> ( t e. ( F ` s ) <-> y e. ( F ` x ) ) )
8	3 7	anbi12d	|- ( ( s = x /\ t = y ) -> ( ( s e. A /\ t e. ( F ` s ) ) <-> ( x e. A /\ y e. ( F ` x ) ) ) )
9	8	cbvopabv	|- { <. s , t >. | ( s e. A /\ t e. ( F ` s ) ) } = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
10		fveq2	|- ( n = x -> ( h ` n ) = ( h ` x ) )
11	10	cbvmptv	|- ( n e. _om |-> ( h ` n ) ) = ( x e. _om |-> ( h ` x ) )
12	1 9 11	axdc2lem	|- ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )