ismred

Description: Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	ismred.ss	$⊢ φ \to C \subseteq 𝒫 X$
	ismred.ba	$⊢ φ \to X \in C$
	ismred.in	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to ⋂ s \in C$
Assertion	ismred	$⊢ φ \to C \in Moore (X)$

Step	Hyp	Ref	Expression
1		ismred.ss	$⊢ φ \to C \subseteq 𝒫 X$
2		ismred.ba	$⊢ φ \to X \in C$
3		ismred.in	$⊢ (φ \land s \subseteq C \land s \neq \emptyset) \to ⋂ s \in C$
4		velpw	$⊢ s \in 𝒫 C \leftrightarrow s \subseteq C$
5	3	3expia	$⊢ (φ \land s \subseteq C) \to (s \neq \emptyset \to ⋂ s \in C)$
6	4 5	sylan2b	$⊢ (φ \land s \in 𝒫 C) \to (s \neq \emptyset \to ⋂ s \in C)$
7	6	ralrimiva	$⊢ φ \to \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)$
8		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))$
9	1 2 7 8	syl3anbrc	$⊢ φ \to C \in Moore (X)$

Metamath Proof Explorer