Metamath Proof Explorer

Table of Contents - 20.33.2.23. Transitive closure of a relation

1. dftrcl3
2. brfvtrcld
3. fvtrcllb1d
4. trclfvcom
5. cnvtrclfv
6. cotrcltrcl
7. trclimalb2
8. brtrclfv2
9. trclfvdecomr
10. trclfvdecoml
11. dmtrclfvRP
12. rntrclfvRP
13. rntrclfv
14. dfrtrcl3
15. brfvrtrcld
16. fvrtrcllb0d
17. fvrtrcllb0da
18. fvrtrcllb1d
19. dfrtrcl4
20. corcltrcl
21. cortrcltrcl
22. corclrtrcl
23. cotrclrcl
24. cortrclrcl
25. cotrclrtrcl
26. cortrclrtrcl