Metamath Proof Explorer

Table of Contents - 20.6. Mathbox for Mario Carneiro

1. Predicate calculus with all distinct variables
   1. ax-7d
   2. ax-8d
   3. ax-9d1
   4. ax-9d2
   5. ax-10d
   6. ax-11d
2. Miscellaneous stuff
   1. quartfull
3. Derangements and the Subfactorial
   1. deranglem
   2. derangval
   3. derangf
   4. derang0
   5. derangsn
   6. derangenlem
   7. derangen
   8. subfacval
   9. derangen2
   10. subfacf
   11. subfaclefac
   12. subfac0
   13. subfac1
   14. subfacp1lem1
   15. subfacp1lem2a
   16. subfacp1lem2b
   17. subfacp1lem3
   18. subfacp1lem4
   19. subfacp1lem5
   20. subfacp1lem6
   21. subfacp1
   22. subfacval2
   23. subfaclim
   24. subfacval3
   25. derangfmla
4. The Erdős-Szekeres theorem
   1. erdszelem1
   2. erdszelem2
   3. erdszelem3
   4. erdszelem4
   5. erdszelem5
   6. erdszelem6
   7. erdszelem7
   8. erdszelem8
   9. erdszelem9
   10. erdszelem10
   11. erdszelem11
   12. erdsze
   13. erdsze2lem1
   14. erdsze2lem2
   15. erdsze2
5. Euler's partition theorem
6. The Kuratowski closure-complement theorem
   1. kur14lem1
   2. kur14lem2
   3. kur14lem3
   4. kur14lem4
   5. kur14lem5
   6. kur14lem6
   7. kur14lem7
   8. kur14lem8
   9. kur14lem9
   10. kur14lem10
   11. kur14
7. Retracts and sections
   1. cretr
   2. df-retr
8. Path-connected and simply connected spaces
   1. cpconn
   2. csconn
   3. df-pconn
   4. df-sconn
   5. ispconn
   6. pconncn
   7. pconntop
   8. issconn
   9. sconnpconn
   10. sconntop
   11. sconnpht
   12. cnpconn
   13. pconnconn
   14. txpconn
   15. ptpconn
   16. indispconn
   17. connpconn
   18. qtoppconn
   19. pconnpi1
   20. sconnpht2
   21. sconnpi1
   22. txsconnlem
   23. txsconn
   24. cvxpconn
   25. cvxsconn
   26. blsconn
   27. cnllysconn
   28. resconn
   29. ioosconn
   30. iccsconn
   31. retopsconn
   32. iccllysconn
   33. rellysconn
   34. iisconn
   35. iillysconn
   36. iinllyconn
9. Covering maps
   1. ccvm
   2. df-cvm
   3. fncvm
   4. cvmscbv
   5. iscvm
   6. cvmtop1
   7. cvmtop2
   8. cvmcn
   9. cvmcov
   10. cvmsrcl
   11. cvmsi
   12. cvmsval
   13. cvmsss
   14. cvmsn0
   15. cvmsuni
   16. cvmsdisj
   17. cvmshmeo
   18. cvmsf1o
   19. cvmscld
   20. cvmsss2
   21. cvmcov2
   22. cvmseu
   23. cvmsiota
   24. cvmopnlem
   25. cvmfolem
   26. cvmopn
   27. cvmliftmolem1
   28. cvmliftmolem2
   29. cvmliftmoi
   30. cvmliftmo
   31. cvmliftlem1
   32. cvmliftlem2
   33. cvmliftlem3
   34. cvmliftlem4
   35. cvmliftlem5
   36. cvmliftlem6
   37. cvmliftlem7
   38. cvmliftlem8
   39. cvmliftlem9
   40. cvmliftlem10
   41. cvmliftlem11
   42. cvmliftlem13
   43. cvmliftlem14
   44. cvmliftlem15
   45. cvmlift
   46. cvmfo
   47. cvmliftiota
   48. cvmlift2lem1
   49. cvmlift2lem9a
   50. cvmlift2lem2
   51. cvmlift2lem3
   52. cvmlift2lem4
   53. cvmlift2lem5
   54. cvmlift2lem6
   55. cvmlift2lem7
   56. cvmlift2lem8
   57. cvmlift2lem9
   58. cvmlift2lem10
   59. cvmlift2lem11
   60. cvmlift2lem12
   61. cvmlift2lem13
   62. cvmlift2
   63. cvmliftphtlem
   64. cvmliftpht
   65. cvmlift3lem1
   66. cvmlift3lem2
   67. cvmlift3lem3
   68. cvmlift3lem4
   69. cvmlift3lem5
   70. cvmlift3lem6
   71. cvmlift3lem7
   72. cvmlift3lem8
   73. cvmlift3lem9
   74. cvmlift3
