Metamath Proof Explorer


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 ) )