ordfin

Description: A generalization of onfin to include the class of all ordinals. (Contributed by Scott Fenton, 19-Feb-2026)

		Ref	Expression
	Assertion	ordfin	$⊢ Ord A \to (A \in Fin \leftrightarrow A \in ω)$

Step	Hyp	Ref	Expression
1		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
2		onfin	$⊢ A \in On \to (A \in Fin \leftrightarrow A \in ω)$
3		onprc	$⊢ \neg On \in V$
4		elex	$⊢ On \in Fin \to On \in V$
5	3 4	mto	$⊢ \neg On \in Fin$
6		eleq1	$⊢ A = On \to (A \in Fin \leftrightarrow On \in Fin)$
7	5 6	mtbiri	$⊢ A = On \to \neg A \in Fin$
8		elex	$⊢ On \in ω \to On \in V$
9	3 8	mto	$⊢ \neg On \in ω$
10		eleq1	$⊢ A = On \to (A \in ω \leftrightarrow On \in ω)$
11	9 10	mtbiri	$⊢ A = On \to \neg A \in ω$
12	7 11	2falsed	$⊢ A = On \to (A \in Fin \leftrightarrow A \in ω)$
13	2 12	jaoi	$⊢ (A \in On \lor A = On) \to (A \in Fin \leftrightarrow A \in ω)$
14	1 13	sylbi	$⊢ Ord A \to (A \in Fin \leftrightarrow A \in ω)$

Metamath Proof Explorer