Theorem dfac13

Description: The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	dfac13	|- ( CHOICE <-> A. x x e. AC_ x )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		acacni	|- ( ( CHOICE /\ x e. _V ) -> AC_ x = _V )
3	2	elvd	|- ( CHOICE -> AC_ x = _V )
4	1 3	eleqtrrid	|- ( CHOICE -> x e. AC_ x )
5	4	alrimiv	|- ( CHOICE -> A. x x e. AC_ x )
6		vpwex	|- ~P z e. _V
7		id	|- ( x = ~P z -> x = ~P z )
8		acneq	|- ( x = ~P z -> AC_ x = AC_ ~P z )
9	7 8	eleq12d	|- ( x = ~P z -> ( x e. AC_ x <-> ~P z e. AC_ ~P z ) )
10	6 9	spcv	|- ( A. x x e. AC_ x -> ~P z e. AC_ ~P z )
11		vex	|- y e. _V
12		vex	|- z e. _V
13	12	canth2	|- z ~< ~P z
14		sdomdom	|- ( z ~< ~P z -> z ~<_ ~P z )
15		acndom2	|- ( z ~<_ ~P z -> ( ~P z e. AC_ ~P z -> z e. AC_ ~P z ) )
16	13 14 15	mp2b	|- ( ~P z e. AC_ ~P z -> z e. AC_ ~P z )
17		acnnum	|- ( z e. AC_ ~P z <-> z e. dom card )
18	16 17	sylib	|- ( ~P z e. AC_ ~P z -> z e. dom card )
19		numacn	|- ( y e. _V -> ( z e. dom card -> z e. AC_ y ) )
20	11 18 19	mpsyl	|- ( ~P z e. AC_ ~P z -> z e. AC_ y )
21	10 20	syl	|- ( A. x x e. AC_ x -> z e. AC_ y )
22	12	a1i	|- ( A. x x e. AC_ x -> z e. _V )
23	21 22	2thd	|- ( A. x x e. AC_ x -> ( z e. AC_ y <-> z e. _V ) )
24	23	eqrdv	|- ( A. x x e. AC_ x -> AC_ y = _V )
25	24	alrimiv	|- ( A. x x e. AC_ x -> A. y AC_ y = _V )
26		dfacacn	|- ( CHOICE <-> A. y AC_ y = _V )
27	25 26	sylibr	|- ( A. x x e. AC_ x -> CHOICE )
28	5 27	impbii	|- ( CHOICE <-> A. x x e. AC_ x )