Metamath Proof Explorer

Theorem scottidm

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

Ref Expression
Assertion scottidm 
|- Scott Scott A = Scott A

Proof

Step Hyp Ref Expression
1 scottss 
 |-  Scott Scott A C_ Scott A
2 elscott 
 |-  ( x e. Scott A <-> ( x e. A /\ A. y e. A ( rank ` x ) C_ ( rank ` y ) ) )
3 scottss 
 |-  Scott A C_ A
4 ssralv 
 |-  ( Scott A C_ A -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> A. y e. Scott A ( rank ` x ) C_ ( rank ` y ) ) )
5 3 4 ax-mp 
 |-  ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> A. y e. Scott A ( rank ` x ) C_ ( rank ` y ) )
6 2 5 simplbiim 
 |-  ( x e. Scott A -> A. y e. Scott A ( rank ` x ) C_ ( rank ` y ) )
7 6 ancli 
 |-  ( x e. Scott A -> ( x e. Scott A /\ A. y e. Scott A ( rank ` x ) C_ ( rank ` y ) ) )
8 elscott 
 |-  ( x e. Scott Scott A <-> ( x e. Scott A /\ A. y e. Scott A ( rank ` x ) C_ ( rank ` y ) ) )
9 7 8 sylibr 
 |-  ( x e. Scott A -> x e. Scott Scott A )
10 9 ssriv 
 |-  Scott A C_ Scott Scott A
11 1 10 eqssi 
 |-  Scott Scott A = Scott A