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. fodom
   30. fodomg
   31. dmct
   32. rnct
   33. fodomb
   34. wdomac
   35. brdom3
   36. brdom5
   37. brdom4
   38. brdom7disj
   39. brdom6disj
   40. fin71ac
   41. imadomg
   42. fimact
   43. fnrndomg
   44. fnct
   45. mptct
   46. iunfo
   47. iundom2g
   48. iundomg
   49. iundom
   50. unidom
   51. uniimadom
   52. 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. infinf
   22. unirnfdomd
   23. konigthlem
   24. konigth
   25. alephsucpw
   26. aleph1
   27. alephval2
   28. 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