Metamath Proof Explorer

Table of Contents - 3.2. ZFC Set Theory - add the Axiom of Choice

  1. Introduce the Axiom of Choice
    1. ax-ac
    2. zfac
    3. ac2
    4. ac3
    5. ax-ac2
    6. axac3
    7. ackm
    8. axac2
    9. axac
    10. axaci
    11. cardeqv
    12. numth3
    13. numth2
    14. numth
    15. ac7
    16. ac7g
    17. ac4
    18. ac4c
    19. ac5
    20. ac5b
    21. ac6num
    22. ac6
    23. ac6c4
    24. ac6c5
    25. ac9
    26. ac6s
    27. ac6n
    28. ac6s2
    29. ac6s3
    30. ac6sg
    31. ac6sf
    32. ac6s4
    33. ac6s5
    34. ac8
    35. ac9s
  2. AC equivalents: well-ordering, Zorn's lemma
    1. numthcor
    2. weth
    3. zorn2lem1
    4. zorn2lem2
    5. zorn2lem3
    6. zorn2lem4
    7. zorn2lem5
    8. zorn2lem6
    9. zorn2lem7
    10. zorn2g
    11. zorng
    12. zornn0g
    13. zorn2
    14. zorn
    15. zornn0
    16. ttukeylem1
    17. ttukeylem2
    18. ttukeylem3
    19. ttukeylem4
    20. ttukeylem5
    21. ttukeylem6
    22. ttukeylem7
    23. ttukey2g
    24. ttukeyg
    25. ttukey
    26. axdclem
    27. axdclem2
    28. axdc
    29. fodomg
    30. fodom
    31. dmct
    32. dmctOLD
    33. rnct
    34. fodomb
    35. wdomac
    36. brdom3
    37. brdom5
    38. brdom4
    39. brdom7disj
    40. brdom6disj
    41. fin71ac
    42. imadomg
    43. imadomnum
    44. fimact
    45. fimactOLD
    46. fnrndomnum
    47. fnrndomg
    48. fnrndomgOLD
    49. fnct
    50. fnctOLD
    51. mptct
    52. iunfo
    53. iundom2g
    54. iundomg
    55. iundom
    56. unidom
    57. uniimadom
    58. uniimadomf
  3. Cardinal number theorems using Axiom of Choice
    1. cardval
    2. cardid
    3. cardidg
    4. cardidd
    5. cardf
    6. carden
    7. cardeq0
    8. unsnen
    9. carddom
    10. cardsdom
    11. domtri
    12. entric
    13. entri2
    14. entri3
    15. sdomsdomcard
    16. canth3
    17. infxpidm
    18. ondomon
    19. cardmin
    20. ficard
    21. infinfg
    22. infinf
    23. unirnfdomd
    24. konigthlem
    25. konigth
    26. alephsucpw
    27. aleph1
    28. alephval2
    29. dominfac
  4. Cardinal number arithmetic using Axiom of Choice
    1. iunctb
    2. unictb
    3. infmap
    4. alephadd
    5. alephmul
    6. alephexp1
    7. alephsuc3
    8. alephexp2
  5. Cofinality using the Axiom of Choice
    1. alephreg
    2. pwcfsdom
    3. cfpwsdom
    4. alephom
    5. smobeth