This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axdc

Description: This theorem derives ax-dc using ax-ac and ax-inf . Thus,AC impliesDC, but not vice-versa (so that ZFC is strictly stronger than ZF+DC). (New usage is discouraged.) (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Assertion axdc 
|- ( ( E. y E. z y x z /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( w = z -> ( u x w <-> u x z ) )
2 1 cbvabv 
 |-  { w | u x w } = { z | u x z }
3 breq1 
 |-  ( u = v -> ( u x z <-> v x z ) )
4 3 abbidv 
 |-  ( u = v -> { z | u x z } = { z | v x z } )
5 2 4 eqtrid 
 |-  ( u = v -> { w | u x w } = { z | v x z } )
6 5 fveq2d 
 |-  ( u = v -> ( g ` { w | u x w } ) = ( g ` { z | v x z } ) )
7 6 cbvmptv 
 |-  ( u e. _V |-> ( g ` { w | u x w } ) ) = ( v e. _V |-> ( g ` { z | v x z } ) )
8 rdgeq1 
 |-  ( ( u e. _V |-> ( g ` { w | u x w } ) ) = ( v e. _V |-> ( g ` { z | v x z } ) ) -> rec ( ( u e. _V |-> ( g ` { w | u x w } ) ) , y ) = rec ( ( v e. _V |-> ( g ` { z | v x z } ) ) , y ) )
9 7 8 ax-mp 
 |-  rec ( ( u e. _V |-> ( g ` { w | u x w } ) ) , y ) = rec ( ( v e. _V |-> ( g ` { z | v x z } ) ) , y )
10 9 reseq1i 
 |-  ( rec ( ( u e. _V |-> ( g ` { w | u x w } ) ) , y ) |` _om ) = ( rec ( ( v e. _V |-> ( g ` { z | v x z } ) ) , y ) |` _om )
11 10 axdclem2 
 |-  ( E. z y x z -> ( ran x C_ dom x -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )
12 11 exlimiv 
 |-  ( E. y E. z y x z -> ( ran x C_ dom x -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )
13 12 imp 
 |-  ( ( E. y E. z y x z /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) )