Theorem oninton

Description: The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of TakeutiZaring p. 44. (Contributed by NM, 29-Jan-1997)

	Ref	Expression
Assertion	oninton	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		onint	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in A$$
2	1	ex	$$⊢A\subseteq \mathrm{On}\to \left(A\ne \varnothing \to \bigcap A\in A\right)$$
3		ssel	$$⊢A\subseteq \mathrm{On}\to \left(\bigcap A\in A\to \bigcap A\in \mathrm{On}\right)$$
4	2 3	syld	$$⊢A\subseteq \mathrm{On}\to \left(A\ne \varnothing \to \bigcap A\in \mathrm{On}\right)$$
5	4	imp	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in \mathrm{On}$$