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 \leftrightarrow {Fin}^{VII} = Fin$
3	1 2	mpbi	$⊢ {Fin}^{VII} = Fin$