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\leftrightarrow \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$$