Theorem cldmreon

Description: The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Assertion	cldmreon	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldmre	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) )
4	1 3	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) )
5		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
6	5	fveq2d	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ( Moore ‘ 𝐵 ) = ( Moore ‘ ∪ 𝐽 ) )
7	4 6	eleqtrrd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝐵 ) )