mrccl

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

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

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2	1	mrcf	$⊢ C \in Moore (X) \to F : 𝒫 X ⟶ C$
3	2	adantr	$⊢ (C \in Moore (X) \land U \subseteq X) \to F : 𝒫 X ⟶ C$
4		mre1cl	$⊢ C \in Moore (X) \to X \in C$
5		elpw2g	$⊢ X \in C \to (U \in 𝒫 X \leftrightarrow U \subseteq X)$
6	4 5	syl	$⊢ C \in Moore (X) \to (U \in 𝒫 X \leftrightarrow U \subseteq X)$
7	6	biimpar	$⊢ (C \in Moore (X) \land U \subseteq X) \to U \in 𝒫 X$
8	3 7	ffvelcdmd	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) \in C$

Metamath Proof Explorer