Metamath Proof Explorer

Table of Contents - 9.2.1. Posets

1. cpo
2. cplt
3. club
4. cglb
5. cjn
6. cmee
7. df-poset
8. ispos
9. ispos2
10. posprs
11. posi
12. posref
13. posasymb
14. postr
15. 0pos
16. isposd
17. isposi
18. isposix
19. df-plt
20. pltfval
21. pltval
22. pltle
23. pltne
24. pltirr
25. pleval2i
26. pleval2
27. pltnle
28. pltval3
29. pltnlt
30. pltn2lp
31. plttr
32. pltletr
33. plelttr
34. pospo
35. df-lub
36. df-glb
37. df-join
38. df-meet
39. lubfval
40. lubdm
41. lubfun
42. lubeldm
43. lubelss
44. lubeu
45. lubval
46. lubcl
47. lubprop
48. luble
49. lublecllem
50. lublecl
51. lubid
52. glbfval
53. glbdm
54. glbfun
55. glbeldm
56. glbelss
57. glbeu
58. glbval
59. glbcl
60. glbprop
61. glble
62. joinfval
63. joinfval2
64. joindm
65. joindef
66. joinval
67. joincl
68. joindmss
69. joinval2lem
70. joinval2
71. joineu
72. joinlem
73. lejoin1
74. lejoin2
75. joinle
76. meetfval
77. meetfval2
78. meetdm
79. meetdef
80. meetval
81. meetcl
82. meetdmss
83. meetval2lem
84. meetval2
85. meeteu
86. meetlem
87. lemeet1
88. lemeet2
89. meetle
90. joincomALT
91. joincom
92. meetcomALT
93. meetcom
94. ctos
95. df-toset
96. istos
97. tosso
98. cp0
99. cp1
100. df-p0
101. df-p1
102. p0val
103. p1val
104. p0le
105. ple1