Metamath Proof Explorer

Table of Contents - 21.51.15.10. Universal property

1. upciclem1
2. upciclem2
3. upciclem3
4. upciclem4
5. upcic
6. upeu
7. upeu2
8. cup
9. df-up
10. reldmup
11. upfval
12. upfval2
13. upfval3
14. isuplem
15. isup
16. reldmup2
17. relup
18. uprcl
19. up1st2nd
20. up1st2ndr
21. up1st2ndb
22. up1st2nd2
23. uprcl2
24. uprcl3
25. uprcl4
26. uprcl5
27. isup2
28. upeu3
29. upeu4
30. uptposlem
31. uptpos
32. oppcuprcl4
33. oppcuprcl3
34. oppcuprcl5
35. oppcuprcl2
36. oppcup3lem
37. oppcup
38. oppcup2
39. oppcup3