Metamath Proof Explorer


Theorem trclfvcom

Description: The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020)

Ref Expression
Assertion trclfvcom ( 𝑅𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 elex ( 𝑅𝑉𝑅 ∈ V )
2 relexpsucnnr ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( 𝑅𝑟 ( 𝑛 + 1 ) ) = ( ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) )
3 relexpsucnnl ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( 𝑅𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑛 ) ) )
4 2 3 eqtr3d ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( 𝑅𝑟 𝑛 ) ) )
5 4 iuneq2dv ( 𝑅 ∈ V → 𝑛 ∈ ℕ ( ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) = 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅𝑟 𝑛 ) ) )
6 oveq1 ( 𝑟 = 𝑅 → ( 𝑟𝑟 𝑛 ) = ( 𝑅𝑟 𝑛 ) )
7 6 iuneq2d ( 𝑟 = 𝑅 𝑛 ∈ ℕ ( 𝑟𝑟 𝑛 ) = 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) )
8 dftrcl3 t+ = ( 𝑟 ∈ V ↦ 𝑛 ∈ ℕ ( 𝑟𝑟 𝑛 ) )
9 nnex ℕ ∈ V
10 ovex ( 𝑅𝑟 𝑛 ) ∈ V
11 9 10 iunex 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) ∈ V
12 7 8 11 fvmpt ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) )
13 12 coeq1d ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) )
14 coiun1 ( 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) = 𝑛 ∈ ℕ ( ( 𝑅𝑟 𝑛 ) ∘ 𝑅 )
15 13 14 eqtrdi ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = 𝑛 ∈ ℕ ( ( 𝑅𝑟 𝑛 ) ∘ 𝑅 ) )
16 12 coeq2d ( 𝑅 ∈ V → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) = ( 𝑅 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) ) )
17 coiun ( 𝑅 𝑛 ∈ ℕ ( 𝑅𝑟 𝑛 ) ) = 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅𝑟 𝑛 ) )
18 16 17 eqtrdi ( 𝑅 ∈ V → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) = 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅𝑟 𝑛 ) ) )
19 5 15 18 3eqtr4d ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) )
20 1 19 syl ( 𝑅𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) )