10. Normal numbers
    1. snmlff
    2. snmlfval
    3. snmlval
    4. snmlflim
11. Compactification
12. Godel-sets of formulas - part 1
    1. cgoe
    2. cgna
    3. cgol
    4. csat
    5. cfmla
    6. csate
    7. cprv
    8. df-goel
    9. df-gona
    10. df-goal
    11. df-sat
    12. df-sate
    13. df-fmla
    14. df-prv
    15. goel
    16. goelel3xp
    17. goeleq12bg
    18. gonafv
    19. goaleq12d
    20. gonanegoal
    21. satf
    22. satfsucom
    23. satfn
    24. satom
    25. satfvsucom
    26. satfv0
    27. satfvsuclem1
    28. satfvsuclem2
    29. satfvsuc
    30. satfv1lem
    31. satfv1
    32. satfsschain
    33. satfvsucsuc
    34. satfbrsuc
    35. satfrel
    36. satfdmlem
    37. satfdm
    38. satfrnmapom
    39. satfv0fun
    40. satf0
    41. satf0sucom
    42. satf00
    43. satf0suclem
    44. satf0suc
    45. satf0op
    46. satf0n0
    47. sat1el2xp
    48. fmlafv
    49. fmla
    50. fmla0
    51. fmla0xp
    52. fmlasuc0
    53. fmlafvel
    54. fmlasuc
    55. fmla1
    56. isfmlasuc
    57. fmlasssuc
    58. fmlaomn0
    59. fmlan0
    60. gonan0
    61. goaln0
    62. gonarlem
    63. gonar
    64. goalrlem
    65. goalr
    66. fmla0disjsuc
    67. fmlasucdisj
    68. satfdmfmla
    69. satffunlem
    70. satffunlem1lem1
    71. satffunlem1lem2
    72. satffunlem2lem1
    73. dmopab3rexdif
    74. satffunlem2lem2
    75. satffunlem1
    76. satffunlem2
    77. satffun
    78. satff
    79. satfun
    80. satfvel
    81. satfv0fvfmla0
    82. satefv
    83. sate0
    84. satef
    85. sate0fv0
    86. satefvfmla0
    87. sategoelfvb
    88. sategoelfv
    89. ex-sategoelel
    90. ex-sategoel
    91. satfv1fvfmla1
    92. 2goelgoanfmla1
    93. satefvfmla1
    94. ex-sategoelelomsuc
    95. ex-sategoelel12
    96. prv
    97. elnanelprv
    98. prv0
    99. prv1n
13. Godel-sets of formulas - part 2
    1. cgon
    2. cgoa
    3. cgoi
    4. cgoo
    5. cgob
    6. cgoq
    7. cgox
    8. df-gonot
    9. df-goan
    10. df-goim
    11. df-goor
    12. df-gobi
    13. df-goeq
    14. df-goex
14. Models of ZF
    1. cgze
    2. cgzr
    3. cgzp
    4. cgzu
    5. cgzg
    6. cgzi
    7. cgzf
    8. df-gzext
    9. df-gzrep
    10. df-gzpow
    11. df-gzun
    12. df-gzreg
    13. df-gzinf
    14. df-gzf
