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+ ‘ 𝑅 ) ) )