Metamath Proof Explorer

Theorem dfacfin7

Description: Axiom of Choice equivalent: the VII-finite sets are the same as I-finite sets. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion dfacfin7 
|- ( CHOICE <-> Fin7 = Fin )

Proof

Step Hyp Ref Expression
1 ssequn2 
 |-  ( ( _V \ dom card ) C_ Fin <-> ( Fin u. ( _V \ dom card ) ) = Fin )
2 dfac10 
 |-  ( CHOICE <-> dom card = _V )
3 finnum 
 |-  ( x e. Fin -> x e. dom card )
4 3 ssriv 
 |-  Fin C_ dom card
5 ssequn2 
 |-  ( Fin C_ dom card <-> ( dom card u. Fin ) = dom card )
6 4 5 mpbi 
 |-  ( dom card u. Fin ) = dom card
7 6 eqeq1i 
 |-  ( ( dom card u. Fin ) = _V <-> dom card = _V )
8 2 7 bitr4i 
 |-  ( CHOICE <-> ( dom card u. Fin ) = _V )
9 ssv 
 |-  ( dom card u. Fin ) C_ _V
10 eqss 
 |-  ( ( dom card u. Fin ) = _V <-> ( ( dom card u. Fin ) C_ _V /\ _V C_ ( dom card u. Fin ) ) )
11 9 10 mpbiran 
 |-  ( ( dom card u. Fin ) = _V <-> _V C_ ( dom card u. Fin ) )
12 ssundif 
 |-  ( _V C_ ( dom card u. Fin ) <-> ( _V \ dom card ) C_ Fin )
13 8 11 12 3bitri 
 |-  ( CHOICE <-> ( _V \ dom card ) C_ Fin )
14 dffin7-2 
 |-  Fin7 = ( Fin u. ( _V \ dom card ) )
15 14 eqeq1i 
 |-  ( Fin7 = Fin <-> ( Fin u. ( _V \ dom card ) ) = Fin )
16 1 13 15 3bitr4i 
 |-  ( CHOICE <-> Fin7 = Fin )