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		reseq1	|- ( rec ( ( u e. _V |-> ( g ` { w | u x w } ) ) , y ) = rec ( ( v e. _V |-> ( g ` { z | v x z } ) ) , y ) -> ( rec ( ( u e. _V |-> ( g ` { w | u x w } ) ) , y ) |` _om ) = ( rec ( ( v e. _V |-> ( g ` { z | v x z } ) ) , y ) |` _om ) )
10	7 8 9	mp2b	|- ( 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 ) )