Metamath Proof Explorer

Table of Contents - 2.4.30. Finite sets (cont.)

  1. onomeneq
  2. onfin
  3. onfin2
  4. nnfiOLD
  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. enfiiOLD
  27. pssnnOLD
  28. xpfir
  29. ssfid
  30. infi
  31. rabfi
  32. finresfin
  33. f1finf1o
  34. nfielex
  35. en1eqsn
  36. en1eqsnbi
  37. dif1enALT
  38. enp1ilem
  39. enp1i
  40. en2
  41. en3
  42. en4
  43. findcard2OLD
  44. findcard3
  45. ac6sfi
  46. frfi
  47. fimax2g
  48. fimaxg
  49. fisupg
  50. wofi
  51. ordunifi
  52. nnunifi
  53. unblem1
  54. unblem2
  55. unblem3
  56. unblem4
  57. unbnn
  58. unbnn2
  59. isfinite2
  60. nnsdomg
  61. isfiniteg
  62. infsdomnn
  63. infn0
  64. fin2inf
  65. unfilem1
  66. unfilem2
  67. unfilem3
  68. unfiOLD
  69. unfir
  70. unfi2
  71. difinf
  72. xpfi
  73. 3xpfi
  74. domunfican
  75. infcntss
  76. prfi
  77. tpfi
  78. fiint
  79. fodomfi
  80. fodomfib
  81. fofinf1o
  82. rneqdmfinf1o
  83. fidomdm
  84. dmfi
  85. fundmfibi
  86. resfnfinfin
  87. residfi
  88. cnvfiALT
  89. rnfi
  90. f1dmvrnfibi
  91. f1vrnfibi
  92. fofi
  93. f1fi
  94. iunfi
  95. unifi
  96. unifi2
  97. infssuni
  98. unirnffid
  99. imafiALT
  100. pwfilemOLD
  101. pwfiOLD
  102. mapfi
  103. ixpfi
  104. ixpfi2
  105. mptfi
  106. abrexfi
  107. cnvimamptfin
  108. elfpw
  109. unifpw
  110. f1opwfi
  111. fissuni
  112. fipreima
  113. finsschain
  114. indexfi