Theorem scottsn

Description: Applying Scott's trick to a singleton leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	scottsn	⊢ Scott { 𝐴 } = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		df-scott	⊢ Scott { 𝐴 } = { 𝑥 ∈ { 𝐴 } ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
2		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
4		eqtr3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝑥 = 𝑦 )
5	2 3 4	syl2anb	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → 𝑥 = 𝑦 )
6		fveq2	⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
7	6	eqimssd	⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
8	5 7	syl	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
9	8	ralrimiva	⊢ ( 𝑥 ∈ { 𝐴 } → ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
10	9	rabeqc	⊢ { 𝑥 ∈ { 𝐴 } ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝐴 }
11	1 10	eqtri	⊢ Scott { 𝐴 } = { 𝐴 }