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	|- ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		0elpw	|- (/) e. ~P A
2		rint0	|- ( x = (/) -> ( U. A i^i |^| x ) = U. A )
3	2	eleq1d	|- ( x = (/) -> ( ( U. A i^i |^| x ) e. A <-> U. A e. A ) )
4	3	rspcv	|- ( (/) e. ~P A -> ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> U. A e. A ) )
5	1 4	ax-mp	|- ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> U. A e. A )
6		uniexr	|- ( U. A e. A -> A e. _V )
7	5 6	syl	|- ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> A e. _V )