Definition df-scott 9956

Description: Define an operation for Scott's trick, expressed as in Equation 9.3 of [Jech] p. 72. Scott's trick collects all sets that have a certain property and are of the smallest possible rank. The resulting collection is guaranteed to be a set (see scottex 9960). Under this definition, the property in question is represented by membership in a class. See scottab 9967 for the case where a wff (meta)variable is used to represent the property. (Contributed by Rohan Ridenour, 9-Aug-2023.)

Assertion

Ref	Expression
df-scott	⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}

Distinct variable group:   𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-scott

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cscott 9955	. 2 class Scott 𝐴
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1569	. . . . . 6 class 𝑥
5		crnk 9794	. . . . . 6 class rank
6	4, 5	cfv 6558	. . . . 5 class (rank‘𝑥)
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1569	. . . . . 6 class 𝑦
9	8, 5	cfv 6558	. . . . 5 class (rank‘𝑦)
10	6, 9	wss 3900	. . . 4 wff (rank‘𝑥) ⊆ (rank‘𝑦)
11	10, 7, 1	wral 3080	. . 3 wff ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)
12	11, 3, 1	crab 3416	. 2 class {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}
13	2, 12	wceq 1570	1 wff Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}

This definition is used by:  scotteqd  9957  nfscott  9959  scottex  9960  scottss  9962  scott0b  9964  scottabf  9966  scottex2OLD  9973  scottelrankd  9975  elscott  35825  dfscott2  35826  scottsn  35834  scott0bOLD  35835  0elscott  35837  scottexf  39292  scott0f  39293