Metamath Proof Explorer

Theorem erscottd

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

Ref Expression
Hypotheses erscottd.1 
|- ( ph -> R Er V )
erscottd.2 
|- ( ph -> A e. V )
Assertion erscottd 
|- ( ph -> ( A R B <-> Scott { x | x R A } = Scott { x | x R B } ) )

Proof

Step Hyp Ref Expression
1 erscottd.1 
 |-  ( ph -> R Er V )
2 erscottd.2 
 |-  ( ph -> A e. V )
3 1 3ad2ant1 
 |-  ( ( ph /\ A R B /\ x R A ) -> R Er V )
4 simp3 
 |-  ( ( ph /\ A R B /\ x R A ) -> x R A )
5 simp2 
 |-  ( ( ph /\ A R B /\ x R A ) -> A R B )
6 3 4 5 ertrd 
 |-  ( ( ph /\ A R B /\ x R A ) -> x R B )
7 6 3expia 
 |-  ( ( ph /\ A R B ) -> ( x R A -> x R B ) )
8 1 3ad2ant1 
 |-  ( ( ph /\ A R B /\ x R B ) -> R Er V )
9 simp3 
 |-  ( ( ph /\ A R B /\ x R B ) -> x R B )
10 simp2 
 |-  ( ( ph /\ A R B /\ x R B ) -> A R B )
11 8 9 10 ertr4d 
 |-  ( ( ph /\ A R B /\ x R B ) -> x R A )
12 11 3expia 
 |-  ( ( ph /\ A R B ) -> ( x R B -> x R A ) )
13 7 12 impbid 
 |-  ( ( ph /\ A R B ) -> ( x R A <-> x R B ) )
14 13 abbidv 
 |-  ( ( ph /\ A R B ) -> { x | x R A } = { x | x R B } )
15 14 scotteqd 
 |-  ( ( ph /\ A R B ) -> Scott { x | x R A } = Scott { x | x R B } )
16 1 2 erref 
 |-  ( ph -> A R A )
17 breq1 
 |-  ( x = A -> ( x R A <-> A R A ) )
18 2 16 17 elabd 
 |-  ( ph -> A e. { x | x R A } )
19 n0i 
 |-  ( A e. { x | x R A } -> -. { x | x R A } = (/) )
20 18 19 syl 
 |-  ( ph -> -. { x | x R A } = (/) )
21 scott0b 
 |-  ( { x | x R A } = (/) <-> Scott { x | x R A } = (/) )
22 20 21 sylnib 
 |-  ( ph -> -. Scott { x | x R A } = (/) )
23 disjeq0 
 |-  ( ( Scott { x | x R A } i^i Scott { x | x R B } ) = (/) -> ( Scott { x | x R A } = Scott { x | x R B } <-> ( Scott { x | x R A } = (/) /\ Scott { x | x R B } = (/) ) ) )
24 23 biimpcd 
 |-  ( Scott { x | x R A } = Scott { x | x R B } -> ( ( Scott { x | x R A } i^i Scott { x | x R B } ) = (/) -> ( Scott { x | x R A } = (/) /\ Scott { x | x R B } = (/) ) ) )
25 simpl 
 |-  ( ( Scott { x | x R A } = (/) /\ Scott { x | x R B } = (/) ) -> Scott { x | x R A } = (/) )
26 25 con3i 
 |-  ( -. Scott { x | x R A } = (/) -> -. ( Scott { x | x R A } = (/) /\ Scott { x | x R B } = (/) ) )
27 24 26 nsyli 
 |-  ( Scott { x | x R A } = Scott { x | x R B } -> ( -. Scott { x | x R A } = (/) -> -. ( Scott { x | x R A } i^i Scott { x | x R B } ) = (/) ) )
28 df-ne 
 |-  ( ( Scott { x | x R A } i^i Scott { x | x R B } ) =/= (/) <-> -. ( Scott { x | x R A } i^i Scott { x | x R B } ) = (/) )
29 ndisj 
 |-  ( ( Scott { x | x R A } i^i Scott { x | x R B } ) =/= (/) <-> E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) )
30 28 29 bitr3i 
 |-  ( -. ( Scott { x | x R A } i^i Scott { x | x R B } ) = (/) <-> E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) )
31 27 30 imbitrdi 
 |-  ( Scott { x | x R A } = Scott { x | x R B } -> ( -. Scott { x | x R A } = (/) -> E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) ) )
32 22 31 mpan9 
 |-  ( ( ph /\ Scott { x | x R A } = Scott { x | x R B } ) -> E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) )
33 1 3ad2ant1 
 |-  ( ( ph /\ y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> R Er V )
34 breq1 
 |-  ( x = y -> ( x R A <-> y R A ) )
35 34 elscottab 
 |-  ( y e. Scott { x | x R A } -> y R A )
36 35 3ad2ant2 
 |-  ( ( ph /\ y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> y R A )
37 breq1 
 |-  ( x = y -> ( x R B <-> y R B ) )
38 37 elscottab 
 |-  ( y e. Scott { x | x R B } -> y R B )
39 38 3ad2ant3 
 |-  ( ( ph /\ y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> y R B )
40 33 36 39 ertr3d 
 |-  ( ( ph /\ y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> A R B )
41 40 3expib 
 |-  ( ph -> ( ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> A R B ) )
42 41 exlimdv 
 |-  ( ph -> ( E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> A R B ) )
43 42 adantr 
 |-  ( ( ph /\ Scott { x | x R A } = Scott { x | x R B } ) -> ( E. y ( y e. Scott { x | x R A } /\ y e. Scott { x | x R B } ) -> A R B ) )
44 32 43 mpd 
 |-  ( ( ph /\ Scott { x | x R A } = Scott { x | x R B } ) -> A R B )
45 15 44 impbida 
 |-  ( ph -> ( A R B <-> Scott { x | x R A } = Scott { x | x R B } ) )