Theorem bj-ismooredr

Description: Sufficient condition to be a Moore collection. There is no sethood hypothesis on A : it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Hypothesis	bj-ismooredr.1	$$⊢\left(\phi \wedge x\subseteq A\right)\to \bigcup A\cap \bigcap x\in A$$
Assertion	bj-ismooredr	$$⊢\phi \to A\in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		bj-ismooredr.1	$$⊢\left(\phi \wedge x\subseteq A\right)\to \bigcup A\cap \bigcap x\in A$$
2		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
3	1	ex	$$⊢\phi \to \left(x\subseteq A\to \bigcup A\cap \bigcap x\in A\right)$$
4	2 3	syl5	$$⊢\phi \to \left(x\in 𝒫A\to \bigcup A\cap \bigcap x\in A\right)$$
5	4	ralrimiv	$$⊢\phi \to \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$
6		bj-ismoore	$$⊢A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$
7	5 6	sylibr	$$⊢\phi \to A\in \underset{\_}{\mathrm{Moore}}$$