Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Definitions and basic properties of transitive closures
trclidm
Next ⟩
trclun
Metamath Proof Explorer
Ascii
Unicode
Theorem
trclidm
Description:
The transitive closure of a relation is idempotent.
(Contributed by
RP
, 29-Apr-2020)
Ref
Expression
Assertion
trclidm
⊢
R
∈
V
→
t+
⁡
t+
⁡
R
=
t+
⁡
R
Proof
Step
Hyp
Ref
Expression
1
fvex
⊢
t+
⁡
R
∈
V
2
trclfvcotr
⊢
R
∈
V
→
t+
⁡
R
∘
t+
⁡
R
⊆
t+
⁡
R
3
cotrtrclfv
⊢
t+
⁡
R
∈
V
∧
t+
⁡
R
∘
t+
⁡
R
⊆
t+
⁡
R
→
t+
⁡
t+
⁡
R
=
t+
⁡
R
4
1
2
3
sylancr
⊢
R
∈
V
→
t+
⁡
t+
⁡
R
=
t+
⁡
R