Theorem fineqvomon

Description: If the Axiom of Infinity is negated, then the class of all natural numbers equals the proper class of all ordinal numbers. (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	fineqvomon	⊢ ( Fin = V → ω = On )

Proof

Step	Hyp	Ref	Expression
1		onfin2	⊢ ω = ( On ∩ Fin )
2		ineq2	⊢ ( Fin = V → ( On ∩ Fin ) = ( On ∩ V ) )
3		inv1	⊢ ( On ∩ V ) = On
4	2 3	eqtrdi	⊢ ( Fin = V → ( On ∩ Fin ) = On )
5	1 4	eqtrid	⊢ ( Fin = V → ω = On )