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

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	$⊢ φ \to R Er X$
2		errel	$⊢ R Er X \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		df-er	$⊢ R Er X \leftrightarrow (Rel R \land dom R = X \land R^{-1} \cup (R \circ R) \subseteq R)$
22	21	simp3bi	$⊢ R Er X \to R^{-1} \cup (R \circ R) \subseteq R$
23	1 22	syl	$⊢ φ \to R^{-1} \cup (R \circ R) \subseteq R$
24	23	unssbd	$⊢ φ \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 ertr

Proof