Theorem scottidm

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

	Ref	Expression
Assertion	scottidm	⊢ Scott Scott 𝐴 = Scott 𝐴

Proof

Step	Hyp	Ref	Expression
1		scottss	⊢ Scott Scott 𝐴 ⊆ Scott 𝐴
2		elscott	⊢ ( 𝑥 ∈ Scott 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
3		scottss	⊢ Scott 𝐴 ⊆ 𝐴
4		ssralv	⊢ ( Scott 𝐴 ⊆ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ∀ 𝑦 ∈ Scott 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
5	3 4	ax-mp	⊢ ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ∀ 𝑦 ∈ Scott 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
6	2 5	simplbiim	⊢ ( 𝑥 ∈ Scott 𝐴 → ∀ 𝑦 ∈ Scott 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
7	6	ancli	⊢ ( 𝑥 ∈ Scott 𝐴 → ( 𝑥 ∈ Scott 𝐴 ∧ ∀ 𝑦 ∈ Scott 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
8		elscott	⊢ ( 𝑥 ∈ Scott Scott 𝐴 ↔ ( 𝑥 ∈ Scott 𝐴 ∧ ∀ 𝑦 ∈ Scott 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
9	7 8	sylibr	⊢ ( 𝑥 ∈ Scott 𝐴 → 𝑥 ∈ Scott Scott 𝐴 )
10	9	ssriv	⊢ Scott 𝐴 ⊆ Scott Scott 𝐴
11	1 10	eqssi	⊢ Scott Scott 𝐴 = Scott 𝐴