Theorem acni3

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	acni3.1	|- ( y = ( g ` x ) -> ( ph <-> ps ) )
Assertion	acni3	|- ( ( X e. AC_ A /\ A. x e. A E. y e. X ph ) -> E. g ( g : A --> X /\ A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		acni3.1	|- ( y = ( g ` x ) -> ( ph <-> ps ) )
2		rabn0	|- ( { y e. X | ph } =/= (/) <-> E. y e. X ph )
3	2	biimpri	|- ( E. y e. X ph -> { y e. X | ph } =/= (/) )
4		ssrab2	|- { y e. X | ph } C_ X
5	3 4	jctil	|- ( E. y e. X ph -> ( { y e. X | ph } C_ X /\ { y e. X | ph } =/= (/) ) )
6	5	ralimi	|- ( A. x e. A E. y e. X ph -> A. x e. A ( { y e. X | ph } C_ X /\ { y e. X | ph } =/= (/) ) )
7		acni2	|- ( ( X e. AC_ A /\ A. x e. A ( { y e. X | ph } C_ X /\ { y e. X | ph } =/= (/) ) ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. { y e. X | ph } ) )
8	6 7	sylan2	|- ( ( X e. AC_ A /\ A. x e. A E. y e. X ph ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. { y e. X | ph } ) )
9	1	elrab	|- ( ( g ` x ) e. { y e. X | ph } <-> ( ( g ` x ) e. X /\ ps ) )
10	9	simprbi	|- ( ( g ` x ) e. { y e. X | ph } -> ps )
11	10	ralimi	|- ( A. x e. A ( g ` x ) e. { y e. X | ph } -> A. x e. A ps )
12	11	anim2i	|- ( ( g : A --> X /\ A. x e. A ( g ` x ) e. { y e. X | ph } ) -> ( g : A --> X /\ A. x e. A ps ) )
13	12	eximi	|- ( E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. { y e. X | ph } ) -> E. g ( g : A --> X /\ A. x e. A ps ) )
14	8 13	syl	|- ( ( X e. AC_ A /\ A. x e. A E. y e. X ph ) -> E. g ( g : A --> X /\ A. x e. A ps ) )