Metamath Proof Explorer

Table of Contents - 19.8. Cover relation, atoms, exchange axiom, and modular symmetry

1. Covers relation; modular pairs
   1. df-cv
   2. df-md
   3. df-dmd
   4. cvbr
   5. cvbr2
   6. cvcon3
   7. cvpss
   8. cvnbtwn
   9. cvnbtwn2
   10. cvnbtwn3
   11. cvnbtwn4
   12. cvnsym
   13. cvnref
   14. cvntr
   15. spansncv2
   16. mdbr
   17. mdi
   18. mdbr2
   19. mdbr3
   20. mdbr4
   21. dmdbr
   22. dmdmd
   23. mddmd
   24. dmdi
   25. dmdbr2
   26. dmdi2
   27. dmdbr3
   28. dmdbr4
   29. dmdi4
   30. dmdbr5
   31. mddmd2
   32. mdsl0
   33. ssmd1
   34. ssmd2
   35. ssdmd1
   36. ssdmd2
   37. dmdsl3
   38. mdsl3
   39. mdslle1i
   40. mdslle2i
   41. mdslj1i
   42. mdslj2i
   43. mdsl1i
   44. mdsl2i
   45. mdsl2bi
   46. cvmdi
   47. mdslmd1lem1
   48. mdslmd1lem2
   49. mdslmd1lem3
   50. mdslmd1lem4
   51. mdslmd1i
   52. mdslmd2i
   53. mdsldmd1i
   54. mdslmd3i
   55. mdslmd4i
   56. csmdsymi
   57. mdexchi
   58. cvmd
   59. cvdmd
2. Atoms
   1. df-at
   2. ela
   3. elat2
   4. elatcv0
   5. atcv0
   6. atssch
   7. atelch
   8. atne0
   9. atss
   10. atsseq
   11. atcveq0
   12. h1da
   13. spansna
   14. sh1dle
   15. ch1dle
   16. atom1d
3. Superposition principle
   1. superpos
4. Atoms, exchange and covering properties, atomicity
   1. chcv1
   2. chcv2
   3. chjatom
   4. shatomici
   5. hatomici
   6. hatomic
   7. shatomistici
   8. hatomistici
   9. chpssati
   10. chrelati
   11. chrelat2i
   12. cvati
   13. cvbr4i
   14. cvexchlem
   15. cvexchi
   16. chrelat2
   17. chrelat3
   18. chrelat3i
   19. chrelat4i
   20. cvexch
   21. cvp
   22. atnssm0
   23. atnemeq0
   24. atssma
   25. atcv0eq
   26. atcv1
   27. atexch
   28. atomli
   29. atoml2i
   30. atordi
   31. atcvatlem
   32. atcvati
   33. atcvat2i
   34. atord
   35. atcvat2
5. Irreducibility
   1. chirredlem1
   2. chirredlem2
   3. chirredlem3
   4. chirredlem4
   5. chirredi
   6. chirred
6. Atoms (cont.)
   1. atcvat3i
   2. atcvat4i
   3. atdmd
   4. atmd
   5. atmd2
   6. atabsi
   7. atabs2i
7. Modular symmetry
   1. mdsymlem1
   2. mdsymlem2
   3. mdsymlem3
   4. mdsymlem4
   5. mdsymlem5
   6. mdsymlem6
   7. mdsymlem7
   8. mdsymlem8
   9. mdsymi
   10. mdsym
   11. dmdsym
   12. atdmd2
   13. sumdmdii
   14. cmmdi
   15. cmdmdi
   16. sumdmdlem
   17. sumdmdlem2
   18. sumdmdi
   19. dmdbr4ati
   20. dmdbr5ati
   21. dmdbr6ati
   22. dmdbr7ati
   23. mdoc1i
   24. mdoc2i
   25. dmdoc1i
   26. dmdoc2i
   27. mdcompli
   28. dmdcompli
   29. mddmdin0i
   30. cdjreui
   31. cdj1i
   32. cdj3lem1
   33. cdj3lem2
   34. cdj3lem2a
   35. cdj3lem2b
   36. cdj3lem3
   37. cdj3lem3a
   38. cdj3lem3b
   39. cdj3i