# Metamath Proof Explorer

## 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 ℕ\to {n}\in {ℕ}_{0}$
3 relexpcnv ${⊢}\left({n}\in {ℕ}_{0}\wedge {R}\in \mathrm{V}\right)\to {\left({R}{↑}_{r}{n}\right)}^{-1}={{R}}^{-1}{↑}_{r}{n}$
4 2 3 sylan ${⊢}\left({n}\in ℕ\wedge {R}\in \mathrm{V}\right)\to {\left({R}{↑}_{r}{n}\right)}^{-1}={{R}}^{-1}{↑}_{r}{n}$
5 4 expcom ${⊢}{R}\in \mathrm{V}\to \left({n}\in ℕ\to {\left({R}{↑}_{r}{n}\right)}^{-1}={{R}}^{-1}{↑}_{r}{n}\right)$
6 5 ralrimiv ${⊢}{R}\in \mathrm{V}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({R}{↑}_{r}{n}\right)}^{-1}={{R}}^{-1}{↑}_{r}{n}$
7 iuneq2 ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({R}{↑}_{r}{n}\right)}^{-1}={{R}}^{-1}{↑}_{r}{n}\to \bigcup _{{n}\in ℕ}{\left({R}{↑}_{r}{n}\right)}^{-1}=\bigcup _{{n}\in ℕ}\left({{R}}^{-1}{↑}_{r}{n}\right)$
8 6 7 syl ${⊢}{R}\in \mathrm{V}\to \bigcup _{{n}\in ℕ}{\left({R}{↑}_{r}{n}\right)}^{-1}=\bigcup _{{n}\in ℕ}\left({{R}}^{-1}{↑}_{r}{n}\right)$
9 oveq1 ${⊢}{r}={R}\to {r}{↑}_{r}{n}={R}{↑}_{r}{n}$
10 9 iuneq2d ${⊢}{r}={R}\to \bigcup _{{n}\in ℕ}\left({r}{↑}_{r}{n}\right)=\bigcup _{{n}\in ℕ}\left({R}{↑}_{r}{n}\right)$
11 dftrcl3 ${⊢}\mathrm{t+}=\left({r}\in \mathrm{V}⟼\bigcup _{{n}\in ℕ}\left({r}{↑}_{r}{n}\right)\right)$
12 nnex ${⊢}ℕ\in \mathrm{V}$
13 ovex ${⊢}{R}{↑}_{r}{n}\in \mathrm{V}$
14 12 13 iunex ${⊢}\bigcup _{{n}\in ℕ}\left({R}{↑}_{r}{n}\right)\in \mathrm{V}$
15 10 11 14 fvmpt ${⊢}{R}\in \mathrm{V}\to \mathrm{t+}\left({R}\right)=\bigcup _{{n}\in ℕ}\left({R}{↑}_{r}{n}\right)$
16 15 cnveqd ${⊢}{R}\in \mathrm{V}\to {\mathrm{t+}\left({R}\right)}^{-1}={\bigcup _{{n}\in ℕ}\left({R}{↑}_{r}{n}\right)}^{-1}$
17 cnviun ${⊢}{\bigcup _{{n}\in ℕ}\left({R}{↑}_{r}{n}\right)}^{-1}=\bigcup _{{n}\in ℕ}{\left({R}{↑}_{r}{n}\right)}^{-1}$
18 16 17 eqtrdi ${⊢}{R}\in \mathrm{V}\to {\mathrm{t+}\left({R}\right)}^{-1}=\bigcup _{{n}\in ℕ}{\left({R}{↑}_{r}{n}\right)}^{-1}$
19 cnvexg ${⊢}{R}\in \mathrm{V}\to {{R}}^{-1}\in \mathrm{V}$
20 oveq1 ${⊢}{s}={{R}}^{-1}\to {s}{↑}_{r}{n}={{R}}^{-1}{↑}_{r}{n}$
21 20 iuneq2d ${⊢}{s}={{R}}^{-1}\to \bigcup _{{n}\in ℕ}\left({s}{↑}_{r}{n}\right)=\bigcup _{{n}\in ℕ}\left({{R}}^{-1}{↑}_{r}{n}\right)$
22 dftrcl3 ${⊢}\mathrm{t+}=\left({s}\in \mathrm{V}⟼\bigcup _{{n}\in ℕ}\left({s}{↑}_{r}{n}\right)\right)$
23 ovex ${⊢}{{R}}^{-1}{↑}_{r}{n}\in \mathrm{V}$
24 12 23 iunex ${⊢}\bigcup _{{n}\in ℕ}\left({{R}}^{-1}{↑}_{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 ℕ}\left({{R}}^{-1}{↑}_{r}{n}\right)$
26 19 25 syl ${⊢}{R}\in \mathrm{V}\to \mathrm{t+}\left({{R}}^{-1}\right)=\bigcup _{{n}\in ℕ}\left({{R}}^{-1}{↑}_{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)$