# Metamath Proof Explorer

## Theorem bj-ismoored

Description: Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021)

Ref Expression
Hypotheses bj-ismoored.1 ${⊢}{\phi }\to {A}\in \underset{_}{\mathrm{Moore}}$
bj-ismoored.2 ${⊢}{\phi }\to {B}\subseteq {A}$
Assertion bj-ismoored ${⊢}{\phi }\to \bigcup {A}\cap \bigcap {B}\in {A}$

### Proof

Step Hyp Ref Expression
1 bj-ismoored.1 ${⊢}{\phi }\to {A}\in \underset{_}{\mathrm{Moore}}$
2 bj-ismoored.2 ${⊢}{\phi }\to {B}\subseteq {A}$
3 inteq ${⊢}{x}={B}\to \bigcap {x}=\bigcap {B}$
4 3 ineq2d ${⊢}{x}={B}\to \bigcup {A}\cap \bigcap {x}=\bigcup {A}\cap \bigcap {B}$
5 4 eleq1d ${⊢}{x}={B}\to \left(\bigcup {A}\cap \bigcap {x}\in {A}↔\bigcup {A}\cap \bigcap {B}\in {A}\right)$
6 bj-ismoore ${⊢}{A}\in \underset{_}{\mathrm{Moore}}↔\forall {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\bigcup {A}\cap \bigcap {x}\in {A}$
7 1 6 sylib ${⊢}{\phi }\to \forall {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\bigcup {A}\cap \bigcap {x}\in {A}$
8 1 2 sselpwd ${⊢}{\phi }\to {B}\in 𝒫{A}$
9 5 7 8 rspcdva ${⊢}{\phi }\to \bigcup {A}\cap \bigcap {B}\in {A}$