Metamath Proof Explorer

Table of Contents - 2.6. ZF Set Theory - add the Axiom of Infinity

1. Introduce the Axiom of Infinity
   1. ax-inf
   2. zfinf
   3. axinf2
   4. ax-inf2
   5. zfinf2
2. Existence of omega (the set of natural numbers)
   1. omex
   2. axinf
   3. inf5
   4. omelon
   5. dfom3
   6. elom3
   7. dfom4
   8. dfom5
   9. oancom
   10. isfinite
   11. fict
   12. nnsdom
   13. omenps
   14. omensuc
   15. infdifsn
   16. infdiffi
   17. unbnn3
   18. noinfep
3. Cantor normal form
   1. ccnf
   2. df-cnf
   3. cantnffval
   4. cantnfdm
   5. cantnfvalf
   6. cantnfs
   7. cantnfcl
   8. cantnfval
   9. cantnfval2
   10. cantnfsuc
   11. cantnfle
   12. cantnflt
   13. cantnflt2
   14. cantnff
   15. cantnf0
   16. cantnfrescl
   17. cantnfres
   18. cantnfp1lem1
   19. cantnfp1lem2
   20. cantnfp1lem3
   21. cantnfp1
   22. oemapso
   23. oemapval
   24. oemapvali
   25. cantnflem1a
   26. cantnflem1b
   27. cantnflem1c
   28. cantnflem1d
   29. cantnflem1
   30. cantnflem2
   31. cantnflem3
   32. cantnflem4
   33. cantnf
   34. oemapwe
   35. cantnffval2
   36. cantnff1o
   37. wemapwe
   38. oef1o
   39. cnfcomlem
   40. cnfcom
   41. cnfcom2lem
   42. cnfcom2
   43. cnfcom3lem
   44. cnfcom3
   45. cnfcom3clem
   46. cnfcom3c
4. Transitive closure
   1. trcl
   2. tz9.1
   3. tz9.1c
   4. epfrs
   5. zfregs
   6. zfregs2
   7. setind
   8. setind2
   9. ctc
   10. df-tc
   11. tcvalg
   12. tcid
   13. tctr
   14. tcmin
   15. tc2
   16. tcsni
   17. tcss
   18. tcel
   19. tcidm
   20. tc0
   21. tc00
5. Rank
   1. cr1
   2. crnk
   3. df-r1
   4. df-rank
   5. r1funlim
   6. r1fnon
   7. r10
   8. r1sucg
   9. r1suc
   10. r1limg
   11. r1lim
   12. r1fin
   13. r1sdom
   14. r111
   15. r1tr
   16. r1tr2
   17. r1ordg
   18. r1ord3g
   19. r1ord
   20. r1ord2
   21. r1ord3
   22. r1sssuc
   23. r1pwss
   24. r1sscl
   25. r1val1
   26. tz9.12lem1
   27. tz9.12lem2
   28. tz9.12lem3
   29. tz9.12
   30. tz9.13
   31. tz9.13g
   32. rankwflemb
   33. rankf
   34. rankon
   35. r1elwf
   36. rankvalb
   37. rankr1ai
   38. rankvaln
   39. rankidb
   40. rankdmr1
   41. rankr1ag
   42. rankr1bg
   43. r1rankidb
   44. r1elssi
   45. r1elss
   46. pwwf
   47. sswf
   48. snwf
   49. unwf
   50. prwf
   51. opwf
   52. unir1
   53. jech9.3
   54. rankwflem
   55. rankval
   56. rankvalg
   57. rankval2
   58. uniwf
   59. rankr1clem
   60. rankr1c
   61. rankidn
   62. rankpwi
   63. rankelb
   64. wfelirr
   65. rankval3b
   66. ranksnb
   67. rankonidlem
   68. rankonid
   69. onwf
   70. onssr1
   71. rankr1g
   72. rankid
   73. rankr1
   74. ssrankr1
   75. rankr1a
   76. r1val2
   77. r1val3
   78. rankel
   79. rankval3
   80. bndrank
   81. unbndrank
   82. rankpw
   83. ranklim
   84. r1pw
   85. r1pwALT
   86. r1pwcl
   87. rankssb
   88. rankss
   89. rankunb
   90. rankprb
   91. rankopb
   92. rankuni2b
   93. ranksn
   94. rankuni2
   95. rankun
   96. rankpr
   97. rankop
   98. r1rankid
   99. rankeq0b
   100. rankeq0
   101. rankr1id
   102. rankuni
   103. rankr1b
   104. ranksuc
   105. rankuniss
   106. rankval4
   107. rankbnd
   108. rankbnd2
   109. rankc1
   110. rankc2
   111. rankelun
   112. rankelpr
   113. rankelop
   114. rankxpl
   115. rankxpu
   116. rankfu
   117. rankmapu
   118. rankxplim
   119. rankxplim2
   120. rankxplim3
   121. rankxpsuc
   122. tcwf
   123. tcrank
6. Scott's trick; collection principle; Hilbert's epsilon
   1. scottex
   2. scott0
   3. scottexs
   4. scott0s
   5. cplem1
   6. cplem2
   7. cp
   8. bnd
   9. bnd2
   10. kardex
   11. karden
   12. htalem
   13. hta
7. Disjoint union
   1. cdju
   2. cinl
   3. cinr
   4. df-dju
   5. df-inl
   6. df-inr
   7. djueq12
   8. djueq1
   9. djueq2
   10. nfdju
   11. djuex
   12. djuexb
   13. djulcl
   14. djurcl
   15. djulf1o
   16. djurf1o
   17. inlresf
   18. inlresf1
   19. inrresf
   20. inrresf1
   21. djuin
   22. djur
   23. djuss
   24. djuunxp
   25. djuexALT
   26. eldju1st
   27. eldju2ndl
   28. eldju2ndr
   29. djuun
   30. 1stinl
   31. 2ndinl
   32. 1stinr
   33. 2ndinr
   34. updjudhf
   35. updjudhcoinlf
   36. updjudhcoinrg
   37. updjud
8. 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. cardmin2
   65. pm54.43lem
   66. pm54.43
   67. pr2nelem
   68. pr2ne
   69. prdom2
   70. en2eqpr
   71. en2eleq
   72. en2other2
   73. dif1card
   74. leweon
   75. r0weon
   76. infxpenlem
   77. infxpen
   78. xpomen
   79. xpct
   80. infxpidm2
   81. infxpenc
   82. infxpenc2lem1
   83. infxpenc2lem2
   84. infxpenc2lem3
   85. infxpenc2
   86. iunmapdisj
   87. fseqenlem1
   88. fseqenlem2
   89. fseqdom
   90. fseqen
   91. infpwfidom
   92. dfac8alem
   93. dfac8a
   94. dfac8b
   95. dfac8clem
   96. dfac8c
   97. ac10ct
   98. ween
   99. ac5num
   100. ondomen
   101. numdom
   102. ssnum
   103. onssnum
   104. indcardi
   105. acnrcl
   106. acneq
   107. isacn
   108. acni
   109. acni2
   110. acni3
   111. acnlem
   112. numacn
   113. finacn
   114. acndom
   115. acnnum
   116. acnen
   117. acndom2
   118. acnen2
   119. fodomacn
   120. fodomnum
   121. fonum
   122. numwdom
   123. fodomfi2
   124. wdomfil
   125. infpwfien
   126. inffien
   127. wdomnumr
   128. alephfnon
   129. aleph0
   130. alephlim
   131. alephsuc
   132. alephon
   133. alephcard
   134. alephnbtwn
   135. alephnbtwn2
   136. alephordilem1
   137. alephordi
   138. alephord
   139. alephord2
   140. alephord2i
   141. alephord3
   142. alephsucdom
   143. alephsuc2
   144. alephdom
   145. alephgeom
   146. alephislim
   147. aleph11
   148. alephf1
   149. alephsdom
   150. alephdom2
   151. alephle
   152. cardaleph
   153. cardalephex
   154. infenaleph
   155. isinfcard
   156. iscard3
   157. cardnum
   158. alephinit
   159. carduniima
   160. cardinfima
   161. alephiso
   162. alephprc
   163. alephsson
   164. unialeph
   165. alephsmo
   166. alephf1ALT
   167. alephfplem1
   168. alephfplem2
   169. alephfplem3
   170. alephfplem4
   171. alephfp
   172. alephfp2
   173. alephval3
   174. alephsucpw2
   175. mappwen
   176. finnisoeu
   177. iunfictbso
