Metamath Proof Explorer

Theorem ac5b

Description: Equivalent of Axiom of Choice. (Contributed by NM, 31-Aug-1999)

Ref Expression
Hypothesis ac5b.1 
|- A e. _V
Assertion ac5b 
|- ( A. x e. A x =/= (/) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )

Proof

Step Hyp Ref Expression
1 ac5b.1 
 |-  A e. _V
2 1 uniex 
 |-  U. A e. _V
3 numth3 
 |-  ( U. A e. _V -> U. A e. dom card )
4 2 3 mp1i 
 |-  ( A. x e. A x =/= (/) -> U. A e. dom card )
5 neirr 
 |-  -. (/) =/= (/)
6 neeq1 
 |-  ( x = (/) -> ( x =/= (/) <-> (/) =/= (/) ) )
7 6 rspccv 
 |-  ( A. x e. A x =/= (/) -> ( (/) e. A -> (/) =/= (/) ) )
8 5 7 mtoi 
 |-  ( A. x e. A x =/= (/) -> -. (/) e. A )
9 ac5num 
 |-  ( ( U. A e. dom card /\ -. (/) e. A ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )
10 4 8 9 syl2anc 
 |-  ( A. x e. A x =/= (/) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )