Theorem xoromon

Description: _om is either an ordinal set or the proper class of all ordinal sets, but not both. This is a stronger version of omon . (Contributed by BTernaryTau, 25-Jan-2026)

	Ref	Expression
Assertion	xoromon	|- ( _om e. On \/_ _om = On )

Proof

Step	Hyp	Ref	Expression
1		omon	|- ( _om e. On \/ _om = On )
2		onprc	|- -. On e. _V
3		prcnel	|- ( -. On e. _V -> -. On e. On )
4	2 3	ax-mp	|- -. On e. On
5		eleq1	|- ( _om = On -> ( _om e. On <-> On e. On ) )
6	4 5	mtbiri	|- ( _om = On -> -. _om e. On )
7	6	con2i	|- ( _om e. On -> -. _om = On )
8		imnan	|- ( ( _om e. On -> -. _om = On ) <-> -. ( _om e. On /\ _om = On ) )
9	7 8	mpbi	|- -. ( _om e. On /\ _om = On )
10		xor2	|- ( ( _om e. On \/_ _om = On ) <-> ( ( _om e. On \/ _om = On ) /\ -. ( _om e. On /\ _om = On ) ) )
11	1 9 10	mpbir2an	|- ( _om e. On \/_ _om = On )