Theorem trclfvcotrg

Description: The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020)

	Ref	Expression
Assertion	trclfvcotrg	$$⊢\mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		trclfvcotr	$$⊢R\in \mathrm{V}\to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
2		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{t+}\left(R\right)=\varnothing$$
3		0trrel	$$⊢\varnothing \circ \varnothing \subseteq \varnothing$$
4	3	a1i	$$⊢\mathrm{t+}\left(R\right)=\varnothing \to \varnothing \circ \varnothing \subseteq \varnothing$$
5		id	$$⊢\mathrm{t+}\left(R\right)=\varnothing \to \mathrm{t+}\left(R\right)=\varnothing$$
6	5 5	coeq12d	$$⊢\mathrm{t+}\left(R\right)=\varnothing \to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)=\varnothing \circ \varnothing$$
7	4 6 5	3sstr4d	$$⊢\mathrm{t+}\left(R\right)=\varnothing \to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
8	2 7	syl	$$⊢\neg R\in \mathrm{V}\to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
9	1 8	pm2.61i	$$⊢\mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$