Metamath Proof Explorer


Theorem bj-discrmoore

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 AV𝒫AMoore_

Proof

Step Hyp Ref Expression
1 unipw 𝒫A=A
2 1 ineq1i 𝒫Ax=Ax
3 inex1g AVAxV
4 inss1 AxA
5 4 a1i AVAxA
6 3 5 elpwd AVAx𝒫A
7 2 6 eqeltrid AV𝒫Ax𝒫A
8 7 adantr AVx𝒫A𝒫Ax𝒫A
9 8 bj-ismooredr AV𝒫AMoore_
10 pwexr 𝒫AMoore_AV
11 9 10 impbii AV𝒫AMoore_