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\leftrightarrow \bigcup A\cap \bigcap B\in A\right)$$
6		bj-ismoore	$$⊢A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$
7	1 6	sylib	$$⊢\phi \to \forall x\in 𝒫A\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$$