Theorem onnmin

Description: No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997)

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

Proof

Step	Hyp	Ref	Expression
1		intss1	$$⊢B\in A\to \bigcap A\subseteq B$$
2	1	adantl	$$⊢\left(A\subseteq \mathrm{On}\wedge B\in A\right)\to \bigcap A\subseteq B$$
3		ne0i	$$⊢B\in A\to A\ne \varnothing$$
4		oninton	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in \mathrm{On}$$
5	3 4	sylan2	$$⊢\left(A\subseteq \mathrm{On}\wedge B\in A\right)\to \bigcap A\in \mathrm{On}$$
6		ssel2	$$⊢\left(A\subseteq \mathrm{On}\wedge B\in A\right)\to B\in \mathrm{On}$$
7		ontri1	$$⊢\left(\bigcap A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\bigcap A\subseteq B\leftrightarrow \neg B\in \bigcap A\right)$$
8	5 6 7	syl2anc	$$⊢\left(A\subseteq \mathrm{On}\wedge B\in A\right)\to \left(\bigcap A\subseteq B\leftrightarrow \neg B\in \bigcap A\right)$$
9	2 8	mpbid	$$⊢\left(A\subseteq \mathrm{On}\wedge B\in A\right)\to \neg B\in \bigcap A$$