Definition df-bj-moore 33943

Description: Define the class of Moore collections. This is to df-mre 16727 what df-top 21221 is to df-topon 21238. For the sake of consistency, the function defined at df-mre 16727 should be denoted by "MooreOn".

Note: df-mre 16727 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 33940.

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 33941). (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 33942	. 2 class Moore
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1507	. . . . . . 7 class 𝑥
4	3	cuni 4708	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1507	. . . . . . 7 class 𝑦
7	6	cint 4745	. . . . . 6 class ∩ 𝑦
8	4, 7	cin 3821	. . . . 5 class (∪ 𝑥 ∩ ∩ 𝑦)
9	8, 3	wcel 2051	. . . 4 wff (∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
10	3	cpw 4416	. . . 4 class 𝒫 𝑥
11	9, 5, 10	wral 3081	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
12	11, 2	cab 2751	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}
13	1, 12	wceq 1508	1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}

This definition is referenced by:  bj-ismoore  33944