9. Axiom of Choice equivalents
   1. wac
   2. df-ac
   3. aceq1
   4. aceq0
   5. aceq2
   6. aceq3lem
   7. dfac3
   8. dfac4
   9. dfac5lem1
   10. dfac5lem2
   11. dfac5lem3
   12. dfac5lem4
   13. dfac5lem5
   14. dfac5
   15. dfac2a
   16. dfac2b
   17. dfac2
   18. dfac7
   19. dfac0
   20. dfac1
   21. dfac8
   22. dfac9
   23. dfac10
   24. dfac10c
   25. dfac10b
   26. acacni
   27. dfacacn
   28. dfac13
   29. dfac12lem1
   30. dfac12lem2
   31. dfac12lem3
   32. dfac12r
   33. dfac12k
   34. dfac12a
   35. dfac12
   36. kmlem1
   37. kmlem2
   38. kmlem3
   39. kmlem4
   40. kmlem5
   41. kmlem6
   42. kmlem7
   43. kmlem8
   44. kmlem9
   45. kmlem10
   46. kmlem11
   47. kmlem12
   48. kmlem13
   49. kmlem14
   50. kmlem15
   51. kmlem16
   52. dfackm
10. Cardinal number arithmetic
    1. undjudom
    2. endjudisj
    3. djuen
    4. djuenun
    5. dju1en
    6. dju1dif
    7. dju1p1e2
    8. dju1p1e2ALT
    9. dju0en
    10. xp2dju
    11. djucomen
    12. djuassen
    13. xpdjuen
    14. mapdjuen
    15. pwdjuen
    16. djudom1
    17. djudom2
    18. djudoml
    19. djuxpdom
    20. djufi
    21. cdainflem
    22. djuinf
    23. infdju1
    24. pwdju1
    25. pwdjuidm
    26. djulepw
    27. onadju
    28. cardadju
    29. djunum
    30. unnum
    31. nnadju
    32. ficardun
    33. ficardun2
    34. pwsdompw
    35. unctb
    36. infdjuabs
    37. infunabs
    38. infdju
    39. infdif
    40. infdif2
    41. infxpdom
    42. infxpabs
    43. infunsdom1
    44. infunsdom
    45. infxp
    46. pwdjudom
    47. infpss
    48. infmap2
11. The Ackermann bijection
    1. ackbij2lem1
    2. ackbij1lem1
    3. ackbij1lem2
    4. ackbij1lem3
    5. ackbij1lem4
    6. ackbij1lem5
    7. ackbij1lem6
    8. ackbij1lem7
    9. ackbij1lem8
    10. ackbij1lem9
    11. ackbij1lem10
    12. ackbij1lem11
    13. ackbij1lem12
    14. ackbij1lem13
    15. ackbij1lem14
    16. ackbij1lem15
    17. ackbij1lem16
    18. ackbij1lem17
    19. ackbij1lem18
    20. ackbij1
    21. ackbij1b
    22. ackbij2lem2
    23. ackbij2lem3
    24. ackbij2lem4
    25. ackbij2
    26. r1om
    27. fictb
12. Cofinality (without Axiom of Choice)
    1. cflem
    2. cfval
    3. cff
    4. cfub
    5. cflm
    6. cf0
    7. cardcf
    8. cflecard
    9. cfle
    10. cfon
    11. cfeq0
    12. cfsuc
    13. cff1
    14. cfflb
    15. cfval2
    16. coflim
    17. cflim3
    18. cflim2
    19. cfom
    20. cfss
    21. cfslb
    22. cfslbn
    23. cfslb2n
    24. cofsmo
    25. cfsmolem
    26. cfsmo
    27. cfcoflem
    28. coftr
    29. cfcof
    30. cfidm
    31. alephsing
13. 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
14. Hereditarily size-limited sets without Choice
    1. itunifval
    2. itunifn
    3. ituni0
    4. itunisuc
    5. itunitc1
    6. itunitc
    7. ituniiun
    8. hsmexlem7
    9. hsmexlem8
    10. hsmexlem9
    11. hsmexlem1
    12. hsmexlem2
    13. hsmexlem3
    14. hsmexlem4
    15. hsmexlem5
    16. hsmexlem6
    17. hsmex
    18. hsmex2
    19. hsmex3