Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-moore | Structured version Visualization version GIF version |
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 34398,
and as illustrated by the lack of sethood condition in bj-ismoore 34401.
This is to df-mre 16860 (defining Moore) what df-top 21505 (defining Top) is to df-topon 21522 (defining TopOn). For the sake of consistency, the function defined at df-mre 16860 should be denoted by "MooreOn". Note: df-mre 16860 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 34397. 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 34398). 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 16860 and df-topon 21522) or the class of all families of that kind, independent of a base set (like df-bj-moore 34400 or df-top 21505). 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.) |
Ref | Expression |
---|---|
df-bj-moore | ⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmoore 34399 | . 2 class Moore | |
2 | vx | . . . . . . . 8 setvar 𝑥 | |
3 | 2 | cv 1535 | . . . . . . 7 class 𝑥 |
4 | 3 | cuni 4841 | . . . . . 6 class ∪ 𝑥 |
5 | vy | . . . . . . . 8 setvar 𝑦 | |
6 | 5 | cv 1535 | . . . . . . 7 class 𝑦 |
7 | 6 | cint 4879 | . . . . . 6 class ∩ 𝑦 |
8 | 4, 7 | cin 3938 | . . . . 5 class (∪ 𝑥 ∩ ∩ 𝑦) |
9 | 8, 3 | wcel 2113 | . . . 4 wff (∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥 |
10 | 3 | cpw 4542 | . . . 4 class 𝒫 𝑥 |
11 | 9, 5, 10 | wral 3141 | . . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥 |
12 | 11, 2 | cab 2802 | . 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} |
13 | 1, 12 | wceq 1536 | 1 wff Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} |
Colors of variables: wff setvar class |
This definition is referenced by: bj-ismoore 34401 |
Copyright terms: Public domain | W3C validator |