Theorem cottrcl

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

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

Proof

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