Definition df-scott

Description: Define the Scott operation. This operation constructs a subset of the input class which is nonempty whenever its input is using Scott's trick. (Contributed by Rohan Ridenour, 9-Aug-2023)

	Ref	Expression
Assertion	df-scott	|- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cscott	|- Scott A
2		vx	|- x
3		vy	|- y
4		crnk	|- rank
5	2	cv	|- x
6	5 4	cfv	|- ( rank ` x )
7	3	cv	|- y
8	7 4	cfv	|- ( rank ` y )
9	6 8	wss	|- ( rank ` x ) C_ ( rank ` y )
10	9 3 0	wral	|- A. y e. A ( rank ` x ) C_ ( rank ` y )
11	10 2 0	crab	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
12	1 11	wceq	|- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }