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

Metamath Proof Explorer

Theorem ac6s

Description: Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 , we derive this strong version of ac6 that doesn't require B to be a set. (Contributed by NM, 4-Feb-2004)

Ref Expression
Hypotheses ac6s.1 
|- A e. _V
ac6s.2 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6s 
|- ( 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 ac6s.1 
 |-  A e. _V
2 ac6s.2 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
3 1 bnd2 
 |-  ( A. x e. A E. y e. B ph -> E. z ( z C_ B /\ A. x e. A E. y e. z ph ) )
4 vex 
 |-  z e. _V
5 1 4 2 ac6 
 |-  ( A. x e. A E. y e. z ph -> E. f ( f : A --> z /\ A. x e. A ps ) )
6 5 anim2i 
 |-  ( ( z C_ B /\ A. x e. A E. y e. z ph ) -> ( z C_ B /\ E. f ( f : A --> z /\ A. x e. A ps ) ) )
7 6 eximi 
 |-  ( E. z ( z C_ B /\ A. x e. A E. y e. z ph ) -> E. z ( z C_ B /\ E. f ( f : A --> z /\ A. x e. A ps ) ) )
8 fss 
 |-  ( ( f : A --> z /\ z C_ B ) -> f : A --> B )
9 8 expcom 
 |-  ( z C_ B -> ( f : A --> z -> f : A --> B ) )
10 9 anim1d 
 |-  ( z C_ B -> ( ( f : A --> z /\ A. x e. A ps ) -> ( f : A --> B /\ A. x e. A ps ) ) )
11 10 eximdv 
 |-  ( z C_ B -> ( E. f ( f : A --> z /\ A. x e. A ps ) -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
12 11 imp 
 |-  ( ( z C_ B /\ E. f ( f : A --> z /\ A. x e. A ps ) ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
13 12 exlimiv 
 |-  ( E. z ( z C_ B /\ E. f ( f : A --> z /\ A. x e. A ps ) ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
14 3 7 13 3syl 
 |-  ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )