Theorem intnex

Description: If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Assertion	intnex	$$⊢\neg \bigcap A\in \mathrm{V}\leftrightarrow \bigcap A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		intex	$$⊢A\ne \varnothing \leftrightarrow \bigcap A\in \mathrm{V}$$
2	1	necon1bbii	$$⊢\neg \bigcap A\in \mathrm{V}\leftrightarrow A=\varnothing$$
3		inteq	$$⊢A=\varnothing \to \bigcap A=\bigcap \varnothing$$
4		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
5	3 4	eqtrdi	$$⊢A=\varnothing \to \bigcap A=\mathrm{V}$$
6	2 5	sylbi	$$⊢\neg \bigcap A\in \mathrm{V}\to \bigcap A=\mathrm{V}$$
7		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
8		eleq1	$$⊢\bigcap A=\mathrm{V}\to \left(\bigcap A\in \mathrm{V}\leftrightarrow \mathrm{V}\in \mathrm{V}\right)$$
9	7 8	mtbiri	$$⊢\bigcap A=\mathrm{V}\to \neg \bigcap A\in \mathrm{V}$$
10	6 9	impbii	$$⊢\neg \bigcap A\in \mathrm{V}\leftrightarrow \bigcap A=\mathrm{V}$$