Theorem bj-ismoore

Description: Characterization of Moore collections. Note that there is no sethood hypothesis on A : it is implied by either side (this is obvious for the LHS, and is the content of bj-mooreset for the RHS). (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-ismoore	$$⊢A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \underset{\_}{\mathrm{Moore}}\to A\in \mathrm{V}$$
2		bj-mooreset	$$⊢\forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\to A\in \mathrm{V}$$
3		pweq	$$⊢y=A\to 𝒫y=𝒫A$$
4		unieq	$$⊢y=A\to \bigcup y=\bigcup A$$
5	4	ineq1d	$$⊢y=A\to \bigcup y\cap \bigcap x=\bigcup A\cap \bigcap x$$
6		id	$$⊢y=A\to y=A$$
7	5 6	eleq12d	$$⊢y=A\to \left(\bigcup y\cap \bigcap x\in y\leftrightarrow \bigcup A\cap \bigcap x\in A\right)$$
8	3 7	raleqbidv	$$⊢y=A\to \left(\forall x\in 𝒫y\bigcup y\cap \bigcap x\in y\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\right)$$
9		df-bj-moore	$$⊢\underset{\_}{\mathrm{Moore}}=\left\{y|\forall x\in 𝒫y\bigcup y\cap \bigcap x\in y\right\}$$
10	8 9	elab2g	$$⊢A\in \mathrm{V}\to \left(A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\right)$$
11	1 2 10	pm5.21nii	$$⊢A\in \underset{\_}{\mathrm{Moore}}\leftrightarrow \forall x\in 𝒫A\bigcup A\cap \bigcap x\in A$$