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	2	ac6	|- ( ( A e. _V /\ z e. _V /\ A. x e. A E. y e. z ph ) -> E. f ( f : A --> z /\ A. x e. A ps ) )
6	1 4 5	mp3an12	|- ( A. x e. A E. y e. z ph -> E. f ( f : A --> z /\ A. x e. A ps ) )
7	6	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 ) ) )
8	7	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 ) ) )
9		fss	|- ( ( f : A --> z /\ z C_ B ) -> f : A --> B )
10	9	expcom	|- ( z C_ B -> ( f : A --> z -> f : A --> B ) )
11	10	anim1d	|- ( z C_ B -> ( ( f : A --> z /\ A. x e. A ps ) -> ( f : A --> B /\ A. x e. A ps ) ) )
12	11	eximdv	|- ( 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	imp	|- ( ( z C_ B /\ E. f ( f : A --> z /\ A. x e. A ps ) ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
14	13	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 ) )
15	3 8 14	3syl	|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )