Metamath Proof Explorer

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	$⊢ (ω \in On ⊻ ω = On)$

Proof

Step	Hyp	Ref	Expression
1		omon	$⊢ (ω \in On \lor ω = On)$
2		onprc	$⊢ \neg On \in V$
3		prcnel	$⊢ \neg On \in V \to \neg On \in On$
4	2 3	ax-mp	$⊢ \neg On \in On$
5		eleq1	$⊢ ω = On \to (ω \in On \leftrightarrow On \in On)$
6	4 5	mtbiri	$⊢ ω = On \to \neg ω \in On$
7	6	con2i	$⊢ ω \in On \to \neg ω = On$
8		imnan	$⊢ (ω \in On \to \neg ω = On) \leftrightarrow \neg (ω \in On \land ω = On)$
9	7 8	mpbi	$⊢ \neg (ω \in On \land ω = On)$
10		xor2	$⊢ (ω \in On ⊻ ω = On) \leftrightarrow ((ω \in On \lor ω = On) \land \neg (ω \in On \land ω = On))$
11	1 9 10	mpbir2an	$⊢ (ω \in On ⊻ ω = On)$