mreincl

Description: Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Assertion	mreincl	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to A \cap B \in C$

Step	Hyp	Ref	Expression
1		intprg	$⊢ (A \in C \land B \in C) \to ⋂ \{A, B\} = A \cap B$
2	1	3adant1	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to ⋂ \{A, B\} = A \cap B$
3		simp1	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to C \in Moore (X)$
4		prssi	$⊢ (A \in C \land B \in C) \to \{A, B\} \subseteq C$
5	4	3adant1	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to \{A, B\} \subseteq C$
6		prnzg	$⊢ A \in C \to \{A, B\} \neq \emptyset$
7	6	3ad2ant2	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to \{A, B\} \neq \emptyset$
8		mreintcl	$⊢ (C \in Moore (X) \land \{A, B\} \subseteq C \land \{A, B\} \neq \emptyset) \to ⋂ \{A, B\} \in C$
9	3 5 7 8	syl3anc	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to ⋂ \{A, B\} \in C$
10	2 9	eqeltrrd	$⊢ (C \in Moore (X) \land A \in C \land B \in C) \to A \cap B \in C$

Metamath Proof Explorer