Metamath Proof Explorer

Table of Contents - 8.4.3. Hom functor

1. chof
2. cyon
3. df-hof
4. df-yon
5. hofval
6. hof1fval
7. hof1
8. hof2fval
9. hof2val
10. hof2
11. hofcllem
12. hofcl
13. oppchofcl
14. yonval
15. yoncl
16. yon1cl
17. yon11
18. yon12
19. yon2
20. hofpropd
21. yonpropd
22. oppcyon
23. oyoncl
24. oyon1cl
25. yonedalem1
26. yonedalem21
27. yonedalem3a
28. yonedalem4a
29. yonedalem4b
30. yonedalem4c
31. yonedalem22
32. yonedalem3b
33. yonedalem3
34. yonedainv
35. yonffthlem
36. yoneda
37. yonffth
38. yoniso