![]() |
Mathbox for Rohan Ridenour |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-scott | Structured version Visualization version GIF version |
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 |
---|---|
df-scott | β’ Scott π΄ = {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class π΄ | |
2 | 1 | cscott 42607 | . 2 class Scott π΄ |
3 | vx | . . . . . . 7 setvar π₯ | |
4 | 3 | cv 1541 | . . . . . 6 class π₯ |
5 | crnk 9707 | . . . . . 6 class rank | |
6 | 4, 5 | cfv 6500 | . . . . 5 class (rankβπ₯) |
7 | vy | . . . . . . 7 setvar π¦ | |
8 | 7 | cv 1541 | . . . . . 6 class π¦ |
9 | 8, 5 | cfv 6500 | . . . . 5 class (rankβπ¦) |
10 | 6, 9 | wss 3914 | . . . 4 wff (rankβπ₯) β (rankβπ¦) |
11 | 10, 7, 1 | wral 3061 | . . 3 wff βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) |
12 | 11, 3, 1 | crab 3406 | . 2 class {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
13 | 2, 12 | wceq 1542 | 1 wff Scott π΄ = {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
Colors of variables: wff setvar class |
This definition is referenced by: scotteqd 42609 nfscott 42611 scottabf 42612 scottss 42615 scottex2 42617 scotteld 42618 scottelrankd 42619 |
Copyright terms: Public domain | W3C validator |