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 of a relation
   1. cttrcl
   2. df-ttrcl
   3. ttrcleq
   4. nfttrcld
   5. nfttrcl
   6. relttrcl
   7. brttrcl
   8. brttrcl2
   9. ssttrcl
   10. ttrcltr
   11. ttrclresv
   12. ttrclco
   13. cottrcl
   14. ttrclss
   15. dmttrcl
   16. rnttrcl
   17. ttrclexg
   18. dfttrcl2
   19. ttrclselem1
   20. ttrclselem2
   21. ttrclse
5. Transitive closure under a relationship
   1. ctrpred
   2. df-trpred
   3. dftrpred2
   4. trpredeq1
   5. trpredeq2
   6. trpredeq3
   7. trpredeq1d
   8. trpredeq2d
   9. trpredeq3d
   10. eltrpred
   11. trpredlem1
   12. trpredpred
   13. trpredss
   14. trpredtr
   15. trpredmintr
   16. trpred0
   17. trpredelss
   18. dftrpred3g
   19. dftrpred4g
   20. trpredpo
   21. trpredrec
   22. trpredex
6. 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
7. Well-Founded Induction
   1. frmin
   2. frminOLD
   3. frind
   4. frinsg
   5. frins
   6. frins2f
   7. frins2
   8. frins3
8. Well-Founded Recursion
   1. frr3g
   2. frrlem15
   3. frrlem16
   4. frr1
   5. frr2
   6. frr3
9. 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
10. 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
11. 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
12. 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. harsucnn
    65. cardmin2
    66. pm54.43lem
    67. pm54.43
    68. pr2nelem
    69. pr2ne
    70. prdom2
    71. en2eqpr
    72. en2eleq
    73. en2other2
    74. dif1card
    75. leweon
    76. r0weon
    77. infxpenlem
    78. infxpen
    79. xpomen
    80. xpct
    81. infxpidm2
    82. infxpenc
    83. infxpenc2lem1
    84. infxpenc2lem2
    85. infxpenc2lem3
    86. infxpenc2
    87. iunmapdisj
    88. fseqenlem1
    89. fseqenlem2
    90. fseqdom
    91. fseqen
    92. infpwfidom
    93. dfac8alem
    94. dfac8a
    95. dfac8b
    96. dfac8clem
    97. dfac8c
    98. ac10ct
    99. ween
    100. ac5num
    101. ondomen
    102. numdom
    103. ssnum
    104. onssnum
    105. indcardi
    106. acnrcl
    107. acneq
    108. isacn
    109. acni
    110. acni2
    111. acni3
    112. acnlem
    113. numacn
    114. finacn
    115. acndom
    116. acnnum
    117. acnen
    118. acndom2
    119. acnen2
    120. fodomacn
    121. fodomnum
    122. fonum
    123. numwdom
    124. fodomfi2
    125. wdomfil
    126. infpwfien
    127. inffien
    128. wdomnumr
    129. alephfnon
    130. aleph0
    131. alephlim
    132. alephsuc
    133. alephon
    134. alephcard
    135. alephnbtwn
    136. alephnbtwn2
    137. alephordilem1
    138. alephordi
    139. alephord
    140. alephord2
    141. alephord2i
    142. alephord3
    143. alephsucdom
    144. alephsuc2
    145. alephdom
    146. alephgeom
    147. alephislim
    148. aleph11
    149. alephf1
    150. alephsdom
    151. alephdom2
    152. alephle
    153. cardaleph
    154. cardalephex
    155. infenaleph
    156. isinfcard
    157. iscard3
    158. cardnum
    159. alephinit
    160. carduniima
    161. cardinfima
    162. alephiso
    163. alephprc
    164. alephsson
    165. unialeph
    166. alephsmo
    167. alephf1ALT
    168. alephfplem1
    169. alephfplem2
    170. alephfplem3
    171. alephfplem4
    172. alephfp
    173. alephfp2
    174. alephval3
    175. alephsucpw2
    176. mappwen
    177. finnisoeu
    178. iunfictbso
13. 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
14. 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. nnadjuALT
    33. ficardadju
    34. ficardun
    35. ficardunOLD
    36. ficardun2
    37. ficardun2OLD
    38. pwsdompw
    39. unctb
    40. infdjuabs
    41. infunabs
    42. infdju
    43. infdif
    44. infdif2
    45. infxpdom
    46. infxpabs
    47. infunsdom1
    48. infunsdom
    49. infxp
    50. pwdjudom
    51. infpss
    52. infmap2
15. 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
16. 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
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
18. 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