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 ffvelrn
 |-  ( ( 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