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 35923
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 35921, and as illustrated by the lack of sethood condition in bj-ismoore 35924.

This is to df-mre 17526 (defining Moore) what df-top 22378 (defining Top) is to df-topon 22395 (defining TopOn).

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

Note: df-mre 17526 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 35920.

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 35921).

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 17526 and df-topon 22395) or the class of all families of that kind, independent of a base set (like df-bj-moore 35923 or df-top 22378). 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
StepHypRef Expression
1 cmoore 35922 . 2 class Moore
2 vx . . . . . . . 8 setvar 𝑥
32cv 1541 . . . . . . 7 class 𝑥
43cuni 4907 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1541 . . . . . . 7 class 𝑦
76cint 4949 . . . . . 6 class 𝑦
84, 7cin 3946 . . . . 5 class ( 𝑥 𝑦)
98, 3wcel 2107 . . . 4 wff ( 𝑥 𝑦) ∈ 𝑥
103cpw 4601 . . . 4 class 𝒫 𝑥
119, 5, 10wral 3062 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥
1211, 2cab 2710 . 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥}
131, 12wceq 1542 1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 𝑦) ∈ 𝑥}
Colors of variables: wff setvar class
This definition is referenced by:  bj-ismoore  35924
  Copyright terms: Public domain W3C validator