# Metamath Proof Explorer

## Theorem bj-ismooredr

Description: Sufficient condition to be a Moore collection. Note that there is no sethood hypothesis on A : it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021)

Ref Expression
Hypothesis bj-ismooredr.1 ${⊢}\left({\phi }\wedge {x}\subseteq {A}\right)\to \bigcup {A}\cap \bigcap {x}\in {A}$
Assertion bj-ismooredr ${⊢}{\phi }\to {A}\in \underset{_}{\mathrm{Moore}}$

### Proof

Step Hyp Ref Expression
1 bj-ismooredr.1 ${⊢}\left({\phi }\wedge {x}\subseteq {A}\right)\to \bigcup {A}\cap \bigcap {x}\in {A}$
2 elpwi ${⊢}{x}\in 𝒫{A}\to {x}\subseteq {A}$
3 1 ex ${⊢}{\phi }\to \left({x}\subseteq {A}\to \bigcup {A}\cap \bigcap {x}\in {A}\right)$
4 2 3 syl5 ${⊢}{\phi }\to \left({x}\in 𝒫{A}\to \bigcup {A}\cap \bigcap {x}\in {A}\right)$
5 4 ralrimiv ${⊢}{\phi }\to \forall {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\bigcup {A}\cap \bigcap {x}\in {A}$
6 bj-ismoore ${⊢}{A}\in \underset{_}{\mathrm{Moore}}↔\forall {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\bigcup {A}\cap \bigcap {x}\in {A}$
7 5 6 sylibr ${⊢}{\phi }\to {A}\in \underset{_}{\mathrm{Moore}}$