Metamath Proof Explorer

Theorem fin71num

Description: A well-orderable set is VII-finite iff it is I-finite. Thus, even without choice, on the class of well-orderable sets all eight definitions of finite set coincide. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	fin71num	$⊢ A \in dom card \to (A \in {Fin}^{VII} \leftrightarrow A \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		isfin7-2	$⊢ A \in dom card \to (A \in {Fin}^{VII} \leftrightarrow (A \in dom card \to A \in Fin))$
2		biimt	$⊢ A \in dom card \to (A \in Fin \leftrightarrow (A \in dom card \to A \in Fin))$
3	1 2	bitr4d	$⊢ A \in dom card \to (A \in {Fin}^{VII} \leftrightarrow A \in Fin)$