Theorem 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	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrccl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	mrcf	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
3	2	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
4		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
5		elpw2g	⊢ ( 𝑋 ∈ 𝐶 → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
6	4 5	syl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
7	6	biimpar	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ∈ 𝒫 𝑋 )
8	3 7	ffvelcdmd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 )