Metamath Proof Explorer

Table of Contents - 5.8.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