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	⊢ ( 𝑅 ∈ 𝑉 → ◡ ( t+ ‘ 𝑅 ) = ( t+ ‘ ◡ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
2		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
3		relexpcnv	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑅 ∈ V ) → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) )
4	2 3	sylan	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑅 ∈ V ) → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) )
5	4	expcom	⊢ ( 𝑅 ∈ V → ( 𝑛 ∈ ℕ → ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) ) )
6	5	ralrimiv	⊢ ( 𝑅 ∈ V → ∀ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) )
7		iuneq2	⊢ ( ∀ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) → ∪ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) )
8	6 7	syl	⊢ ( 𝑅 ∈ V → ∪ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) )
9		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
10	9	iuneq2d	⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
11		dftrcl3	⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
12		nnex	⊢ ℕ ∈ V
13		ovex	⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
14	12 13	iunex	⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
15	10 11 14	fvmpt	⊢ ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
16	15	cnveqd	⊢ ( 𝑅 ∈ V → ◡ ( t+ ‘ 𝑅 ) = ◡ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
17		cnviun	⊢ ◡ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 )
18	16 17	eqtrdi	⊢ ( 𝑅 ∈ V → ◡ ( t+ ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ◡ ( 𝑅 ↑𝑟 𝑛 ) )
19		cnvexg	⊢ ( 𝑅 ∈ V → ◡ 𝑅 ∈ V )
20		oveq1	⊢ ( 𝑠 = ◡ 𝑅 → ( 𝑠 ↑𝑟 𝑛 ) = ( ◡ 𝑅 ↑𝑟 𝑛 ) )
21	20	iuneq2d	⊢ ( 𝑠 = ◡ 𝑅 → ∪ 𝑛 ∈ ℕ ( 𝑠 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) )
22		dftrcl3	⊢ t+ = ( 𝑠 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑠 ↑𝑟 𝑛 ) )
23		ovex	⊢ ( ◡ 𝑅 ↑𝑟 𝑛 ) ∈ V
24	12 23	iunex	⊢ ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) ∈ V
25	21 22 24	fvmpt	⊢ ( ◡ 𝑅 ∈ V → ( t+ ‘ ◡ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) )
26	19 25	syl	⊢ ( 𝑅 ∈ V → ( t+ ‘ ◡ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝑅 ↑𝑟 𝑛 ) )
27	8 18 26	3eqtr4d	⊢ ( 𝑅 ∈ V → ◡ ( t+ ‘ 𝑅 ) = ( t+ ‘ ◡ 𝑅 ) )
28	1 27	syl	⊢ ( 𝑅 ∈ 𝑉 → ◡ ( t+ ‘ 𝑅 ) = ( t+ ‘ ◡ 𝑅 ) )