Theorem tcidm

Description: The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013)

	Ref	Expression
Assertion	tcidm	$$⊢\mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)=\mathrm{TC}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)$$
2		tctr	$$⊢\mathrm{Tr}\mathrm{TC}\left(A\right)$$
3		fvex	$$⊢\mathrm{TC}\left(A\right)\in \mathrm{V}$$
4		tcmin	$$⊢\mathrm{TC}\left(A\right)\in \mathrm{V}\to \left(\left(\mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)\wedge \mathrm{Tr}\mathrm{TC}\left(A\right)\right)\to \mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)\subseteq \mathrm{TC}\left(A\right)\right)$$
5	3 4	ax-mp	$$⊢\left(\mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)\wedge \mathrm{Tr}\mathrm{TC}\left(A\right)\right)\to \mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)\subseteq \mathrm{TC}\left(A\right)$$
6	1 2 5	mp2an	$$⊢\mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)\subseteq \mathrm{TC}\left(A\right)$$
7		tcid	$$⊢\mathrm{TC}\left(A\right)\in \mathrm{V}\to \mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)$$
8	3 7	ax-mp	$$⊢\mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)$$
9	6 8	eqssi	$$⊢\mathrm{TC}\left(\mathrm{TC}\left(A\right)\right)=\mathrm{TC}\left(A\right)$$