Definition df-bj-moore 37945

Description: Define the class of Moore collections. This is indeed the class of all Moore collections since these all are sets, as proved in bj-mooreset 37943, and as illustrated by the lack of sethood condition in bj-ismoore 37946.

This is to df-mre 17717 (defining Moore) what df-top 23173 (defining Top) is to df-topon 23190 (defining TopOn).

For the sake of consistency, the function defined at df-mre 17717 should be denoted by "MooreOn".

Note: df-mre 17717 singles out the empty intersection. This is not necessary. It could be written instead ⊢ Moore = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝒫 𝑥 ∣ ∀𝑧 ∈ 𝒫 𝑦(𝑥 ∩ ∩ 𝑧) ∈ 𝑦}) and the equivalence of both definitions is proved by bj-0int 37942.

There is no added generality in defining a "Moore predicate" for arbitrary classes, since a Moore class satisfying such a predicate is automatically a set (see bj-mooreset 37943).

TODO: move to the main section. For many families of sets, one can define both the function associating to each set the set of families of that kind on it (like df-mre 17717 and df-topon 23190) or the class of all families of that kind, independent of a base set (like df-bj-moore 37945 or df-top 23173). In general, the former will be more useful and the extra generality of the latter is not necessary. Moore collections, however, are particular in that they are more ubiquitous and are used in a wide variety of applications (for many families of sets, the family of families of a given kind is often a Moore collection, for instance). Therefore, in the case of Moore families, having both definitions is useful.

(Contributed by BJ, 27-Apr-2021.)

Assertion

Ref	Expression
df-bj-moore	⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-moore

Step	Hyp	Ref	Expression
1		cmoore 37944	. 2 class Moore
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1569	. . . . . . 7 class 𝑥
4	3	cuni 4866	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1569	. . . . . . 7 class 𝑦
7	6	cint 4906	. . . . . 6 class ∩ 𝑦
8	4, 7	cin 3897	. . . . 5 class (∪ 𝑥 ∩ ∩ 𝑦)
9	8, 3	wcel 2145	. . . 4 wff (∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
10	3	cpw 4556	. . . 4 class 𝒫 𝑥
11	9, 5, 10	wral 3076	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
12	11, 2	cab 2738	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}
13	1, 12	wceq 1570	1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}

This definition is used by:  bj-ismoore  37946