Theorem scottsn

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

	Ref	Expression
Assertion	scottsn	$$⊢Scott\left\{A\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-scott	$$⊢Scott\left\{A\right\}=\left\{x\in \left\{A\right\}|\forall y\in \left\{A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$
2		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
3		velsn	$$⊢y\in \left\{A\right\}\leftrightarrow y=A$$
4		eqtr3	$$⊢\left(x=A\wedge y=A\right)\to x=y$$
5	2 3 4	syl2anb	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to x=y$$
6		fveq2	$$⊢x=y\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(y\right)$$
7	6	eqimssd	$$⊢x=y\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
8	5 7	syl	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
9	8	ralrimiva	$$⊢x\in \left\{A\right\}\to \forall y\in \left\{A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
10	9	rabeqc	$$⊢\left\{x\in \left\{A\right\}|\forall y\in \left\{A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{A\right\}$$
11	1 10	eqtri	$$⊢Scott\left\{A\right\}=\left\{A\right\}$$