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 \neq \emptyset \leftrightarrow ⋂ A \in V$

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

Metamath Proof Explorer