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 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
Assertion ertr ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ersymb.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2 errel ⊢ ( 𝑅 Er 𝑋 → 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 df-er ⊢ ( 𝑅 Er 𝑋 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )
22 21 simp3bi ⊢ ( 𝑅 Er 𝑋 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
23 1 22 syl ⊢ ( 𝜑 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
24 23 unssbd ⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
25 24 ssbrd ⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 → 𝐴 𝑅 𝐶 ) )
26 20 25 syld ⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )