# Metamath Proof Explorer

## Theorem ismred

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

Ref Expression
Hypotheses ismred.ss ${⊢}{\phi }\to {C}\subseteq 𝒫{X}$
ismred.ba ${⊢}{\phi }\to {X}\in {C}$
ismred.in ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to \bigcap {s}\in {C}$
Assertion ismred ${⊢}{\phi }\to {C}\in \mathrm{Moore}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 ismred.ss ${⊢}{\phi }\to {C}\subseteq 𝒫{X}$
2 ismred.ba ${⊢}{\phi }\to {X}\in {C}$
3 ismred.in ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to \bigcap {s}\in {C}$
4 velpw ${⊢}{s}\in 𝒫{C}↔{s}\subseteq {C}$
5 3 3expia ${⊢}\left({\phi }\wedge {s}\subseteq {C}\right)\to \left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)$
6 4 5 sylan2b ${⊢}\left({\phi }\wedge {s}\in 𝒫{C}\right)\to \left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)$
7 6 ralrimiva ${⊢}{\phi }\to \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)$
8 ismre ${⊢}{C}\in \mathrm{Moore}\left({X}\right)↔\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)$
9 1 2 7 8 syl3anbrc ${⊢}{\phi }\to {C}\in \mathrm{Moore}\left({X}\right)$