mrerintcl

Description: The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015)

		Ref	Expression
	Assertion	mrerintcl	$⊢ (C \in Moore (X) \land S \subseteq C) \to X \cap ⋂ S \in C$

Step	Hyp	Ref	Expression
1		rint0	$⊢ S = \emptyset \to X \cap ⋂ S = X$
2	1	adantl	$⊢ ((C \in Moore (X) \land S \subseteq C) \land S = \emptyset) \to X \cap ⋂ S = X$
3		mre1cl	$⊢ C \in Moore (X) \to X \in C$
4	3	ad2antrr	$⊢ ((C \in Moore (X) \land S \subseteq C) \land S = \emptyset) \to X \in C$
5	2 4	eqeltrd	$⊢ ((C \in Moore (X) \land S \subseteq C) \land S = \emptyset) \to X \cap ⋂ S \in C$
6		simp2	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to S \subseteq C$
7		mresspw	$⊢ C \in Moore (X) \to C \subseteq 𝒫 X$
8	7	3ad2ant1	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to C \subseteq 𝒫 X$
9	6 8	sstrd	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to S \subseteq 𝒫 X$
10		simp3	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to S \neq \emptyset$
11		rintn0	$⊢ (S \subseteq 𝒫 X \land S \neq \emptyset) \to X \cap ⋂ S = ⋂ S$
12	9 10 11	syl2anc	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to X \cap ⋂ S = ⋂ S$
13		mreintcl	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to ⋂ S \in C$
14	12 13	eqeltrd	$⊢ (C \in Moore (X) \land S \subseteq C \land S \neq \emptyset) \to X \cap ⋂ S \in C$
15	14	3expa	$⊢ ((C \in Moore (X) \land S \subseteq C) \land S \neq \emptyset) \to X \cap ⋂ S \in C$
16	5 15	pm2.61dane	$⊢ (C \in Moore (X) \land S \subseteq C) \to X \cap ⋂ S \in C$

Metamath Proof Explorer