# Metamath Proof Explorer

## Theorem bj-ismoored2

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}$
bj-ismoored2.3 ${⊢}{\phi }\to {B}\ne \varnothing$
Assertion bj-ismoored2 ${⊢}{\phi }\to \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 bj-ismoored2.3 ${⊢}{\phi }\to {B}\ne \varnothing$
4 intssuni2 ${⊢}\left({B}\subseteq {A}\wedge {B}\ne \varnothing \right)\to \bigcap {B}\subseteq \bigcup {A}$
5 2 3 4 syl2anc ${⊢}{\phi }\to \bigcap {B}\subseteq \bigcup {A}$
6 sseqin2 ${⊢}\bigcap {B}\subseteq \bigcup {A}↔\bigcup {A}\cap \bigcap {B}=\bigcap {B}$
7 5 6 sylib ${⊢}{\phi }\to \bigcup {A}\cap \bigcap {B}=\bigcap {B}$
8 1 2 bj-ismoored ${⊢}{\phi }\to \bigcup {A}\cap \bigcap {B}\in {A}$
9 7 8 eqeltrrd ${⊢}{\phi }\to \bigcap {B}\in {A}$