Theorem ttrclco

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

	Ref	Expression
Assertion	ttrclco	$$⊢\mathrm{t++}R\circ 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		coss2	$$⊢{R\upharpoonright }_{\mathrm{V}}\subseteq \mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\to \mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \left({R\upharpoonright }_{\mathrm{V}}\right)\subseteq \mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)$$
4	1 2 3	mp2b	$$⊢\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \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		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)$$
6	4 5	sstri	$$⊢\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \left({R\upharpoonright }_{\mathrm{V}}\right)\subseteq \mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)$$
7		relco	$$⊢\mathrm{Rel}\left(\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R\right)$$
8		dfrel3	$$⊢\mathrm{Rel}\left(\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R\right)\leftrightarrow {\left(\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R\right)\upharpoonright }_{\mathrm{V}}=\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R$$
9	7 8	mpbi	$$⊢{\left(\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R\right)\upharpoonright }_{\mathrm{V}}=\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R$$
10		resco	$$⊢{\left(\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R\right)\upharpoonright }_{\mathrm{V}}=\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \left({R\upharpoonright }_{\mathrm{V}}\right)$$
11		ttrclresv	$$⊢\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)=\mathrm{t++}R$$
12	11	coeq1i	$$⊢\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ R=\mathrm{t++}R\circ R$$
13	9 10 12	3eqtr3i	$$⊢\mathrm{t++}\left({R\upharpoonright }_{\mathrm{V}}\right)\circ \left({R\upharpoonright }_{\mathrm{V}}\right)=\mathrm{t++}R\circ R$$
14	6 13 11	3sstr3i	$$⊢\mathrm{t++}R\circ R\subseteq \mathrm{t++}R$$