Theorem bj-mooreset

Description: A Moore collection is a set. Therefore, the class Moore_ of all Moore sets defined in df-bj-moore is actually the class of all Moore collections. This is also illustrated by the lack of sethood condition in bj-ismoore .

Note that the closed sets of a topology form a Moore collection, so a topology is a set, and this remark also applies to many other families of sets (namely, as soon as the whole set is required to be a set of the family, then the associated kind of family has no proper classes: that this condition suffices to impose sethood can be seen in this proof, which relies crucially on uniexr ).

Note: if, in the above predicate, we substitute ~P X for A , then the last e. ~P X could be weakened to C_ X , and then the predicate would be obviously satisfied since |- U. ~P X = X ( unipw ) , making ~P X a Moore collection in this weaker sense, for any class X , even proper, but the addition of this single case does not add anything interesting. Instead, we have the biconditional bj-discrmoore . (Contributed by BJ, 8-Dec-2021)

	Ref	Expression
Assertion	bj-mooreset	$$⊢\forall x\in 𝒫A\bigcup A\cap \bigcap x\in A\to A\in \mathrm{V}$$

Proof

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