This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )