Theorem bj-discrmoore

Description: The powerclass ~P A is a Moore collection if and only if A is a set. It is then called the discrete Moore collection. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-discrmoore	$$⊢A\in \mathrm{V}\leftrightarrow 𝒫A\in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		unipw	$$⊢\bigcup 𝒫A=A$$
2	1	ineq1i	$$⊢\bigcup 𝒫A\cap \bigcap x=A\cap \bigcap x$$
3		inex1g	$$⊢A\in \mathrm{V}\to A\cap \bigcap x\in \mathrm{V}$$
4		inss1	$$⊢A\cap \bigcap x\subseteq A$$
5	4	a1i	$$⊢A\in \mathrm{V}\to A\cap \bigcap x\subseteq A$$
6	3 5	elpwd	$$⊢A\in \mathrm{V}\to A\cap \bigcap x\in 𝒫A$$
7	2 6	eqeltrid	$$⊢A\in \mathrm{V}\to \bigcup 𝒫A\cap \bigcap x\in 𝒫A$$
8	7	adantr	$$⊢\left(A\in \mathrm{V}\wedge x\subseteq 𝒫A\right)\to \bigcup 𝒫A\cap \bigcap x\in 𝒫A$$
9	8	bj-ismooredr	$$⊢A\in \mathrm{V}\to 𝒫A\in \underset{\_}{\mathrm{Moore}}$$
10		pwexr	$$⊢𝒫A\in \underset{\_}{\mathrm{Moore}}\to A\in \mathrm{V}$$
11	9 10	impbii	$$⊢A\in \mathrm{V}\leftrightarrow 𝒫A\in \underset{\_}{\mathrm{Moore}}$$