trclfvcotr

Description: The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020)

		Ref	Expression
	Assertion	trclfvcotr	$⊢ R \in V \to t+ (R) \circ t+ (R) \subseteq t+ (R)$

Proof

Step	Hyp	Ref	Expression
1		cotr	$⊢ r \circ r \subseteq r \leftrightarrow \forall a \forall b \forall c ((a r b \land b r c) \to a r c)$
2		sp	$⊢ \forall a \forall b \forall c ((a r b \land b r c) \to a r c) \to \forall b \forall c ((a r b \land b r c) \to a r c)$
3	2	19.21bbi	$⊢ \forall a \forall b \forall c ((a r b \land b r c) \to a r c) \to ((a r b \land b r c) \to a r c)$
4	1 3	sylbi	$⊢ r \circ r \subseteq r \to ((a r b \land b r c) \to a r c)$
5	4	adantl	$⊢ (R \subseteq r \land r \circ r \subseteq r) \to ((a r b \land b r c) \to a r c)$
6	5	a2i	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to ((R \subseteq r \land r \circ r \subseteq r) \to a r c)$
7	6	alimi	$⊢ \forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c)$
8	7	ax-gen	$⊢ \forall c (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c))$
9	8	ax-gen	$⊢ \forall b \forall c (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c))$
10	9	ax-gen	$⊢ \forall a \forall b \forall c (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c))$
11		brtrclfv	$⊢ R \in V \to (a t+ (R) b \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r b))$
12		brtrclfv	$⊢ R \in V \to (b t+ (R) c \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to b r c))$
13	11 12	anbi12d	$⊢ R \in V \to ((a t+ (R) b \land b t+ (R) c) \leftrightarrow (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land \forall r ((R \subseteq r \land r \circ r \subseteq r) \to b r c)))$
14		jcab	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \leftrightarrow (((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land ((R \subseteq r \land r \circ r \subseteq r) \to b r c))$
15	14	albii	$⊢ \forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \leftrightarrow \forall r (((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land ((R \subseteq r \land r \circ r \subseteq r) \to b r c))$
16		19.26	$⊢ \forall r (((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land ((R \subseteq r \land r \circ r \subseteq r) \to b r c)) \leftrightarrow (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land \forall r ((R \subseteq r \land r \circ r \subseteq r) \to b r c))$
17	15 16	bitri	$⊢ \forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \leftrightarrow (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r b) \land \forall r ((R \subseteq r \land r \circ r \subseteq r) \to b r c))$
18	13 17	syl6bbr	$⊢ R \in V \to ((a t+ (R) b \land b t+ (R) c) \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)))$
19		brtrclfv	$⊢ R \in V \to (a t+ (R) c \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c))$
20	18 19	imbi12d	$⊢ R \in V \to (((a t+ (R) b \land b t+ (R) c) \to a t+ (R) c) \leftrightarrow (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c)))$
21	20	albidv	$⊢ R \in V \to (\forall c ((a t+ (R) b \land b t+ (R) c) \to a t+ (R) c) \leftrightarrow \forall c (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c)))$
22	21	2albidv	$⊢ R \in V \to (\forall a \forall b \forall c ((a t+ (R) b \land b t+ (R) c) \to a t+ (R) c) \leftrightarrow \forall a \forall b \forall c (\forall r ((R \subseteq r \land r \circ r \subseteq r) \to (a r b \land b r c)) \to \forall r ((R \subseteq r \land r \circ r \subseteq r) \to a r c)))$
23	10 22	mpbiri	$⊢ R \in V \to \forall a \forall b \forall c ((a t+ (R) b \land b t+ (R) c) \to a t+ (R) c)$
24		cotr	$⊢ t+ (R) \circ t+ (R) \subseteq t+ (R) \leftrightarrow \forall a \forall b \forall c ((a t+ (R) b \land b t+ (R) c) \to a t+ (R) c)$
25	23 24	sylibr	$⊢ R \in V \to t+ (R) \circ t+ (R) \subseteq t+ (R)$

Metamath Proof Explorer

Theorem trclfvcotr

Proof