Metamath Proof Explorer

Theorem eqvreltr

Description: An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Hypothesis eqvreltr.1 
|- ( ph -> EqvRel R )
Assertion eqvreltr 
|- ( ph -> ( ( A R B /\ B R C ) -> A R C ) )

Proof

Step Hyp Ref Expression
1 eqvreltr.1 
 |-  ( ph -> EqvRel R )
2 eqvrelrel 
 |-  ( EqvRel R -> Rel R )
3 1 2 syl 
 |-  ( ph -> Rel R )
4 simpr 
 |-  ( ( A R B /\ B R C ) -> B R C )
5 brrelex1 
 |-  ( ( Rel R /\ B R C ) -> B e. _V )
6 3 4 5 syl2an 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> B e. _V )
7 simpr 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> ( A R B /\ B R C ) )
8 breq2 
 |-  ( x = B -> ( A R x <-> A R B ) )
9 breq1 
 |-  ( x = B -> ( x R C <-> B R C ) )
10 8 9 anbi12d 
 |-  ( x = B -> ( ( A R x /\ x R C ) <-> ( A R B /\ B R C ) ) )
11 6 7 10 spcedv 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> E. x ( A R x /\ x R C ) )
12 simpl 
 |-  ( ( A R B /\ B R C ) -> A R B )
13 brrelex1 
 |-  ( ( Rel R /\ A R B ) -> A e. _V )
14 3 12 13 syl2an 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> A e. _V )
15 brrelex2 
 |-  ( ( Rel R /\ B R C ) -> C e. _V )
16 3 4 15 syl2an 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> C e. _V )
17 brcog 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A ( R o. R ) C <-> E. x ( A R x /\ x R C ) ) )
18 14 16 17 syl2anc 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> ( A ( R o. R ) C <-> E. x ( A R x /\ x R C ) ) )
19 11 18 mpbird 
 |-  ( ( ph /\ ( A R B /\ B R C ) ) -> A ( R o. R ) C )
20 19 ex 
 |-  ( ph -> ( ( A R B /\ B R C ) -> A ( R o. R ) C ) )
21 dfeqvrel2 
 |-  ( EqvRel R <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) )
22 21 simplbi 
 |-  ( EqvRel R -> ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) )
23 22 simp3d 
 |-  ( EqvRel R -> ( R o. R ) C_ R )
24 1 23 syl 
 |-  ( ph -> ( R o. R ) C_ R )
25 24 ssbrd 
 |-  ( ph -> ( A ( R o. R ) C -> A R C ) )
26 20 25 syld 
 |-  ( ph -> ( ( A R B /\ B R C ) -> A R C ) )