Metamath Proof Explorer

Table of Contents - 2.6.17. Eight inequivalent definitions of finite set

1. sornom
2. cfin1a
3. cfin2
4. cfin4
5. cfin3
6. cfin5
7. cfin6
8. cfin7
9. df-fin1a
10. df-fin2
11. df-fin4
12. df-fin3
13. df-fin5
14. df-fin6
15. df-fin7
16. isfin1a
17. fin1ai
18. isfin2
19. fin2i
20. isfin3
21. isfin4
22. fin4i
23. isfin5
24. isfin6
25. isfin7
26. sdom2en01
27. infpssrlem1
28. infpssrlem2
29. infpssrlem3
30. infpssrlem4
31. infpssrlem5
32. infpssr
33. fin4en1
34. ssfin4
35. domfin4
36. ominf4
37. infpssALT
38. isfin4-2
39. isfin4p1
40. fin23lem7
41. fin23lem11
42. fin2i2
43. isfin2-2
44. ssfin2
45. enfin2i
46. fin23lem24
47. fincssdom
48. fin23lem25
49. fin23lem26
50. fin23lem23
51. fin23lem22
52. fin23lem27
53. isfin3ds
54. ssfin3ds
55. fin23lem12
56. fin23lem13
57. fin23lem14
58. fin23lem15
59. fin23lem16
60. fin23lem19
61. fin23lem20
62. fin23lem17
63. fin23lem21
64. fin23lem28
65. fin23lem29
66. fin23lem30
67. fin23lem31
68. fin23lem32
69. fin23lem33
70. fin23lem34
71. fin23lem35
72. fin23lem36
73. fin23lem38
74. fin23lem39
75. fin23lem40
76. fin23lem41
77. isf32lem1
78. isf32lem2
79. isf32lem3
80. isf32lem4
81. isf32lem5
82. isf32lem6
83. isf32lem7
84. isf32lem8
85. isf32lem9
86. isf32lem10
87. isf32lem11
88. isf32lem12
89. isfin32i
90. isf33lem
91. isfin3-2
92. isfin3-3
93. fin33i
94. compsscnvlem
95. compsscnv
96. isf34lem1
97. isf34lem2
98. compssiso
99. isf34lem3
100. compss
101. isf34lem4
102. isf34lem5
103. isf34lem7
104. isf34lem6
105. fin34i
106. isfin3-4
107. fin11a
108. enfin1ai
109. isfin1-2
110. isfin1-3
111. isfin1-4
112. dffin1-5
113. fin23
114. fin34
115. isfin5-2
116. fin45
117. fin56
118. fin17
119. fin67
120. isfin7-2
121. fin71num
122. dffin7-2
123. dfacfin7
124. fin1a2lem1
125. fin1a2lem2
126. fin1a2lem3
127. fin1a2lem4
128. fin1a2lem5
129. fin1a2lem6
130. fin1a2lem7
131. fin1a2lem8
132. fin1a2lem9
133. fin1a2lem10
134. fin1a2lem11
135. fin1a2lem12
136. fin1a2lem13
137. fin12
138. fin1a2s
139. fin1a2