Theorem trclfvlb3

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

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

Proof

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