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 FinVII = Fin

Proof

Step Hyp Ref Expression
1 axac3 CHOICE
2 dfacfin7 ( CHOICE ↔ FinVII = Fin )
3 1 2 mpbi FinVII = Fin