Theorem unissint

Description: If the union of a class is included in its intersection, the class is either the empty set or a singleton ( uniintsn ). (Contributed by NM, 30-Oct-2010) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	unissint	$$⊢\bigcup A\subseteq \bigcap A\leftrightarrow \left(A=\varnothing \vee \bigcup A=\bigcap A\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\bigcup A\subseteq \bigcap A\wedge \neg A=\varnothing \right)\to \bigcup A\subseteq \bigcap A$$
2		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
3		intssuni	$$⊢A\ne \varnothing \to \bigcap A\subseteq \bigcup A$$
4	2 3	sylbir	$$⊢\neg A=\varnothing \to \bigcap A\subseteq \bigcup A$$
5	4	adantl	$$⊢\left(\bigcup A\subseteq \bigcap A\wedge \neg A=\varnothing \right)\to \bigcap A\subseteq \bigcup A$$
6	1 5	eqssd	$$⊢\left(\bigcup A\subseteq \bigcap A\wedge \neg A=\varnothing \right)\to \bigcup A=\bigcap A$$
7	6	ex	$$⊢\bigcup A\subseteq \bigcap A\to \left(\neg A=\varnothing \to \bigcup A=\bigcap A\right)$$
8	7	orrd	$$⊢\bigcup A\subseteq \bigcap A\to \left(A=\varnothing \vee \bigcup A=\bigcap A\right)$$
9		ssv	$$⊢\bigcup A\subseteq \mathrm{V}$$
10		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
11	9 10	sseqtrri	$$⊢\bigcup A\subseteq \bigcap \varnothing$$
12		inteq	$$⊢A=\varnothing \to \bigcap A=\bigcap \varnothing$$
13	11 12	sseqtrrid	$$⊢A=\varnothing \to \bigcup A\subseteq \bigcap A$$
14		eqimss	$$⊢\bigcup A=\bigcap A\to \bigcup A\subseteq \bigcap A$$
15	13 14	jaoi	$$⊢\left(A=\varnothing \vee \bigcup A=\bigcap A\right)\to \bigcup A\subseteq \bigcap A$$
16	8 15	impbii	$$⊢\bigcup A\subseteq \bigcap A\leftrightarrow \left(A=\varnothing \vee \bigcup A=\bigcap A\right)$$