cottrcl

Description: Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024)

		Ref	Expression
	Assertion	cottrcl	$⊢ R \circ t++ R \subseteq t++ R$

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({R ↾}_{V})$
2		ssttrcl	$⊢ Rel ({R ↾}_{V}) \to {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
3	1 2	ax-mp	$⊢ {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
4		coss1	$⊢ {R ↾}_{V} \subseteq t++ ({R ↾}_{V}) \to ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) \subseteq t++ ({R ↾}_{V}) \circ t++ ({R ↾}_{V})$
5	3 4	ax-mp	$⊢ ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) \subseteq t++ ({R ↾}_{V}) \circ t++ ({R ↾}_{V})$
6		ttrcltr	$⊢ t++ ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) \subseteq t++ ({R ↾}_{V})$
7	5 6	sstri	$⊢ ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) \subseteq t++ ({R ↾}_{V})$
8		ssv	$⊢ ran t++ ({R ↾}_{V}) \subseteq V$
9		cores	$⊢ ran t++ ({R ↾}_{V}) \subseteq V \to ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) = R \circ t++ ({R ↾}_{V})$
10	8 9	ax-mp	$⊢ ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) = R \circ t++ ({R ↾}_{V})$
11		ttrclresv	$⊢ t++ ({R ↾}_{V}) = t++ R$
12	11	coeq2i	$⊢ R \circ t++ ({R ↾}_{V}) = R \circ t++ R$
13	10 12	eqtri	$⊢ ({R ↾}_{V}) \circ t++ ({R ↾}_{V}) = R \circ t++ R$
14	7 13 11	3sstr3i	$⊢ R \circ t++ R \subseteq t++ R$

Metamath Proof Explorer