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