cldmre

Description: The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	cldmre	$⊢ J \in Top \to Clsd (J) \in Moore (X)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	cldss2	$⊢ Clsd (J) \subseteq 𝒫 X$
3	2	a1i	$⊢ J \in Top \to Clsd (J) \subseteq 𝒫 X$
4	1	topcld	$⊢ J \in Top \to X \in Clsd (J)$
5		intcld	$⊢ (x \neq \emptyset \land x \subseteq Clsd (J)) \to ⋂ x \in Clsd (J)$
6	5	ancoms	$⊢ (x \subseteq Clsd (J) \land x \neq \emptyset) \to ⋂ x \in Clsd (J)$
7	6	3adant1	$⊢ (J \in Top \land x \subseteq Clsd (J) \land x \neq \emptyset) \to ⋂ x \in Clsd (J)$
8	3 4 7	ismred	$⊢ J \in Top \to Clsd (J) \in Moore (X)$

Metamath Proof Explorer