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. hasheqf1oi
23. hashf1rn
24. hasheqf1od
25. fz1eqb
26. hashcard
27. hashcl
28. hashxrcl
29. hashclb
30. nfile
31. hashvnfin
32. hashnfinnn0
33. isfinite4
34. hasheq0
35. hashneq0
36. hashgt0n0
37. hashnncl
38. hash0
39. hashelne0d
40. hashsng
41. hashen1
42. hash1elsn
43. hashrabrsn
44. hashrabsn01
45. hashrabsn1
46. hashfn
47. fseq1hash
48. hashgadd
49. hashgval2
50. hashdom
51. hashdomi
52. hashsdom
53. hashun
54. hashun2
55. hashun3
56. hashinfxadd
57. hashunx
58. hashge0
59. hashgt0
60. hashge1
61. 1elfz0hash
62. hashnn0n0nn
63. hashunsng
64. hashunsngx
65. hashunsnggt
66. hashprg
67. elprchashprn2
68. hashprb
69. hashprdifel
70. prhash2ex
71. hashle00
72. hashgt0elex
73. hashgt0elexb
74. hashp1i
75. hash1
76. hash2
77. hash3
78. hash4
79. pr0hash2ex
80. hashss
81. prsshashgt1
82. hashin
83. hashssdif
84. hashdif
85. hashdifsn
86. hashdifpr
87. hashsn01
88. hashsnle1
89. hashsnlei
90. hash1snb
91. euhash1
92. hash1n0
93. hashgt12el
94. hashgt12el2
95. hashgt23el
96. hashunlei
97. hashsslei
98. hashfz
99. fzsdom2
100. hashfzo
101. hashfzo0
102. hashfzp1
103. hashfz0
104. hashxplem
105. hashxp
106. hashmap
107. hashpw
108. hashfun
109. hashres
110. hashreshashfun
111. hashimarn
112. hashimarni
113. hashfundm
114. hashf1dmrn
115. hashf1dmcdm
116. resunimafz0
117. fnfz0hash
118. ffz0hash
119. fnfz0hashnn0
120. ffzo0hash
121. fnfzo0hash
122. fnfzo0hashnn0
123. hashbclem
124. hashbc
125. hashfacen
126. hashf1lem1
127. hashf1lem2
128. hashf1
129. hashfac
130. leiso
131. leisorel
132. fz1isolem
133. fz1iso
134. ishashinf
135. seqcoll
136. seqcoll2
137. phphashd
138. phphashrd
139. 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. hash7g
     20. hashge3el3dif
     21. elss2prb
     22. hash2sspr
     23. exprelprel
     24. hash3tr
     25. hash1to3
     26. hash3tpde
     27. hash3tpexb
     28. hash3tpb
     29. tpf1ofv0
     30. tpf1ofv1
     31. tpf1ofv2
     32. tpf
     33. tpfo
     34. tpf1o
140. Functions with a domain containing at least two different elements
     1. fundmge2nop0
     2. fundmge2nop
     3. fun2dmnop0
     4. fun2dmnop
141. 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