15. Metamath formal systems
    1. cmcn
    2. cmvar
    3. cmty
    4. cmvt
    5. cmtc
    6. cmax
    7. cmrex
    8. cmex
    9. cmdv
    10. cmvrs
    11. cmrsub
    12. cmsub
    13. cmvh
    14. cmpst
    15. cmsr
    16. cmsta
    17. cmfs
    18. cmcls
    19. cmpps
    20. cmthm
    21. df-mcn
    22. df-mvar
    23. df-mty
    24. df-mtc
    25. df-mmax
    26. df-mvt
    27. df-mrex
    28. df-mex
    29. df-mdv
    30. df-mvrs
    31. df-mrsub
    32. df-msub
    33. df-mvh
    34. df-mpst
    35. df-msr
    36. df-msta
    37. df-mfs
    38. df-mcls
    39. df-mpps
    40. df-mthm
    41. mvtval
    42. mrexval
    43. mexval
    44. mexval2
    45. mdvval
    46. mvrsval
    47. mvrsfpw
    48. mrsubffval
    49. mrsubfval
    50. mrsubval
    51. mrsubcv
    52. mrsubvr
    53. mrsubff
    54. mrsubrn
    55. mrsubff1
    56. mrsubff1o
    57. mrsub0
    58. mrsubf
    59. mrsubccat
    60. mrsubcn
    61. elmrsubrn
    62. mrsubco
    63. mrsubvrs
    64. msubffval
    65. msubfval
    66. msubval
    67. msubrsub
    68. msubty
    69. elmsubrn
    70. msubrn
    71. msubff
    72. msubco
    73. msubf
    74. mvhfval
    75. mvhval
    76. mpstval
    77. elmpst
    78. msrfval
    79. msrval
    80. mpstssv
    81. mpst123
    82. mpstrcl
    83. msrf
    84. msrrcl
    85. mstaval
    86. msrid
    87. msrfo
    88. mstapst
    89. elmsta
    90. ismfs
    91. mfsdisj
    92. mtyf2
    93. mtyf
    94. mvtss
    95. maxsta
    96. mvtinf
    97. msubff1
    98. msubff1o
    99. mvhf
    100. mvhf1
    101. msubvrs
    102. mclsrcl
    103. mclsssvlem
    104. mclsval
    105. mclsssv
    106. ssmclslem
    107. vhmcls
    108. ssmcls
    109. ss2mcls
    110. mclsax
    111. mclsind
    112. mppspstlem
    113. mppsval
    114. elmpps
    115. mppspst
    116. mthmval
    117. elmthm
    118. mthmi
    119. mthmsta
    120. mppsthm
    121. mthmblem
    122. mthmb
    123. mthmpps
    124. mclsppslem
    125. mclspps
16. Grammatical formal systems
    1. cm0s
    2. cmsa
    3. cmwgfs
    4. cmsy
    5. cmesy
    6. cmgfs
    7. cmtree
    8. cmst
    9. cmsax
    10. cmufs
    11. df-m0s
    12. df-msa
    13. df-mwgfs
    14. df-msyn
    15. df-mesyn
    16. df-mgfs
    17. df-mtree
    18. df-mst
    19. df-msax
    20. df-mufs
17. Models of formal systems
    1. cmuv
    2. cmvl
    3. cmvsb
    4. cmfsh
    5. cmfr
    6. cmevl
    7. cmdl
    8. cusyn
    9. cgmdl
    10. cmitp
    11. cmfitp
    12. df-muv
    13. df-mfsh
    14. df-mevl
    15. df-mvl
    16. df-mvsb
    17. df-mfrel
    18. df-mdl
    19. df-musyn
    20. df-gmdl
    21. df-mitp
    22. df-mfitp
18. Splitting fields
    1. citr
    2. ccpms
    3. chlb
    4. chlim
    5. cpfl
    6. csf1
    7. csf
    8. cpsl
    9. df-irng
    10. df-cplmet
    11. df-homlimb
    12. df-homlim
    13. df-plfl
    14. df-sfl1
    15. df-sfl
    16. df-psl
19. p-adic number fields
    1. czr
    2. cgf
    3. cgfo
    4. ceqp
    5. crqp
    6. cqp
    7. czp
    8. cqpa
    9. ccp
    10. df-zrng
    11. df-gf
    12. df-gfoo
    13. df-eqp
    14. df-rqp
    15. df-qp
    16. df-zp
    17. df-qpa
    18. df-cp