Metamath Proof Explorer

Theorem ecscottd

Description: Applying the Scott operation to equivalence classes preserves their equality property. (Contributed by BTernaryTau, 20-Oct-2026)

Ref Expression
Hypotheses ecscottd.1 
|- ( ph -> R Er V )
ecscottd.2 
|- ( ph -> A e. V )
Assertion ecscottd 
|- ( ph -> ( A R B <-> Scott [ A ] R = Scott [ B ] R ) )

Proof

Step Hyp Ref Expression
1 ecscottd.1 
 |-  ( ph -> R Er V )
2 ecscottd.2 
 |-  ( ph -> A e. V )
3 1 2 erscottd 
 |-  ( ph -> ( A R B <-> Scott { x | x R A } = Scott { x | x R B } ) )
4 3 adantr 
 |-  ( ( ph /\ B e. V ) -> ( A R B <-> Scott { x | x R A } = Scott { x | x R B } ) )
5 dfec2 
 |-  ( A e. V -> [ A ] R = { x | A R x } )
6 2 5 syl 
 |-  ( ph -> [ A ] R = { x | A R x } )
7 1 ersymb 
 |-  ( ph -> ( A R x <-> x R A ) )
8 7 abbidv 
 |-  ( ph -> { x | A R x } = { x | x R A } )
9 6 8 eqtrd 
 |-  ( ph -> [ A ] R = { x | x R A } )
10 9 scotteqd 
 |-  ( ph -> Scott [ A ] R = Scott { x | x R A } )
11 10 adantr 
 |-  ( ( ph /\ B e. V ) -> Scott [ A ] R = Scott { x | x R A } )
12 dfec2 
 |-  ( B e. V -> [ B ] R = { x | B R x } )
13 1 ersymb 
 |-  ( ph -> ( B R x <-> x R B ) )
14 13 abbidv 
 |-  ( ph -> { x | B R x } = { x | x R B } )
15 12 14 sylan9eqr 
 |-  ( ( ph /\ B e. V ) -> [ B ] R = { x | x R B } )
16 15 scotteqd 
 |-  ( ( ph /\ B e. V ) -> Scott [ B ] R = Scott { x | x R B } )
17 11 16 eqeq12d 
 |-  ( ( ph /\ B e. V ) -> ( Scott [ A ] R = Scott [ B ] R <-> Scott { x | x R A } = Scott { x | x R B } ) )
18 4 17 bitr4d 
 |-  ( ( ph /\ B e. V ) -> ( A R B <-> Scott [ A ] R = Scott [ B ] R ) )
19 1 adantr 
 |-  ( ( ph /\ A R B ) -> R Er V )
20 simpr 
 |-  ( ( ph /\ A R B ) -> A R B )
21 19 20 ercl2 
 |-  ( ( ph /\ A R B ) -> B e. V )
22 21 stoic1a 
 |-  ( ( ph /\ -. B e. V ) -> -. A R B )
23 erdm 
 |-  ( R Er V -> dom R = V )
24 1 23 syl 
 |-  ( ph -> dom R = V )
25 2 24 eleqtrrd 
 |-  ( ph -> A e. dom R )
26 ecdmn0 
 |-  ( A e. dom R <-> [ A ] R =/= (/) )
27 25 26 sylib 
 |-  ( ph -> [ A ] R =/= (/) )
28 scott0b 
 |-  ( [ A ] R = (/) <-> Scott [ A ] R = (/) )
29 28 necon3bii 
 |-  ( [ A ] R =/= (/) <-> Scott [ A ] R =/= (/) )
30 27 29 sylib 
 |-  ( ph -> Scott [ A ] R =/= (/) )
31 30 adantr 
 |-  ( ( ph /\ -. B e. V ) -> Scott [ A ] R =/= (/) )
32 24 eleq2d 
 |-  ( ph -> ( B e. dom R <-> B e. V ) )
33 32 notbid 
 |-  ( ph -> ( -. B e. dom R <-> -. B e. V ) )
34 33 biimpar 
 |-  ( ( ph /\ -. B e. V ) -> -. B e. dom R )
35 ecdmn0 
 |-  ( B e. dom R <-> [ B ] R =/= (/) )
36 35 necon2bbii 
 |-  ( [ B ] R = (/) <-> -. B e. dom R )
37 34 36 sylibr 
 |-  ( ( ph /\ -. B e. V ) -> [ B ] R = (/) )
38 scott0b 
 |-  ( [ B ] R = (/) <-> Scott [ B ] R = (/) )
39 37 38 sylib 
 |-  ( ( ph /\ -. B e. V ) -> Scott [ B ] R = (/) )
40 31 39 neeqtrrd 
 |-  ( ( ph /\ -. B e. V ) -> Scott [ A ] R =/= Scott [ B ] R )
41 40 neneqd 
 |-  ( ( ph /\ -. B e. V ) -> -. Scott [ A ] R = Scott [ B ] R )
42 22 41 2falsed 
 |-  ( ( ph /\ -. B e. V ) -> ( A R B <-> Scott [ A ] R = Scott [ B ] R ) )
43 18 42 pm2.61dan 
 |-  ( ph -> ( A R B <-> Scott [ A ] R = Scott [ B ] R ) )