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