Theorem onssneli

Description: An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994)

	Ref	Expression
Hypothesis	on.1	$$⊢A\in \mathrm{On}$$
Assertion	onssneli	$$⊢A\subseteq B\to \neg B\in A$$

Proof

Step	Hyp	Ref	Expression
1		on.1	$$⊢A\in \mathrm{On}$$
2		ssel	$$⊢A\subseteq B\to \left(B\in A\to B\in B\right)$$
3	1	oneli	$$⊢B\in A\to B\in \mathrm{On}$$
4		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
5		ordirr	$$⊢\mathrm{Ord}B\to \neg B\in B$$
6	3 4 5	3syl	$$⊢B\in A\to \neg B\in B$$
7	2 6	nsyli	$$⊢A\subseteq B\to \left(B\in A\to \neg B\in A\right)$$
8	7	pm2.01d	$$⊢A\subseteq B\to \neg B\in A$$