Theorem cnvtrclfv

Description: The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢R\in V\to R\in \mathrm{V}$$
2		nnnn0	$$⊢n\in \mathbb{N}\to n\in {\mathbb{N}}_0$$
3		relexpcnv	$$⊢\left(n\in {\mathbb{N}}_0\wedge R\in \mathrm{V}\right)\to {\left(R{\uparrow }_{r}n\right)}^{-1}=R^{-1}{\uparrow }_{r}n$$
4	2 3	sylan	$$⊢\left(n\in \mathbb{N}\wedge R\in \mathrm{V}\right)\to {\left(R{\uparrow }_{r}n\right)}^{-1}=R^{-1}{\uparrow }_{r}n$$
5	4	expcom	$$⊢R\in \mathrm{V}\to \left(n\in \mathbb{N}\to {\left(R{\uparrow }_{r}n\right)}^{-1}=R^{-1}{\uparrow }_{r}n\right)$$
6	5	ralrimiv	$$⊢R\in \mathrm{V}\to \forall n\in \mathbb{N}{\left(R{\uparrow }_{r}n\right)}^{-1}=R^{-1}{\uparrow }_{r}n$$
7		iuneq2	$$⊢\forall n\in \mathbb{N}{\left(R{\uparrow }_{r}n\right)}^{-1}=R^{-1}{\uparrow }_{r}n\to \bigcup _{n\in \mathbb{N}}{\left(R{\uparrow }_{r}n\right)}^{-1}=\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)$$
8	6 7	syl	$$⊢R\in \mathrm{V}\to \bigcup _{n\in \mathbb{N}}{\left(R{\uparrow }_{r}n\right)}^{-1}=\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)$$
9		oveq1	$$⊢r=R\to r{\uparrow }_{r}n=R{\uparrow }_{r}n$$
10	9	iuneq2d	$$⊢r=R\to \bigcup _{n\in \mathbb{N}}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in \mathbb{N}}\left(R{\uparrow }_{r}n\right)$$
11		dftrcl3	$$⊢\mathrm{t+}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \mathbb{N}}\left(r{\uparrow }_{r}n\right)\right)$$
12		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
13		ovex	$$⊢R{\uparrow }_{r}n\in \mathrm{V}$$
14	12 13	iunex	$$⊢\bigcup _{n\in \mathbb{N}}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
15	10 11 14	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{t+}\left(R\right)=\bigcup _{n\in \mathbb{N}}\left(R{\uparrow }_{r}n\right)$$
16	15	cnveqd	$$⊢R\in \mathrm{V}\to {\mathrm{t+}\left(R\right)}^{-1}={\bigcup _{n\in \mathbb{N}}\left(R{\uparrow }_{r}n\right)}^{-1}$$
17		cnviun	$$⊢{\bigcup _{n\in \mathbb{N}}\left(R{\uparrow }_{r}n\right)}^{-1}=\bigcup _{n\in \mathbb{N}}{\left(R{\uparrow }_{r}n\right)}^{-1}$$
18	16 17	eqtrdi	$$⊢R\in \mathrm{V}\to {\mathrm{t+}\left(R\right)}^{-1}=\bigcup _{n\in \mathbb{N}}{\left(R{\uparrow }_{r}n\right)}^{-1}$$
19		cnvexg	$$⊢R\in \mathrm{V}\to R^{-1}\in \mathrm{V}$$
20		oveq1	$$⊢s=R^{-1}\to s{\uparrow }_{r}n=R^{-1}{\uparrow }_{r}n$$
21	20	iuneq2d	$$⊢s=R^{-1}\to \bigcup _{n\in \mathbb{N}}\left(s{\uparrow }_{r}n\right)=\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)$$
22		dftrcl3	$$⊢\mathrm{t+}=\left(s\in \mathrm{V}⟼\bigcup _{n\in \mathbb{N}}\left(s{\uparrow }_{r}n\right)\right)$$
23		ovex	$$⊢R^{-1}{\uparrow }_{r}n\in \mathrm{V}$$
24	12 23	iunex	$$⊢\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)\in \mathrm{V}$$
25	21 22 24	fvmpt	$$⊢R^{-1}\in \mathrm{V}\to \mathrm{t+}\left(R^{-1}\right)=\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)$$
26	19 25	syl	$$⊢R\in \mathrm{V}\to \mathrm{t+}\left(R^{-1}\right)=\bigcup _{n\in \mathbb{N}}\left(R^{-1}{\uparrow }_{r}n\right)$$
27	8 18 26	3eqtr4d	$$⊢R\in \mathrm{V}\to {\mathrm{t+}\left(R\right)}^{-1}=\mathrm{t+}\left(R^{-1}\right)$$
28	1 27	syl	$$⊢R\in V\to {\mathrm{t+}\left(R\right)}^{-1}=\mathrm{t+}\left(R^{-1}\right)$$