Theorem scottsn

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

	Ref	Expression
Assertion	scottsn	|- Scott { A } = { A }

Proof

Step	Hyp	Ref	Expression
1		df-scott	|- Scott { A } = { x e. { A } | A. y e. { A } ( rank ` x ) C_ ( rank ` y ) }
2		velsn	|- ( x e. { A } <-> x = A )
3		velsn	|- ( y e. { A } <-> y = A )
4		eqtr3	|- ( ( x = A /\ y = A ) -> x = y )
5	2 3 4	syl2anb	|- ( ( x e. { A } /\ y e. { A } ) -> x = y )
6		fveq2	|- ( x = y -> ( rank ` x ) = ( rank ` y ) )
7	6	eqimssd	|- ( x = y -> ( rank ` x ) C_ ( rank ` y ) )
8	5 7	syl	|- ( ( x e. { A } /\ y e. { A } ) -> ( rank ` x ) C_ ( rank ` y ) )
9	8	ralrimiva	|- ( x e. { A } -> A. y e. { A } ( rank ` x ) C_ ( rank ` y ) )
10	9	rabeqc	|- { x e. { A } | A. y e. { A } ( rank ` x ) C_ ( rank ` y ) } = { A }
11	1 10	eqtri	|- Scott { A } = { A }