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

Metamath Proof Explorer

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 )