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 ( 𝜑 → EqvRel 𝑅 )
Assertion eqvreltr ( 𝜑 → ( ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqvreltr.1 ( 𝜑 → EqvRel 𝑅 )
2 eqvrelrel ( EqvRel 𝑅 → Rel 𝑅 )
3 1 2 syl ( 𝜑 → Rel 𝑅 )
4 simpr ( ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) → 𝐵 𝑅 𝐶 )
5 brrelex1 ( ( Rel 𝑅𝐵 𝑅 𝐶 ) → 𝐵 ∈ V )
6 3 4 5 syl2an ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → 𝐵 ∈ V )
7 simpr ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) )
8 breq2 ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥𝐴 𝑅 𝐵 ) )
9 breq1 ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝐶𝐵 𝑅 𝐶 ) )
10 8 9 anbi12d ( 𝑥 = 𝐵 → ( ( 𝐴 𝑅 𝑥𝑥 𝑅 𝐶 ) ↔ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) )
11 6 7 10 spcedv ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 𝑅 𝐶 ) )
12 simpl ( ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐵 )
13 brrelex1 ( ( Rel 𝑅𝐴 𝑅 𝐵 ) → 𝐴 ∈ V )
14 3 12 13 syl2an ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → 𝐴 ∈ V )
15 brrelex2 ( ( Rel 𝑅𝐵 𝑅 𝐶 ) → 𝐶 ∈ V )
16 3 4 15 syl2an ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → 𝐶 ∈ V )
17 brcog ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ( 𝑅𝑅 ) 𝐶 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 𝑅 𝐶 ) ) )
18 14 16 17 syl2anc ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → ( 𝐴 ( 𝑅𝑅 ) 𝐶 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 𝑅 𝐶 ) ) )
19 11 18 mpbird ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) ) → 𝐴 ( 𝑅𝑅 ) 𝐶 )
20 19 ex ( 𝜑 → ( ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) → 𝐴 ( 𝑅𝑅 ) 𝐶 ) )
21 dfeqvrel2 ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
22 21 simplbi ( EqvRel 𝑅 → ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) )
23 22 simp3d ( EqvRel 𝑅 → ( 𝑅𝑅 ) ⊆ 𝑅 )
24 1 23 syl ( 𝜑 → ( 𝑅𝑅 ) ⊆ 𝑅 )
25 24 ssbrd ( 𝜑 → ( 𝐴 ( 𝑅𝑅 ) 𝐶𝐴 𝑅 𝐶 ) )
26 20 25 syld ( 𝜑 → ( ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )