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	$⊢ φ \to EqvRel R$
	Assertion	eqvreltr	$⊢ φ \to ((A R B \land B R C) \to A R C)$

Proof

Step	Hyp	Ref	Expression
1		eqvreltr.1	$⊢ φ \to EqvRel R$
2		eqvrelrel	$⊢ EqvRel R \to Rel R$
3	1 2	syl	$⊢ φ \to Rel R$
4		simpr	$⊢ (A R B \land B R C) \to B R C$
5		brrelex1	$⊢ (Rel R \land B R C) \to B \in V$
6	3 4 5	syl2an	$⊢ (φ \land (A R B \land B R C)) \to B \in V$
7		simpr	$⊢ (φ \land (A R B \land B R C)) \to (A R B \land B R C)$
8		breq2	$⊢ x = B \to (A R x \leftrightarrow A R B)$
9		breq1	$⊢ x = B \to (x R C \leftrightarrow B R C)$
10	8 9	anbi12d	$⊢ x = B \to ((A R x \land x R C) \leftrightarrow (A R B \land B R C))$
11	6 7 10	spcedv	$⊢ (φ \land (A R B \land B R C)) \to \exists x (A R x \land x R C)$
12		simpl	$⊢ (A R B \land B R C) \to A R B$
13		brrelex1	$⊢ (Rel R \land A R B) \to A \in V$
14	3 12 13	syl2an	$⊢ (φ \land (A R B \land B R C)) \to A \in V$
15		brrelex2	$⊢ (Rel R \land B R C) \to C \in V$
16	3 4 15	syl2an	$⊢ (φ \land (A R B \land B R C)) \to C \in V$
17		brcog	$⊢ (A \in V \land C \in V) \to (A (R \circ R) C \leftrightarrow \exists x (A R x \land x R C))$
18	14 16 17	syl2anc	$⊢ (φ \land (A R B \land B R C)) \to (A (R \circ R) C \leftrightarrow \exists x (A R x \land x R C))$
19	11 18	mpbird	$⊢ (φ \land (A R B \land B R C)) \to A (R \circ R) C$
20	19	ex	$⊢ φ \to ((A R B \land B R C) \to A (R \circ R) C)$
21		dfeqvrel2	$⊢ EqvRel R \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$
22	21	simplbi	$⊢ EqvRel R \to ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R)$
23	22	simp3d	$⊢ EqvRel R \to R \circ R \subseteq R$
24	1 23	syl	$⊢ φ \to R \circ R \subseteq R$
25	24	ssbrd	$⊢ φ \to (A (R \circ R) C \to A R C)$
26	20 25	syld	$⊢ φ \to ((A R B \land B R C) \to A R C)$

Metamath Proof Explorer

Theorem eqvreltr

Proof