Theorem trclfvlb2

Description: The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020)

	Ref	Expression
Assertion	trclfvlb2	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∘ 𝑅 ) ⊆ ( t+ ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		trclfvcotr	⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
2		trclfvlb	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
3	1 2 2	trrelssd	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∘ 𝑅 ) ⊆ ( t+ ‘ 𝑅 ) )