Theorem trclidm

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

	Ref	Expression
Assertion	trclidm	$$⊢R\in V\to \mathrm{t+}\left(\mathrm{t+}\left(R\right)\right)=\mathrm{t+}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢\mathrm{t+}\left(R\right)\in \mathrm{V}$$
2		trclfvcotr	$$⊢R\in V\to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
3		cotrtrclfv	$$⊢\left(\mathrm{t+}\left(R\right)\in \mathrm{V}\wedge \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\right)\to \mathrm{t+}\left(\mathrm{t+}\left(R\right)\right)=\mathrm{t+}\left(R\right)$$
4	1 2 3	sylancr	$$⊢R\in V\to \mathrm{t+}\left(\mathrm{t+}\left(R\right)\right)=\mathrm{t+}\left(R\right)$$