Metamath Proof Explorer


Theorem scotteqd

Description: Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023)

Ref Expression
Hypothesis scotteqd.1
|- ( ph -> A = B )
Assertion scotteqd
|- ( ph -> Scott A = Scott B )

Proof

Step Hyp Ref Expression
1 scotteqd.1
 |-  ( ph -> A = B )
2 1 adantr
 |-  ( ( ph /\ x e. A ) -> A = B )
3 2 raleqdv
 |-  ( ( ph /\ x e. A ) -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) <-> A. y e. B ( rank ` x ) C_ ( rank ` y ) ) )
4 1 3 rabeqbidva
 |-  ( ph -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { x e. B | A. y e. B ( rank ` x ) C_ ( rank ` y ) } )
5 df-scott
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
6 df-scott
 |-  Scott B = { x e. B | A. y e. B ( rank ` x ) C_ ( rank ` y ) }
7 4 5 6 3eqtr4g
 |-  ( ph -> Scott A = Scott B )