Theorem ontri1

Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003)

	Ref	Expression
Assertion	ontri1	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\subseteq B\leftrightarrow \neg B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
3		ordtri1	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow \neg B\in A\right)$$
4	1 2 3	syl2an	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\subseteq B\leftrightarrow \neg B\in A\right)$$