Description: A Moore collection is a set. Therefore, the class Moore_ of all Moore sets defined in df-bj-moore is actually the class of all Moore collections. This is also illustrated by the lack of sethood condition in bj-ismoore .
Note that the closed sets of a topology form a Moore collection, so a topology is a set, and this remark also applies to many other families of sets (namely, as soon as the whole set is required to be a set of the family, then the associated kind of family has no proper classes: that this condition suffices to impose sethood can be seen in this proof, which relies crucially on uniexr ).
Note: if, in the above predicate, we substitute ~P X for A , then the last e. ~P X could be weakened to C_ X , and then the predicate would be obviously satisfied since |- U. ~P X = X ( unipw ), making ~P X a Moore collection in this weaker sense, for any class X , even proper, but the addition of this single case does not add anything interesting. Instead, we have the biconditional bj-discrmoore . (Contributed by BJ, 8-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-mooreset | ⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → 𝐴 ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0elpw | ⊢ ∅ ∈ 𝒫 𝐴 | |
| 2 | rint0 | ⊢ ( 𝑥 = ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) = ∪ 𝐴 ) | |
| 3 | 2 | eleq1d | ⊢ ( 𝑥 = ∅ → ( ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ↔ ∪ 𝐴 ∈ 𝐴 ) ) |
| 4 | 3 | rspcv | ⊢ ( ∅ ∈ 𝒫 𝐴 → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) ) |
| 5 | 1 4 | ax-mp | ⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) |
| 6 | uniexr | ⊢ ( ∪ 𝐴 ∈ 𝐴 → 𝐴 ∈ V ) | |
| 7 | 5 6 | syl | ⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → 𝐴 ∈ V ) |