iin0

Description: An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005)

		Ref	Expression
	Assertion	iin0	$⊢ A \neq \emptyset \leftrightarrow ⋂_{x \in A} \emptyset = \emptyset$

Step	Hyp	Ref	Expression
1		iinconst	$⊢ A \neq \emptyset \to ⋂_{x \in A} \emptyset = \emptyset$
2		0ex	$⊢ \emptyset \in V$
3	2	n0ii	$⊢ \neg V = \emptyset$
4		0iin	$⊢ ⋂_{x \in \emptyset} \emptyset = V$
5	4	eqeq1i	$⊢ ⋂_{x \in \emptyset} \emptyset = \emptyset \leftrightarrow V = \emptyset$
6	3 5	mtbir	$⊢ \neg ⋂_{x \in \emptyset} \emptyset = \emptyset$
7		iineq1	$⊢ A = \emptyset \to ⋂_{x \in A} \emptyset = ⋂_{x \in \emptyset} \emptyset$
8	7	eqeq1d	$⊢ A = \emptyset \to (⋂_{x \in A} \emptyset = \emptyset \leftrightarrow ⋂_{x \in \emptyset} \emptyset = \emptyset)$
9	6 8	mtbiri	$⊢ A = \emptyset \to \neg ⋂_{x \in A} \emptyset = \emptyset$
10	9	necon2ai	$⊢ ⋂_{x \in A} \emptyset = \emptyset \to A \neq \emptyset$
11	1 10	impbii	$⊢ A \neq \emptyset \leftrightarrow ⋂_{x \in A} \emptyset = \emptyset$

Metamath Proof Explorer