Metamath Proof Explorer

Theorem eqvrelth

Description: Basic property of equivalence relations. Theorem 73 of Suppes p. 82. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Hypotheses eqvrelth.1 
|- ( ph -> EqvRel R )
eqvrelth.2 
|- ( ph -> A e. dom R )
Assertion eqvrelth 
|- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )

Proof

Step Hyp Ref Expression
1 eqvrelth.1 
 |-  ( ph -> EqvRel R )
2 eqvrelth.2 
 |-  ( ph -> A e. dom R )
3 1 eqvrelsymb 
 |-  ( ph -> ( A R B <-> B R A ) )
4 3 biimpa 
 |-  ( ( ph /\ A R B ) -> B R A )
5 1 eqvreltr 
 |-  ( ph -> ( ( B R A /\ A R x ) -> B R x ) )
6 5 impl 
 |-  ( ( ( ph /\ B R A ) /\ A R x ) -> B R x )
7 4 6 syldanl 
 |-  ( ( ( ph /\ A R B ) /\ A R x ) -> B R x )
8 1 eqvreltr 
 |-  ( ph -> ( ( A R B /\ B R x ) -> A R x ) )
9 8 impl 
 |-  ( ( ( ph /\ A R B ) /\ B R x ) -> A R x )
10 7 9 impbida 
 |-  ( ( ph /\ A R B ) -> ( A R x <-> B R x ) )
11 vex 
 |-  x e. _V
12 2 adantr 
 |-  ( ( ph /\ A R B ) -> A e. dom R )
13 elecg 
 |-  ( ( x e. _V /\ A e. dom R ) -> ( x e. [ A ] R <-> A R x ) )
14 11 12 13 sylancr 
 |-  ( ( ph /\ A R B ) -> ( x e. [ A ] R <-> A R x ) )
15 eqvrelrel 
 |-  ( EqvRel R -> Rel R )
16 1 15 syl 
 |-  ( ph -> Rel R )
17 brrelex2 
 |-  ( ( Rel R /\ A R B ) -> B e. _V )
18 16 17 sylan 
 |-  ( ( ph /\ A R B ) -> B e. _V )
19 elecg 
 |-  ( ( x e. _V /\ B e. _V ) -> ( x e. [ B ] R <-> B R x ) )
20 11 18 19 sylancr 
 |-  ( ( ph /\ A R B ) -> ( x e. [ B ] R <-> B R x ) )
21 10 14 20 3bitr4d 
 |-  ( ( ph /\ A R B ) -> ( x e. [ A ] R <-> x e. [ B ] R ) )
22 21 eqrdv 
 |-  ( ( ph /\ A R B ) -> [ A ] R = [ B ] R )
23 1 adantr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> EqvRel R )
24 1 2 eqvrelref 
 |-  ( ph -> A R A )
25 24 adantr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A R A )
26 2 adantr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. dom R )
27 elecALTV 
 |-  ( ( A e. dom R /\ A e. dom R ) -> ( A e. [ A ] R <-> A R A ) )
28 26 26 27 syl2anc 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. [ A ] R <-> A R A ) )
29 25 28 mpbird 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. [ A ] R )
30 simpr 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> [ A ] R = [ B ] R )
31 29 30 eleqtrd 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A e. [ B ] R )
32 30 dmec2d 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. dom R <-> B e. dom R ) )
33 26 32 mpbid 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> B e. dom R )
34 elecALTV 
 |-  ( ( B e. dom R /\ A e. dom R ) -> ( A e. [ B ] R <-> B R A ) )
35 33 26 34 syl2anc 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> ( A e. [ B ] R <-> B R A ) )
36 31 35 mpbid 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> B R A )
37 23 36 eqvrelsym 
 |-  ( ( ph /\ [ A ] R = [ B ] R ) -> A R B )
38 22 37 impbida 
 |-  ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )