Definition df-bj-moore 33058

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

Note: df-mre 16246 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 33055.

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 33056). (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 33057	. 2 class Moore
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1482	. . . . . . 7 class 𝑥
4	3	cuni 4436	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1482	. . . . . . 7 class 𝑦
7	6	cint 4475	. . . . . 6 class ∩ 𝑦
8	4, 7	cin 3573	. . . . 5 class (∪ 𝑥 ∩ ∩ 𝑦)
9	8, 3	wcel 1990	. . . 4 wff (∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
10	3	cpw 4158	. . . 4 class 𝒫 𝑥
11	9, 5, 10	wral 2912	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
12	11, 2	cab 2608	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}
13	1, 12	wceq 1483	1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}

This definition is referenced by:  bj-ismoore  33059