Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Definitions and basic properties of transitive closures
trclfvlb3
Next ⟩
cotrtrclfv
Metamath Proof Explorer
Ascii
Unicode
Theorem
trclfvlb3
Description:
The transitive closure of a relation has a lower bound.
(Contributed by
RP
, 8-May-2020)
Ref
Expression
Assertion
trclfvlb3
⊢
R
∈
V
→
R
∪
R
∘
R
⊆
t+
⁡
R
Proof
Step
Hyp
Ref
Expression
1
trclfvlb
⊢
R
∈
V
→
R
⊆
t+
⁡
R
2
trclfvlb2
⊢
R
∈
V
→
R
∘
R
⊆
t+
⁡
R
3
1
2
unssd
⊢
R
∈
V
→
R
∪
R
∘
R
⊆
t+
⁡
R