Theorem onint0

Description: The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	onint0	$$⊢A\subseteq \mathrm{On}\to \left(\bigcap A=\varnothing \leftrightarrow \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		eleq1	$$⊢\bigcap A=\varnothing \to \left(\bigcap A\in \mathrm{V}\leftrightarrow \varnothing \in \mathrm{V}\right)$$
3	1 2	mpbiri	$$⊢\bigcap A=\varnothing \to \bigcap A\in \mathrm{V}$$
4		intex	$$⊢A\ne \varnothing \leftrightarrow \bigcap A\in \mathrm{V}$$
5	3 4	sylibr	$$⊢\bigcap A=\varnothing \to A\ne \varnothing$$
6		onint	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in A$$
7	5 6	sylan2	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcap A=\varnothing \right)\to \bigcap A\in A$$
8		eleq1	$$⊢\bigcap A=\varnothing \to \left(\bigcap A\in A\leftrightarrow \varnothing \in A\right)$$
9	8	adantl	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcap A=\varnothing \right)\to \left(\bigcap A\in A\leftrightarrow \varnothing \in A\right)$$
10	7 9	mpbid	$$⊢\left(A\subseteq \mathrm{On}\wedge \bigcap A=\varnothing \right)\to \varnothing \in A$$
11	10	ex	$$⊢A\subseteq \mathrm{On}\to \left(\bigcap A=\varnothing \to \varnothing \in A\right)$$
12		int0el	$$⊢\varnothing \in A\to \bigcap A=\varnothing$$
13	11 12	impbid1	$$⊢A\subseteq \mathrm{On}\to \left(\bigcap A=\varnothing \leftrightarrow \varnothing \in A\right)$$