Theorem trclfvcotrg

Description: The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020)

	Ref	Expression
Assertion	trclfvcotrg	⊢ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trclfvcotr	⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
2		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∅ )
3		0trrel	⊢ ( ∅ ∘ ∅ ) ⊆ ∅
4	3	a1i	⊢ ( ( t+ ‘ 𝑅 ) = ∅ → ( ∅ ∘ ∅ ) ⊆ ∅ )
5		id	⊢ ( ( t+ ‘ 𝑅 ) = ∅ → ( t+ ‘ 𝑅 ) = ∅ )
6	5 5	coeq12d	⊢ ( ( t+ ‘ 𝑅 ) = ∅ → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) = ( ∅ ∘ ∅ ) )
7	4 6 5	3sstr4d	⊢ ( ( t+ ‘ 𝑅 ) = ∅ → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
8	2 7	syl	⊢ ( ¬ 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
9	1 8	pm2.61i	⊢ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 )