dirtr

Description: A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

		Ref	Expression
	Assertion	dirtr	$⊢ ((R \in DirRel \land C \in V) \land (A R B \land B R C)) \to A R C$

Proof

Step	Hyp	Ref	Expression
1		reldir	$⊢ R \in DirRel \to Rel R$
2		brrelex1	$⊢ (Rel R \land A R B) \to A \in V$
3	2	ex	$⊢ Rel R \to (A R B \to A \in V)$
4		brrelex1	$⊢ (Rel R \land B R C) \to B \in V$
5	4	ex	$⊢ Rel R \to (B R C \to B \in V)$
6	3 5	anim12d	$⊢ Rel R \to ((A R B \land B R C) \to (A \in V \land B \in V))$
7	1 6	syl	$⊢ R \in DirRel \to ((A R B \land B R C) \to (A \in V \land B \in V))$
8		eqid	$⊢ ⋃ ⋃ R = ⋃ ⋃ R$
9	8	isdir	$⊢ R \in DirRel \to (R \in DirRel \leftrightarrow ((Rel R \land {I ↾}_{⋃ ⋃ R} \subseteq R) \land (R \circ R \subseteq R \land ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R)))$
10	9	ibi	$⊢ R \in DirRel \to ((Rel R \land {I ↾}_{⋃ ⋃ R} \subseteq R) \land (R \circ R \subseteq R \land ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R))$
11	10	simprld	$⊢ R \in DirRel \to R \circ R \subseteq R$
12		cotr	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
13	11 12	sylib	$⊢ R \in DirRel \to \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
14		breq12	$⊢ (x = A \land y = B) \to (x R y \leftrightarrow A R B)$
15	14	3adant3	$⊢ (x = A \land y = B \land z = C) \to (x R y \leftrightarrow A R B)$
16		breq12	$⊢ (y = B \land z = C) \to (y R z \leftrightarrow B R C)$
17	16	3adant1	$⊢ (x = A \land y = B \land z = C) \to (y R z \leftrightarrow B R C)$
18	15 17	anbi12d	$⊢ (x = A \land y = B \land z = C) \to ((x R y \land y R z) \leftrightarrow (A R B \land B R C))$
19		breq12	$⊢ (x = A \land z = C) \to (x R z \leftrightarrow A R C)$
20	19	3adant2	$⊢ (x = A \land y = B \land z = C) \to (x R z \leftrightarrow A R C)$
21	18 20	imbi12d	$⊢ (x = A \land y = B \land z = C) \to (((x R y \land y R z) \to x R z) \leftrightarrow ((A R B \land B R C) \to A R C))$
22	21	spc3gv	$⊢ (A \in V \land B \in V \land C \in V) \to (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to ((A R B \land B R C) \to A R C))$
23	13 22	syl5	$⊢ (A \in V \land B \in V \land C \in V) \to (R \in DirRel \to ((A R B \land B R C) \to A R C))$
24	23	3expia	$⊢ (A \in V \land B \in V) \to (C \in V \to (R \in DirRel \to ((A R B \land B R C) \to A R C)))$
25	24	com4t	$⊢ R \in DirRel \to ((A R B \land B R C) \to ((A \in V \land B \in V) \to (C \in V \to A R C)))$
26	7 25	mpdd	$⊢ R \in DirRel \to ((A R B \land B R C) \to (C \in V \to A R C))$
27	26	imp31	$⊢ ((R \in DirRel \land (A R B \land B R C)) \land C \in V) \to A R C$
28	27	an32s	$⊢ ((R \in DirRel \land C \in V) \land (A R B \land B R C)) \to A R C$

Metamath Proof Explorer

Theorem dirtr

Proof