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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unipw | |
|
2 | 1 | ineq1i | |
3 | inex1g | |
|
4 | inss1 | |
|
5 | 4 | a1i | |
6 | 3 5 | elpwd | |
7 | 2 6 | eqeltrid | |
8 | 7 | adantr | |
9 | 8 | bj-ismooredr | |
10 | pwexr | |
|
11 | 9 10 | impbii | |