This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mre1cl

Description: In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Assertion	mre1cl	$⊢ C \in Moore (X) \to X \in C$

Step	Hyp	Ref	Expression
1		ismre	$⊢ C \in Moore (X) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))$
2	1	simp2bi	$⊢ C \in Moore (X) \to X \in C$