Theorem axcc

Description: Although CC can be proven trivially using ac5 , we prove it here using DC. (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Feb-2013)

	Ref	Expression
Assertion	axcc	|- ( x ~~ _om -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x \ { (/) } ) = ( x \ { (/) } )
2		eqid	|- ( t e. _om , y e. U. ( x \ { (/) } ) |-> ( v ` t ) ) = ( t e. _om , y e. U. ( x \ { (/) } ) |-> ( v ` t ) )
3		eqid	|- ( w e. ( x \ { (/) } ) |-> ( u ` suc ( `' v ` w ) ) ) = ( w e. ( x \ { (/) } ) |-> ( u ` suc ( `' v ` w ) ) )
4	1 2 3	axcclem	|- ( x ~~ _om -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )