Metamath Proof Explorer

Theorem axdc4

Description: A more general version of axdc3 that allows the function F to vary with k . (Contributed by Mario Carneiro, 31-Jan-2013)

		Ref	Expression
	Hypothesis	axdc4.1	\|- A e. _V
	Assertion	axdc4	\|- ( ( C e. A /\ F : ( _om X. A ) --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( k F ( g ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc4.1	\|- A e. _V
2		eqid	\|- ( n e. _om , x e. A \|-> ( { suc n } X. ( n F x ) ) ) = ( n e. _om , x e. A \|-> ( { suc n } X. ( n F x ) ) )
3	1 2	axdc4lem	\|- ( ( C e. A /\ F : ( _om X. A ) --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( k F ( g ` k ) ) ) )

Step

Hyp

Ref

Expression

axdc4.1

 |-  A e. _V

eqid

 |-  ( n e. _om , x e. A |-> ( { suc n } X. ( n F x ) ) ) = ( n e. _om , x e. A |-> ( { suc n } X. ( n F x ) ) )

1 2

axdc4lem

 |-  ( ( C e. A /\ F : ( _om X. A ) --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( k F ( g ` k ) ) ) )