Theorem fineqvomon

Description: If all sets are finite, 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	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{\omega }=\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
2		ineq2	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{On}\cap \mathrm{Fin}=\mathrm{On}\cap \mathrm{V}$$
3		inv1	$$⊢\mathrm{On}\cap \mathrm{V}=\mathrm{On}$$
4	2 3	eqtrdi	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{On}\cap \mathrm{Fin}=\mathrm{On}$$
5	1 4	eqtrid	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{\omega }=\mathrm{On}$$