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 ) )