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

Metamath Proof Explorer

Theorem acacni

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

Ref Expression
Assertion acacni 
|- ( ( CHOICE /\ A e. V ) -> AC_ A = _V )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( CHOICE /\ A e. V ) -> A e. V )
2 vex 
 |-  x e. _V
3 simpl 
 |-  ( ( CHOICE /\ A e. V ) -> CHOICE )
4 dfac10 
 |-  ( CHOICE <-> dom card = _V )
5 3 4 sylib 
 |-  ( ( CHOICE /\ A e. V ) -> dom card = _V )
6 2 5 eleqtrrid 
 |-  ( ( CHOICE /\ A e. V ) -> x e. dom card )
7 numacn 
 |-  ( A e. V -> ( x e. dom card -> x e. AC_ A ) )
8 1 6 7 sylc 
 |-  ( ( CHOICE /\ A e. V ) -> x e. AC_ A )
9 2 a1i 
 |-  ( ( CHOICE /\ A e. V ) -> x e. _V )
10 8 9 2thd 
 |-  ( ( CHOICE /\ A e. V ) -> ( x e. AC_ A <-> x e. _V ) )
11 10 eqrdv 
 |-  ( ( CHOICE /\ A e. V ) -> AC_ A = _V )