mrcid

Description: The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015)

		Ref	Expression
	Hypothesis	mrcfval.f	$⊢ F = mrCls (C)$
	Assertion	mrcid	$⊢ (C \in Moore (X) \land U \in C) \to F (U) = U$

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2		mress	$⊢ (C \in Moore (X) \land U \in C) \to U \subseteq X$
3	1	mrcval	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$
4	2 3	syldan	$⊢ (C \in Moore (X) \land U \in C) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$
5		intmin	$⊢ U \in C \to ⋂ \{s \in C \| U \subseteq s\} = U$
6	5	adantl	$⊢ (C \in Moore (X) \land U \in C) \to ⋂ \{s \in C \| U \subseteq s\} = U$
7	4 6	eqtrd	$⊢ (C \in Moore (X) \land U \in C) \to F (U) = U$

Metamath Proof Explorer