Metamath Proof Explorer


Table of Contents - 5.8. Reflexive and transitive closures of relations

A relation, , has the reflexive property if holds whenever is an element which could be related by the relation, namely, an element of its domain or range. Eliminating dummy variables, we see that a segment of the identity relation must be a subset of the relation, or . See idref.

A relation, , has the transitive property if holds whenever there exists an intermediate value such that both and hold. This can be expressed without dummy variables as . See cotr.

The transitive closure of a relation, , is the smallest superset of the relation which has the transitive property. Likewise, the reflexive-transitive closure, , is the smallest superset which has both the reflexive and transitive properties.

Not to be confused with the transitive closure of a set, trcl, which is a closure relative to a different transitive property, df-tr.

  1. The reflexive and transitive properties of relations
    1. coss12d
    2. trrelssd
    3. xpcogend
    4. xpcoidgend
    5. cotr2g
    6. cotr2
    7. cotr3
    8. coemptyd
    9. xptrrel
    10. 0trrel
  2. Basic properties of closures
    1. cleq1lem
    2. cleq1
    3. clsslem
  3. Definitions and basic properties of transitive closures
    1. ctcl
    2. crtcl
    3. df-trcl
    4. df-rtrcl
    5. trcleq1
    6. trclsslem
    7. trcleq2lem
    8. cvbtrcl
    9. trcleq12lem
    10. trclexlem
    11. trclublem
    12. trclubi
    13. trclubgi
    14. trclub
    15. trclubg
    16. trclfv
    17. brintclab
    18. brtrclfv
    19. brcnvtrclfv
    20. brtrclfvcnv
    21. brcnvtrclfvcnv
    22. trclfvss
    23. trclfvub
    24. trclfvlb
    25. trclfvcotr
    26. trclfvlb2
    27. trclfvlb3
    28. cotrtrclfv
    29. trclidm
    30. trclun
    31. trclfvg
    32. trclfvcotrg
    33. reltrclfv
    34. dmtrclfv
  4. Exponentiation of relations
    1. crelexp
    2. df-relexp
    3. reldmrelexp
    4. relexp0g
    5. relexp0
    6. relexp0d
    7. relexpsucnnr
    8. relexp1g
    9. dfid5
    10. dfid6
    11. relexp1d
    12. relexpsucnnl
    13. relexpsucl
    14. relexpsucr
    15. relexpsucrd
    16. relexpsucld
    17. relexpcnv
    18. relexpcnvd
    19. relexp0rel
    20. relexprelg
    21. relexprel
    22. relexpreld
    23. relexpnndm
    24. relexpdmg
    25. relexpdm
    26. relexpdmd
    27. relexpnnrn
    28. relexprng
    29. relexprn
    30. relexprnd
    31. relexpfld
    32. relexpfldd
    33. relexpaddnn
    34. relexpuzrel
    35. relexpaddg
    36. relexpaddd
  5. Reflexive-transitive closure as an indexed union
    1. crtrcl
    2. df-rtrclrec
    3. rtrclreclem1
    4. dfrtrclrec2
    5. rtrclreclem2
    6. rtrclreclem3
    7. rtrclreclem4
    8. dfrtrcl2
  6. Principle of transitive induction.
    1. relexpindlem
    2. relexpind
    3. rtrclind