Definition df-bj-mre 32249

Description: Define the class of Moore collections. This is to df-mre 16069 what df-top 20521 is to df-topon 20523.

Note: df-mre 16069 singles out the empty intersection. This is not necessary. It could be written instead Moore = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝒫 𝑥 ∣ ∀𝑧 ∈ 𝒫 𝑦(𝑥 ∩ ∩ 𝑧) ∈ 𝑦})

Remark: as usual, if one wanted a more general definition, one could define a new syntax and (Moore𝐴 ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴). (Contributed by BJ, 27-Apr-2021.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-mre

Step	Hyp	Ref	Expression
1		cmoo 32248	. 2 class Moore
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1474	. . . . . . 7 class 𝑥
4	3	cuni 4372	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1474	. . . . . . 7 class 𝑦
7	6	cint 4410	. . . . . 6 class ∩ 𝑦
8	4, 7	cin 3539	. . . . 5 class (∪ 𝑥 ∩ ∩ 𝑦)
9	8, 3	wcel 1977	. . . 4 wff (∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
10	3	cpw 4108	. . . 4 class 𝒫 𝑥
11	9, 5, 10	wral 2896	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥
12	11, 2	cab 2596	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}
13	1, 12	wceq 1475	1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}

This definition is referenced by: (None)