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	|- ( A e. _V <-> ~P A e. Moore_ )

Proof

Step	Hyp	Ref	Expression
1		unipw	|- U. ~P A = A
2	1	ineq1i	|- ( U. ~P A i^i |^| x ) = ( A i^i |^| x )
3		inex1g	|- ( A e. _V -> ( A i^i |^| x ) e. _V )
4		inss1	|- ( A i^i |^| x ) C_ A
5	4	a1i	|- ( A e. _V -> ( A i^i |^| x ) C_ A )
6	3 5	elpwd	|- ( A e. _V -> ( A i^i |^| x ) e. ~P A )
7	2 6	eqeltrid	|- ( A e. _V -> ( U. ~P A i^i |^| x ) e. ~P A )
8	7	adantr	|- ( ( A e. _V /\ x C_ ~P A ) -> ( U. ~P A i^i |^| x ) e. ~P A )
9	8	bj-ismooredr	|- ( A e. _V -> ~P A e. Moore_ )
10		pwexr	|- ( ~P A e. Moore_ -> A e. _V )
11	9 10	impbii	|- ( A e. _V <-> ~P A e. Moore_ )