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	⊢ ( ω ∈ On ⊻ ω = On )

Proof

Step	Hyp	Ref	Expression
1		omon	⊢ ( ω ∈ On ∨ ω = On )
2		onprc	⊢ ¬ On ∈ V
3		prcnel	⊢ ( ¬ On ∈ V → ¬ On ∈ On )
4	2 3	ax-mp	⊢ ¬ On ∈ On
5		eleq1	⊢ ( ω = On → ( ω ∈ On ↔ On ∈ On ) )
6	4 5	mtbiri	⊢ ( ω = On → ¬ ω ∈ On )
7	6	con2i	⊢ ( ω ∈ On → ¬ ω = On )
8		imnan	⊢ ( ( ω ∈ On → ¬ ω = On ) ↔ ¬ ( ω ∈ On ∧ ω = On ) )
9	7 8	mpbi	⊢ ¬ ( ω ∈ On ∧ ω = On )
10		xor2	⊢ ( ( ω ∈ On ⊻ ω = On ) ↔ ( ( ω ∈ On ∨ ω = On ) ∧ ¬ ( ω ∈ On ∧ ω = On ) ) )
11	1 9 10	mpbir2an	⊢ ( ω ∈ On ⊻ ω = On )