Metamath Proof Explorer


Table of Contents - 2.4.28. Finite sets

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