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

Metamath Proof Explorer

Theorem acnrcl

Description: Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnrcl 
|- ( X e. AC_ A -> A e. _V )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( X e. { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } -> { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) )
2 abn0 
 |-  ( { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) <-> E. x ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) )
3 simpl 
 |-  ( ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) -> A e. _V )
4 3 exlimiv 
 |-  ( E. x ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) -> A e. _V )
5 2 4 sylbi 
 |-  ( { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) -> A e. _V )
6 1 5 syl 
 |-  ( X e. { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } -> A e. _V )
7 df-acn 
 |-  AC_ A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
8 6 7 eleq2s 
 |-  ( X e. AC_ A -> A e. _V )