Theorem mrccls

Description: Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrccls.f	⊢ 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) )
Assertion	mrccls	⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		mrccls.f	⊢ 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	clsfval	⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) )
4	2	cldmre	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) )
5	1	mrcfval	⊢ ( ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) → 𝐹 = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) )
6	4 5	syl	⊢ ( 𝐽 ∈ Top → 𝐹 = ( 𝑎 ∈ 𝒫 ∪ 𝐽 ↦ ∩ { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎 ⊆ 𝑏 } ) )
7	3 6	eqtr4d	⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 )