Metamath Proof Explorer

Table of Contents - 2.6.12. Cardinal numbers

  1. ccrd
  2. cale
  3. ccf
  4. wacn
  5. df-card
  6. df-aleph
  7. df-cf
  8. df-acn
  9. cardf2
  10. cardon
  11. isnum2
  12. isnumi
  13. ennum
  14. finnum
  15. onenon
  16. tskwe
  17. xpnum
  18. cardval3
  19. cardid2
  20. isnum3
  21. oncardval
  22. oncardid
  23. cardonle
  24. card0
  25. cardidm
  26. oncard
  27. ficardom
  28. ficardid
  29. cardnn
  30. cardnueq0
  31. cardne
  32. carden2a
  33. carden2b
  34. card1
  35. cardsn
  36. carddomi2
  37. sdomsdomcardi
  38. cardlim
  39. cardsdomelir
  40. cardsdomel
  41. iscard
  42. iscard2
  43. carddom2
  44. harcard
  45. cardprclem
  46. cardprc
  47. carduni
  48. cardiun
  49. cardennn
  50. cardsucinf
  51. cardsucnn
  52. cardom
  53. carden2
  54. cardsdom2
  55. domtri2
  56. nnsdomel
  57. cardval2
  58. isinffi
  59. fidomtri
  60. fidomtri2
  61. harsdom
  62. onsdom
  63. harval2
  64. harsucnn
  65. cardmin2
  66. pm54.43lem
  67. pm54.43
  68. pr2nelem
  69. pr2ne
  70. prdom2
  71. en2eqpr
  72. en2eleq
  73. en2other2
  74. dif1card
  75. leweon
  76. r0weon
  77. infxpenlem
  78. infxpen
  79. xpomen
  80. xpct
  81. infxpidm2
  82. infxpenc
  83. infxpenc2lem1
  84. infxpenc2lem2
  85. infxpenc2lem3
  86. infxpenc2
  87. iunmapdisj
  88. fseqenlem1
  89. fseqenlem2
  90. fseqdom
  91. fseqen
  92. infpwfidom
  93. dfac8alem
  94. dfac8a
  95. dfac8b
  96. dfac8clem
  97. dfac8c
  98. ac10ct
  99. ween
  100. ac5num
  101. ondomen
  102. numdom
  103. ssnum
  104. onssnum
  105. indcardi
  106. acnrcl
  107. acneq
  108. isacn
  109. acni
  110. acni2
  111. acni3
  112. acnlem
  113. numacn
  114. finacn
  115. acndom
  116. acnnum
  117. acnen
  118. acndom2
  119. acnen2
  120. fodomacn
  121. fodomnum
  122. fonum
  123. numwdom
  124. fodomfi2
  125. wdomfil
  126. infpwfien
  127. inffien
  128. wdomnumr
  129. alephfnon
  130. aleph0
  131. alephlim
  132. alephsuc
  133. alephon
  134. alephcard
  135. alephnbtwn
  136. alephnbtwn2
  137. alephordilem1
  138. alephordi
  139. alephord
  140. alephord2
  141. alephord2i
  142. alephord3
  143. alephsucdom
  144. alephsuc2
  145. alephdom
  146. alephgeom
  147. alephislim
  148. aleph11
  149. alephf1
  150. alephsdom
  151. alephdom2
  152. alephle
  153. cardaleph
  154. cardalephex
  155. infenaleph
  156. isinfcard
  157. iscard3
  158. cardnum
  159. alephinit
  160. carduniima
  161. cardinfima
  162. alephiso
  163. alephprc
  164. alephsson
  165. unialeph
  166. alephsmo
  167. alephf1ALT
  168. alephfplem1
  169. alephfplem2
  170. alephfplem3
  171. alephfplem4
  172. alephfp
  173. alephfp2
  174. alephval3
  175. alephsucpw2
  176. mappwen
  177. finnisoeu
  178. iunfictbso