Theorem bj-ismoore

Description: Characterization of Moore collections. Note that there is no sethood hypothesis on A : it is implied by either side (this is obvious for the LHS, and is the content of bj-mooreset for the RHS). (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-ismoore	|- ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. Moore_ -> A e. _V )
2		bj-mooreset	|- ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> A e. _V )
3		pweq	|- ( y = A -> ~P y = ~P A )
4		unieq	|- ( y = A -> U. y = U. A )
5	4	ineq1d	|- ( y = A -> ( U. y i^i |^| x ) = ( U. A i^i |^| x ) )
6		id	|- ( y = A -> y = A )
7	5 6	eleq12d	|- ( y = A -> ( ( U. y i^i |^| x ) e. y <-> ( U. A i^i |^| x ) e. A ) )
8	3 7	raleqbidv	|- ( y = A -> ( A. x e. ~P y ( U. y i^i |^| x ) e. y <-> A. x e. ~P A ( U. A i^i |^| x ) e. A ) )
9		df-bj-moore	|- Moore_ = { y | A. x e. ~P y ( U. y i^i |^| x ) e. y }
10	8 9	elab2g	|- ( A e. _V -> ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A ) )
11	1 2 10	pm5.21nii	|- ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A )