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

Metamath Proof Explorer

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