Theorem ordprcon

Description: If an ordinal class is not a set, then it must be the proper class of all ordinals. (Contributed by BTernaryTau, 9-Jun-2026)

	Ref	Expression
Assertion	ordprcon	|- ( ( Ord A /\ -. A e. _V ) -> A = On )

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	|- ( Ord A <-> ( A e. On \/ A = On ) )
2	1	birani	|- ( ( Ord A /\ -. A e. _V ) -> ( A e. On \/ A = On ) )
3		prcnel	|- ( -. A e. _V -> -. A e. On )
4	3	adantl	|- ( ( Ord A /\ -. A e. _V ) -> -. A e. On )
5	2 4	orcnd	|- ( ( Ord A /\ -. A e. _V ) -> A = On )