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

Metamath Proof Explorer

Theorem ac6

Description: Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a larger set B , where ph depends on x (the natural number) and y (to specify a member of B ). A stronger version of this theorem, ac6s , allows B to be a proper class. (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses ac6.1 
|- A e. _V
ac6.2 
|- B e. _V
ac6.3 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6 
|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 ac6.1 
 |-  A e. _V
2 ac6.2 
 |-  B e. _V
3 ac6.3 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
4 ssrab2 
 |-  { y e. B | ph } C_ B
5 4 rgenw 
 |-  A. x e. A { y e. B | ph } C_ B
6 iunss 
 |-  ( U_ x e. A { y e. B | ph } C_ B <-> A. x e. A { y e. B | ph } C_ B )
7 5 6 mpbir 
 |-  U_ x e. A { y e. B | ph } C_ B
8 2 7 ssexi 
 |-  U_ x e. A { y e. B | ph } e. _V
9 numth3 
 |-  ( U_ x e. A { y e. B | ph } e. _V -> U_ x e. A { y e. B | ph } e. dom card )
10 8 9 ax-mp 
 |-  U_ x e. A { y e. B | ph } e. dom card
11 3 ac6num 
 |-  ( ( A e. _V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
12 1 10 11 mp3an12 
 |-  ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )