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 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cscott	⊢ Scott 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		crnk	⊢ rank
5	2	cv	⊢ 𝑥
6	5 4	cfv	⊢ ( rank ‘ 𝑥 )
7	3	cv	⊢ 𝑦
8	7 4	cfv	⊢ ( rank ‘ 𝑦 )
9	6 8	wss	⊢ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
10	9 3 0	wral	⊢ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
11	10 2 0	crab	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
12	1 11	wceq	⊢ Scott 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }