Metamath Proof Explorer

Table of Contents - 2.4.28. Finite sets

  1. onomeneq
  2. onfin
  3. onfin2
  4. nnfi
  5. nndomo
  6. nnsdomo
  7. sucdom2
  8. sucdom
  9. 0sdom1dom
  10. 1sdom2
  11. sdom1
  12. modom
  13. modom2
  14. 1sdom
  15. unxpdomlem1
  16. unxpdomlem2
  17. unxpdomlem3
  18. unxpdom
  19. unxpdom2
  20. sucxpdom
  21. pssinf
  22. fisseneq
  23. ominf
  24. isinf
  25. fineqvlem
  26. fineqv
  27. enfi
  28. enfii
  29. pssnn
  30. ssnnfi
  31. ssfi
  32. domfi
  33. xpfir
  34. ssfid
  35. infi
  36. rabfi
  37. finresfin
  38. f1finf1o
  39. 0fin
  40. nfielex
  41. en1eqsn
  42. en1eqsnbi
  43. diffi
  44. dif1en
  45. enp1ilem
  46. enp1i
  47. en2
  48. en3
  49. en4
  50. findcard
  51. findcard2
  52. findcard2s
  53. findcard2d
  54. findcard3
  55. ac6sfi
  56. frfi
  57. fimax2g
  58. fimaxg
  59. fisupg
  60. wofi
  61. ordunifi
  62. nnunifi
  63. unblem1
  64. unblem2
  65. unblem3
  66. unblem4
  67. unbnn
  68. unbnn2
  69. isfinite2
  70. nnsdomg
  71. isfiniteg
  72. infsdomnn
  73. infn0
  74. fin2inf
  75. unfilem1
  76. unfilem2
  77. unfilem3
  78. unfi
  79. unfir
  80. unfi2
  81. difinf
  82. xpfi
  83. 3xpfi
  84. domunfican
  85. infcntss
  86. prfi
  87. tpfi
  88. fiint
  89. fnfi
  90. fodomfi
  91. fodomfib
  92. fofinf1o
  93. rneqdmfinf1o
  94. fidomdm
  95. dmfi
  96. fundmfibi
  97. resfnfinfin
  98. residfi
  99. cnvfi
  100. rnfi
  101. f1dmvrnfibi
  102. f1vrnfibi
  103. fofi
  104. f1fi
  105. iunfi
  106. unifi
  107. unifi2
  108. infssuni
  109. unirnffid
  110. imafi
  111. pwfilem
  112. pwfi
  113. mapfi
  114. ixpfi
  115. ixpfi2
  116. mptfi
  117. abrexfi
  118. cnvimamptfin
  119. elfpw
  120. unifpw
  121. f1opwfi
  122. fissuni
  123. fipreima
  124. finsschain
  125. indexfi