Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-moore Structured version   Visualization version   GIF version

Definition df-bj-moore 33390
Description: Define the class of Moore collections. This is to df-mre 16454 what df-top 20919 is to df-topon 20936. For the sake of consistency, the function defined at df-mre 16454 should be denoted by "MooreOn".

Note: df-mre 16454 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 33387.

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 33388). (Contributed by BJ, 27-Apr-2021.)

Assertion
Ref Expression
df-bj-moore Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-moore
StepHypRef Expression
1 cmoore 33389 . 2 class Moore
2 vx . . . . . . . 8 setvar 𝑥
32cv 1630 . . . . . . 7 class 𝑥
43cuni 4575 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1630 . . . . . . 7 class 𝑦
76cint 4612 . . . . . 6 class 𝑦
84, 7cin 3722 . . . . 5 class ( 𝑥 𝑦)
98, 3wcel 2145 . . . 4 wff ( 𝑥 𝑦) ∈ 𝑥
103cpw 4298 . . . 4 class 𝒫 𝑥
119, 5, 10wral 3061 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥
1211, 2cab 2757 . 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥}
131, 12wceq 1631 1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥}
Colors of variables: wff setvar class
This definition is referenced by:  bj-ismoore  33391
  Copyright terms: Public domain W3C validator