Metamath Proof Explorer

Table of Contents - 5.6.11. The ` # ` (set size) function

1. chash
2. df-hash
3. hashkf
4. hashgval
5. hashginv
6. hashinf
7. hashbnd
8. hashfxnn0
9. hashf
10. hashxnn0
11. hashresfn
12. dmhashres
13. hashnn0pnf
14. hashnnn0genn0
15. hashnemnf
16. hashv01gt1
17. hashfz1
18. hashen
19. hasheni
20. hasheqf1o
21. fiinfnf1o
22. focdmex
23. hasheqf1oi
24. hashf1rn
25. hasheqf1od
26. fz1eqb
27. hashcard
28. hashcl
29. hashxrcl
30. hashclb
31. nfile
32. hashvnfin
33. hashnfinnn0
34. isfinite4
35. hasheq0
36. hashneq0
37. hashgt0n0
38. hashnncl
39. hash0
40. hashelne0d
41. hashsng
42. hashen1
43. hash1elsn
44. hashrabrsn
45. hashrabsn01
46. hashrabsn1
47. hashfn
48. fseq1hash
49. hashgadd
50. hashgval2
51. hashdom
52. hashdomi
53. hashsdom
54. hashun
55. hashun2
56. hashun3
57. hashinfxadd
58. hashunx
59. hashge0
60. hashgt0
61. hashge1
62. 1elfz0hash
63. hashnn0n0nn
64. hashunsng
65. hashunsngx
66. hashunsnggt
67. hashprg
68. elprchashprn2
69. hashprb
70. hashprdifel
71. prhash2ex
72. hashle00
73. hashgt0elex
74. hashgt0elexb
75. hashp1i
76. hash1
77. hash2
78. hash3
79. hash4
80. pr0hash2ex
81. hashss
82. prsshashgt1
83. hashin
84. hashssdif
85. hashdif
86. hashdifsn
87. hashdifpr
88. hashsn01
89. hashsnle1
90. hashsnlei
91. hash1snb
92. euhash1
93. hash1n0
94. hashgt12el
95. hashgt12el2
96. hashgt23el
97. hashunlei
98. hashsslei
99. hashfz
100. fzsdom2
101. hashfzo
102. hashfzo0
103. hashfzp1
104. hashfz0
105. hashxplem
106. hashxp
107. hashmap
108. hashpw
109. hashfun
110. hashres
111. hashreshashfun
112. hashimarn
113. hashimarni
114. resunimafz0
115. fnfz0hash
116. ffz0hash
117. fnfz0hashnn0
118. ffzo0hash
119. fnfzo0hash
120. fnfzo0hashnn0
121. hashbclem
122. hashbc
123. hashfacen
124. hashf1lem1
125. hashf1lem2
126. hashf1
127. hashfac
128. leiso
129. leisorel
130. fz1isolem
131. fz1iso
132. ishashinf
133. seqcoll
134. seqcoll2
135. phphashd
136. phphashrd
137. Proper unordered pairs and triples (sets of size 2 and 3)
     1. hashprlei
     2. hash2pr
     3. hash2prde
     4. hash2exprb
     5. hash2prb
     6. prprrab
     7. nehash2
     8. hash2prd
     9. hash2pwpr
     10. hashle2pr
     11. hashle2prv
     12. pr2pwpr
     13. hashge2el2dif
     14. hashge2el2difr
     15. hashge2el2difb
     16. hashdmpropge2
     17. hashtplei
     18. hashtpg
     19. hashge3el3dif
     20. elss2prb
     21. hash2sspr
     22. exprelprel
     23. hash3tr
     24. hash1to3
138. Functions with a domain containing at least two different elements
     1. fundmge2nop0
     2. fundmge2nop
     3. fun2dmnop0
     4. fun2dmnop
139. Finite induction on the size of the first component of a binary relation
     1. hashdifsnp1
     2. fi1uzind
     3. brfi1uzind
     4. brfi1ind
     5. brfi1indALT
     6. opfi1uzind
     7. opfi1ind