# Metamath Proof Explorer

## 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}=\left\{{x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{rank}\left({x}\right)\subseteq \mathrm{rank}\left({y}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 cscott ${class}Scott{A}$
2 vx ${setvar}{x}$
3 vy ${setvar}{y}$
4 crnk ${class}\mathrm{rank}$
5 2 cv ${setvar}{x}$
6 5 4 cfv ${class}\mathrm{rank}\left({x}\right)$
7 3 cv ${setvar}{y}$
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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\mathrm{rank}\left({x}\right)\subseteq \mathrm{rank}\left({y}\right)\right\}$
12 1 11 wceq ${wff}Scott{A}=\left\{{x}\in {A}|\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{rank}\left({x}\right)\subseteq \mathrm{rank}\left({y}\right)\right\}$