Theorem bj-ismoored0

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

	Ref	Expression
Assertion	bj-ismoored0	$$⊢A\in \underset{\_}{\mathrm{Moore}}\to \bigcup A\in A$$

Proof

Step	Hyp	Ref	Expression
1		bj-ismoore	$$⊢A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$
2		0elpw	$$⊢\varnothing \in 𝒫A$$
3		rint0	$$⊢x=\varnothing \to \bigcup A\cap \bigcap x=\bigcup A$$
4	3	eleq1d	$$⊢x=\varnothing \to \left(\bigcup A\cap \bigcap x\in A\leftrightarrow \bigcup A\in A\right)$$
5	4	rspcv	$$⊢\varnothing \in 𝒫A\to \left(\forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\to \bigcup A\in A\right)$$
6	2 5	ax-mp	$$⊢\forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\to \bigcup A\in A$$
7	1 6	sylbi	$$⊢A\in \underset{\_}{\mathrm{Moore}}\to \bigcup A\in A$$