Definition df-bj-moore 33058

Description: Define the class of Moore collections. This is to df-mre 16246 what df-top 20699 is to df-topon 20716. For the sake of consistency, the function defined at df-mre 16246 should be denoted by "MooreOn".

Note: df-mre 16246 singles out the empty intersection. This is not necessary. It could be written instead Moore = ( x e. _V |-> { y e. ~P ~P x | A. z e. ~P y ( x i^i |^| z ) e. y } ) and the equivalence of both definitions is proved by bj-0int 33055.

There is no added generality in defining a "Moore predicate" for arbitrary classes, since a Moore class satisfying such a predicate is automatically a set (see bj-mooreset 33056). (Contributed by BJ, 27-Apr-2021.)

Assertion

Ref	Expression
df-bj-moore	|- Moore_ = { x | A. y e. ~P x ( U. x i^i |^| y ) e. x }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-bj-moore

Step	Hyp	Ref	Expression
1		cmoore 33057	. 2 class Moore_
2		vx	. . . . . . . 8 setvar x
3	2	cv 1482	. . . . . . 7 class x
4	3	cuni 4436	. . . . . 6 class U. x
5		vy	. . . . . . . 8 setvar y
6	5	cv 1482	. . . . . . 7 class y
7	6	cint 4475	. . . . . 6 class |^| y
8	4, 7	cin 3573	. . . . 5 class ( U. x i^i |^| y )
9	8, 3	wcel 1990	. . . 4 wff ( U. x i^i |^| y ) e. x
10	3	cpw 4158	. . . 4 class ~P x
11	9, 5, 10	wral 2912	. . 3 wff A. y e. ~P x ( U. x i^i |^| y ) e. x
12	11, 2	cab 2608	. 2 class { x | A. y e. ~P x ( U. x i^i |^| y ) e. x }
13	1, 12	wceq 1483	1 wff Moore_ = { x | A. y e. ~P x ( U. x i^i |^| y ) e. x }

This definition is referenced by:  bj-ismoore  33059