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

Metamath Proof Explorer

Theorem eqvreltr

Proof