Theorem onssmin

Description: A nonempty class of ordinal numbers has the smallest member. Exercise 9 of TakeutiZaring p. 40. (Contributed by NM, 3-Oct-2003)

	Ref	Expression
Assertion	onssmin	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\subseteq y$$

Proof

Step	Hyp	Ref	Expression
1		onint	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in A$$
2		intss1	$$⊢y\in A\to \bigcap A\subseteq y$$
3	2	rgen	$$⊢\forall y\in A\bigcap A\subseteq y$$
4		sseq1	$$⊢x=\bigcap A\to \left(x\subseteq y\leftrightarrow \bigcap A\subseteq y\right)$$
5	4	ralbidv	$$⊢x=\bigcap A\to \left(\forall y\in Ax\subseteq y\leftrightarrow \forall y\in A\bigcap A\subseteq y\right)$$
6	5	rspcev	$$⊢\left(\bigcap A\in A\wedge \forall y\in A\bigcap A\subseteq y\right)\to \exists x\in A\forall y\in Ax\subseteq y$$
7	1 3 6	sylancl	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\subseteq y$$