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

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	⊢ Fin^VII = Fin

Proof

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