# Metamath Proof Explorer

## Theorem ertr

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

Ref Expression
Hypothesis ersymb.1
|- ( ph -> R Er X )
Assertion ertr
|- ( ph -> ( ( A R B /\ B R C ) -> A R C ) )

### Proof

Step Hyp Ref Expression
1 ersymb.1
|-  ( ph -> R Er X )
2 errel
|-  ( R Er X -> 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 df-er
|-  ( R Er X <-> ( Rel R /\ dom R = X /\ ( `' R u. ( R o. R ) ) C_ R ) )
22 21 simp3bi
|-  ( R Er X -> ( `' R u. ( R o. R ) ) C_ R )
23 1 22 syl
|-  ( ph -> ( `' R u. ( R o. R ) ) C_ R )
24 23 unssbd
|-  ( 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 ) )