Theorem intex

Description: The intersection of a nonempty class exists. Exercise 5 of TakeutiZaring p. 44 and its converse. (Contributed by NM, 13-Aug-2002)

	Ref	Expression
Assertion	intex	$$⊢A\ne \varnothing \leftrightarrow \bigcap A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		intss1	$$⊢x\in A\to \bigcap A\subseteq x$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	ssex	$$⊢\bigcap A\subseteq x\to \bigcap A\in \mathrm{V}$$
5	2 4	syl	$$⊢x\in A\to \bigcap A\in \mathrm{V}$$
6	5	exlimiv	$$⊢\exists xx\in A\to \bigcap A\in \mathrm{V}$$
7	1 6	sylbi	$$⊢A\ne \varnothing \to \bigcap A\in \mathrm{V}$$
8		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
9		inteq	$$⊢A=\varnothing \to \bigcap A=\bigcap \varnothing$$
10		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
11	9 10	eqtrdi	$$⊢A=\varnothing \to \bigcap A=\mathrm{V}$$
12	11	eleq1d	$$⊢A=\varnothing \to \left(\bigcap A\in \mathrm{V}\leftrightarrow \mathrm{V}\in \mathrm{V}\right)$$
13	8 12	mtbiri	$$⊢A=\varnothing \to \neg \bigcap A\in \mathrm{V}$$
14	13	necon2ai	$$⊢\bigcap A\in \mathrm{V}\to A\ne \varnothing$$
15	7 14	impbii	$$⊢A\ne \varnothing \leftrightarrow \bigcap A\in \mathrm{V}$$