Theorem fineqvomonb

Description: All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026)

	Ref	Expression
Assertion	fineqvomonb	⊢ ( Fin = V ↔ ω = On )

Proof

Step	Hyp	Ref	Expression
1		fineqvomon	⊢ ( Fin = V → ω = On )
2		onprc	⊢ ¬ On ∈ V
3		eleq1	⊢ ( ω = On → ( ω ∈ V ↔ On ∈ V ) )
4	2 3	mtbiri	⊢ ( ω = On → ¬ ω ∈ V )
5		fineqv	⊢ ( ¬ ω ∈ V ↔ Fin = V )
6	4 5	sylib	⊢ ( ω = On → Fin = V )
7	1 6	impbii	⊢ ( Fin = V ↔ ω = On )