Theorem scottidm

Description: The Scott operation is idempotent. (Contributed by BTernaryTau, 23-Aug-2026)

	Ref	Expression
Assertion	scottidm	$$⊢ScottScottA=ScottA$$

Proof

Step	Hyp	Ref	Expression
1		scottss	$$⊢ScottScottA\subseteq ScottA$$
2		elscott	$$⊢x\in ScottA\leftrightarrow \left(x\in A\wedge \forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
3		scottss	$$⊢ScottA\subseteq A$$
4		ssralv	$$⊢ScottA\subseteq A\to \left(\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\to \forall y\in ScottA\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
5	3 4	ax-mp	$$⊢\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\to \forall y\in ScottA\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
6	2 5	simplbiim	$$⊢x\in ScottA\to \forall y\in ScottA\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
7	6	ancli	$$⊢x\in ScottA\to \left(x\in ScottA\wedge \forall y\in ScottA\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
8		elscott	$$⊢x\in ScottScottA\leftrightarrow \left(x\in ScottA\wedge \forall y\in ScottA\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
9	7 8	sylibr	$$⊢x\in ScottA\to x\in ScottScottA$$
10	9	ssriv	$$⊢ScottA\subseteq ScottScottA$$
11	1 10	eqssi	$$⊢ScottScottA=ScottA$$