Metamath Proof Explorer

Theorem dfac8c

Description: If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013)

		Ref	Expression
	Assertion	dfac8c	\|- ( A e. B -> ( E. r r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) )

Step	Hyp	Ref	Expression
1		eqid	\|- ( x e. ( A \ { (/) } ) \|-> ( iota_ y e. x A. w e. x -. w r y ) ) = ( x e. ( A \ { (/) } ) \|-> ( iota_ y e. x A. w e. x -. w r y ) )
2	1	dfac8clem	\|- ( A e. B -> ( E. r r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) )

Step

Hyp

Ref

Expression

 |-  ( x e. ( A \ { (/) } ) |-> ( iota_ y e. x A. w e. x -. w r y ) ) = ( x e. ( A \ { (/) } ) |-> ( iota_ y e. x A. w e. x -. w r y ) )

 |-  ( A e. B -> ( E. r r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) )