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

Metamath Proof Explorer

Theorem acncc

Description: An ax-cc equivalent: every set has choice sets of length _om . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acncc 
|- AC_ _om = _V

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 omex 
 |-  _om e. _V
3 isacn 
 |-  ( ( x e. _V /\ _om e. _V ) -> ( x e. AC_ _om <-> A. f e. ( ( ~P x \ { (/) } ) ^m _om ) E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) )
4 1 2 3 mp2an 
 |-  ( x e. AC_ _om <-> A. f e. ( ( ~P x \ { (/) } ) ^m _om ) E. g A. y e. _om ( g ` y ) e. ( f ` y ) )
5 axcc2 
 |-  E. g ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) )
6 elmapi 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> f : _om --> ( ~P x \ { (/) } ) )
7 ffvelcdm 
 |-  ( ( f : _om --> ( ~P x \ { (/) } ) /\ y e. _om ) -> ( f ` y ) e. ( ~P x \ { (/) } ) )
8 eldifsni 
 |-  ( ( f ` y ) e. ( ~P x \ { (/) } ) -> ( f ` y ) =/= (/) )
9 7 8 syl 
 |-  ( ( f : _om --> ( ~P x \ { (/) } ) /\ y e. _om ) -> ( f ` y ) =/= (/) )
10 6 9 sylan 
 |-  ( ( f e. ( ( ~P x \ { (/) } ) ^m _om ) /\ y e. _om ) -> ( f ` y ) =/= (/) )
11 id 
 |-  ( ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) )
12 10 11 syl5com 
 |-  ( ( f e. ( ( ~P x \ { (/) } ) ^m _om ) /\ y e. _om ) -> ( ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> ( g ` y ) e. ( f ` y ) ) )
13 12 ralimdva 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> A. y e. _om ( g ` y ) e. ( f ` y ) ) )
14 13 adantld 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) -> A. y e. _om ( g ` y ) e. ( f ` y ) ) )
15 14 eximdv 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( E. g ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) -> E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) )
16 5 15 mpi 
 |-  ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> E. g A. y e. _om ( g ` y ) e. ( f ` y ) )
17 4 16 mprgbir 
 |-  x e. AC_ _om
18 17 1 2th 
 |-  ( x e. AC_ _om <-> x e. _V )
19 18 eqriv 
 |-  AC_ _om = _V