# 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 ∈ V → t+ ⁡ R -1 = t+ ⁡ R -1$

### Proof

Step Hyp Ref Expression
1 elex $⊢ R ∈ V → R ∈ V$
2 nnnn0 $⊢ n ∈ ℕ → n ∈ ℕ 0$
3 relexpcnv $⊢ n ∈ ℕ 0 ∧ R ∈ V → R ↑ r n -1 = R -1 ↑ r n$
4 2 3 sylan $⊢ n ∈ ℕ ∧ R ∈ V → R ↑ r n -1 = R -1 ↑ r n$
5 4 expcom $⊢ R ∈ V → n ∈ ℕ → R ↑ r n -1 = R -1 ↑ r n$
6 5 ralrimiv $⊢ R ∈ V → ∀ n ∈ ℕ R ↑ r n -1 = R -1 ↑ r n$
7 iuneq2 $⊢ ∀ n ∈ ℕ R ↑ r n -1 = R -1 ↑ r n → ⋃ n ∈ ℕ R ↑ r n -1 = ⋃ n ∈ ℕ R -1 ↑ r n$
8 6 7 syl $⊢ R ∈ V → ⋃ n ∈ ℕ R ↑ r n -1 = ⋃ n ∈ ℕ R -1 ↑ r n$
9 oveq1 $⊢ r = R → r ↑ r n = R ↑ r n$
10 9 iuneq2d $⊢ r = R → ⋃ n ∈ ℕ r ↑ r n = ⋃ n ∈ ℕ R ↑ r n$
11 dftrcl3 $⊢ t+ = r ∈ V ⟼ ⋃ n ∈ ℕ r ↑ r n$
12 nnex $⊢ ℕ ∈ V$
13 ovex $⊢ R ↑ r n ∈ V$
14 12 13 iunex $⊢ ⋃ n ∈ ℕ R ↑ r n ∈ V$
15 10 11 14 fvmpt $⊢ R ∈ V → t+ ⁡ R = ⋃ n ∈ ℕ R ↑ r n$
16 15 cnveqd $⊢ R ∈ V → t+ ⁡ R -1 = ⋃ n ∈ ℕ R ↑ r n -1$
17 cnviun $⊢ ⋃ n ∈ ℕ R ↑ r n -1 = ⋃ n ∈ ℕ R ↑ r n -1$
18 16 17 eqtrdi $⊢ R ∈ V → t+ ⁡ R -1 = ⋃ n ∈ ℕ R ↑ r n -1$
19 cnvexg $⊢ R ∈ V → R -1 ∈ V$
20 oveq1 $⊢ s = R -1 → s ↑ r n = R -1 ↑ r n$
21 20 iuneq2d $⊢ s = R -1 → ⋃ n ∈ ℕ s ↑ r n = ⋃ n ∈ ℕ R -1 ↑ r n$
22 dftrcl3 $⊢ t+ = s ∈ V ⟼ ⋃ n ∈ ℕ s ↑ r n$
23 ovex $⊢ R -1 ↑ r n ∈ V$
24 12 23 iunex $⊢ ⋃ n ∈ ℕ R -1 ↑ r n ∈ V$
25 21 22 24 fvmpt $⊢ R -1 ∈ V → t+ ⁡ R -1 = ⋃ n ∈ ℕ R -1 ↑ r n$
26 19 25 syl $⊢ R ∈ V → t+ ⁡ R -1 = ⋃ n ∈ ℕ R -1 ↑ r n$
27 8 18 26 3eqtr4d $⊢ R ∈ V → t+ ⁡ R -1 = t+ ⁡ R -1$
28 1 27 syl $⊢ R ∈ V → t+ ⁡ R -1 = t+ ⁡ R -1$