mreintcl

Description: A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Assertion	mreintcl	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to ⋂ S \in C$

Step	Hyp	Ref	Expression
1		elpw2g	$⊢ C \in Moore (X) \to (S \in 𝒫 C \leftrightarrow S \subseteq C)$
2	1	biimpar	$⊢ (C \in Moore (X) \land S \subseteq C) \to S \in 𝒫 C$
3	2	3adant3	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to S \in 𝒫 C$
4		ismre	$⊢ C \in Moore (X) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))$
5	4	simp3bi	$⊢ C \in Moore (X) \to \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)$
6	5	3ad2ant1	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)$
7		simp3	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to S \neq \emptyset$
8		neeq1	$⊢ s = S \to (s \neq \emptyset \leftrightarrow S \neq \emptyset)$
9		inteq	$⊢ s = S \to ⋂ s = ⋂ S$
10	9	eleq1d	$⊢ s = S \to (⋂ s \in C \leftrightarrow ⋂ S \in C)$
11	8 10	imbi12d	$⊢ s = S \to ((s \neq \emptyset \to ⋂ s \in C) \leftrightarrow (S \neq \emptyset \to ⋂ S \in C))$
12	11	rspcva	$⊢ (S \in 𝒫 C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)) \to (S \neq \emptyset \to ⋂ S \in C)$
13	12	3impia	$⊢ (S \in 𝒫 C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C) \land S \neq \emptyset) \to ⋂ S \in C$
14	3 6 7 13	syl3anc	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to ⋂ S \in C$

Metamath Proof Explorer