Description: The powerclass ~P A is a Moore collection if and only if A is a set. It is then called the discrete Moore collection. (Contributed by BJ, 9-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-discrmoore | ⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unipw | ⊢ ∪ 𝒫 𝐴 = 𝐴 | |
| 2 | 1 | ineq1i | ⊢ ( ∪ 𝒫 𝐴 ∩ ∩ 𝑥 ) = ( 𝐴 ∩ ∩ 𝑥 ) |
| 3 | inex1g | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ∩ 𝑥 ) ∈ V ) | |
| 4 | inss1 | ⊢ ( 𝐴 ∩ ∩ 𝑥 ) ⊆ 𝐴 | |
| 5 | 4 | a1i | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ∩ 𝑥 ) ⊆ 𝐴 ) |
| 6 | 3 5 | elpwd | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ∩ 𝑥 ) ∈ 𝒫 𝐴 ) |
| 7 | 2 6 | eqeltrid | ⊢ ( 𝐴 ∈ V → ( ∪ 𝒫 𝐴 ∩ ∩ 𝑥 ) ∈ 𝒫 𝐴 ) |
| 8 | 7 | adantr | ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ⊆ 𝒫 𝐴 ) → ( ∪ 𝒫 𝐴 ∩ ∩ 𝑥 ) ∈ 𝒫 𝐴 ) |
| 9 | 8 | bj-ismooredr | ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ Moore ) |
| 10 | pwexr | ⊢ ( 𝒫 𝐴 ∈ Moore → 𝐴 ∈ V ) | |
| 11 | 9 10 | impbii | ⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore ) |