Theorem 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 𝐴 → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
2		onfin	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )
3		onprc	⊢ ¬ On ∈ V
4		elex	⊢ ( On ∈ Fin → On ∈ V )
5	3 4	mto	⊢ ¬ On ∈ Fin
6		eleq1	⊢ ( 𝐴 = On → ( 𝐴 ∈ Fin ↔ On ∈ Fin ) )
7	5 6	mtbiri	⊢ ( 𝐴 = On → ¬ 𝐴 ∈ Fin )
8		elex	⊢ ( On ∈ ω → On ∈ V )
9	3 8	mto	⊢ ¬ On ∈ ω
10		eleq1	⊢ ( 𝐴 = On → ( 𝐴 ∈ ω ↔ On ∈ ω ) )
11	9 10	mtbiri	⊢ ( 𝐴 = On → ¬ 𝐴 ∈ ω )
12	7 11	2falsed	⊢ ( 𝐴 = On → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )
13	2 12	jaoi	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )
14	1 13	sylbi	⊢ ( Ord 𝐴 → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )