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