Description: Sufficient condition to be a Moore collection. Note that there is no sethood hypothesis on A : it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | bj-ismooredr.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) | |
| Assertion | bj-ismooredr | ⊢ ( 𝜑 → 𝐴 ∈ Moore ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-ismooredr.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) | |
| 2 | elpwi | ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 ) | |
| 3 | 1 | ex | ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) ) |
| 4 | 2 3 | syl5 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) ) |
| 5 | 4 | ralrimiv | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) |
| 6 | bj-ismoore | ⊢ ( 𝐴 ∈ Moore ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) | |
| 7 | 5 6 | sylibr | ⊢ ( 𝜑 → 𝐴 ∈ Moore ) |