Metamath Proof Explorer


Theorem fin71ac

Description: Once we allow AC, the "strongest" definition of finite set becomes equivalent to the "weakest" and the entire hierarchy collapses. (Contributed by Stefan O'Rear, 29-Oct-2014)

Ref Expression
Assertion fin71ac
|- Fin7 = Fin

Proof

Step Hyp Ref Expression
1 axac3
 |-  CHOICE
2 dfacfin7
 |-  ( CHOICE <-> Fin7 = Fin )
3 1 2 mpbi
 |-  Fin7 = Fin