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	$$⊢ScottA=\left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cscott	$$classScottA$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		crnk	$$class\mathrm{rank}$$
5	2	cv	$$setvarx$$
6	5 4	cfv	$$class\mathrm{rank}\left(x\right)$$
7	3	cv	$$setvary$$
8	7 4	cfv	$$class\mathrm{rank}\left(y\right)$$
9	6 8	wss	$$wff\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
10	9 3 0	wral	$$wff\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
11	10 2 0	crab	$$class\left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$
12	1 11	wceq	$$wffScottA=\left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$