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 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
Assertion ertr ${⊢}{\phi }\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$

Proof

Step Hyp Ref Expression
1 ersymb.1 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
2 errel ${⊢}{R}\mathrm{Er}{X}\to \mathrm{Rel}{R}$
3 1 2 syl ${⊢}{\phi }\to \mathrm{Rel}{R}$
4 simpr ${⊢}\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {B}{R}{C}$
5 brrelex1 ${⊢}\left(\mathrm{Rel}{R}\wedge {B}{R}{C}\right)\to {B}\in \mathrm{V}$
6 3 4 5 syl2an ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to {B}\in \mathrm{V}$
7 simpr ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to \left({A}{R}{B}\wedge {B}{R}{C}\right)$
8 breq2 ${⊢}{x}={B}\to \left({A}{R}{x}↔{A}{R}{B}\right)$
9 breq1 ${⊢}{x}={B}\to \left({x}{R}{C}↔{B}{R}{C}\right)$
10 8 9 anbi12d ${⊢}{x}={B}\to \left(\left({A}{R}{x}\wedge {x}{R}{C}\right)↔\left({A}{R}{B}\wedge {B}{R}{C}\right)\right)$
11 6 7 10 spcedv ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({A}{R}{x}\wedge {x}{R}{C}\right)$
12 simpl ${⊢}\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{B}$
13 brrelex1 ${⊢}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to {A}\in \mathrm{V}$
14 3 12 13 syl2an ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to {A}\in \mathrm{V}$
15 brrelex2 ${⊢}\left(\mathrm{Rel}{R}\wedge {B}{R}{C}\right)\to {C}\in \mathrm{V}$
16 3 4 15 syl2an ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to {C}\in \mathrm{V}$
17 brcog ${⊢}\left({A}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to \left({A}\left({R}\circ {R}\right){C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}{R}{x}\wedge {x}{R}{C}\right)\right)$
18 14 16 17 syl2anc ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to \left({A}\left({R}\circ {R}\right){C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}{R}{x}\wedge {x}{R}{C}\right)\right)$
19 11 18 mpbird ${⊢}\left({\phi }\wedge \left({A}{R}{B}\wedge {B}{R}{C}\right)\right)\to {A}\left({R}\circ {R}\right){C}$
20 19 ex ${⊢}{\phi }\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}\left({R}\circ {R}\right){C}\right)$
21 df-er ${⊢}{R}\mathrm{Er}{X}↔\left(\mathrm{Rel}{R}\wedge \mathrm{dom}{R}={X}\wedge {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}\right)$
22 21 simp3bi ${⊢}{R}\mathrm{Er}{X}\to {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}$
23 1 22 syl ${⊢}{\phi }\to {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}$
24 23 unssbd ${⊢}{\phi }\to {R}\circ {R}\subseteq {R}$
25 24 ssbrd ${⊢}{\phi }\to \left({A}\left({R}\circ {R}\right){C}\to {A}{R}{C}\right)$
26 20 25 syld ${⊢}{\phi }\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$