Metamath Proof Explorer

Table of Contents - 20.10. Mathbox for Scott Fenton

1. ZFC Axioms in primitive form
   1. axextprim
   2. axrepprim
   3. axunprim
   4. axpowprim
   5. axregprim
   6. axinfprim
   7. axacprim
2. Untangled classes
   1. untelirr
   2. untuni
   3. untsucf
   4. unt0
   5. untint
   6. efrunt
   7. untangtr
3. Extra propositional calculus theorems
   1. 3pm3.2ni
   2. 3jaodd
   3. 3orit
   4. biimpexp
   5. 3orel13
   6. onelssex
4. Misc. Useful Theorems
   1. nepss
   2. 3ccased
   3. dfso3
   4. brtpid1
   5. brtpid2
   6. brtpid3
   7. ceqsrexv2
   8. iota5f
   9. ceqsralv2
   10. dford5
   11. jath
   12. riotarab
   13. reurab
   14. snres0
   15. fnssintima
   16. xpab
   17. ralxpes
   18. ot2elxp
   19. ot21std
   20. ot22ndd
   21. otthne
   22. elxpxp
   23. elxpxpss
   24. ralxp3f
   25. ralxp3
   26. sbcoteq1a
   27. ralxp3es
   28. onunel
   29. imaeqsexv
   30. imaeqsalv
   31. nnuni
5. Properties of real and complex numbers
   1. sqdivzi
   2. supfz
   3. inffz
   4. fz0n
   5. shftvalg
   6. divcnvlin
   7. climlec3
   8. logi
   9. iexpire
   10. bcneg1
   11. bcm1nt
   12. bcprod
   13. bccolsum
6. Infinite products
   1. iprodefisumlem
   2. iprodefisum
   3. iprodgam
7. Factorial limits
   1. faclimlem1
   2. faclimlem2
   3. faclimlem3
   4. faclim
   5. iprodfac
   6. faclim2
8. Greatest common divisor and divisibility
   1. gcd32
   2. gcdabsorb
9. Properties of relationships
   1. brtp
   2. dftr6
   3. coep
   4. coepr
   5. dffr5
   6. dfso2
   7. br8
   8. br6
   9. br4
   10. cnvco1
   11. cnvco2
   12. eldm3
   13. elrn3
   14. pocnv
   15. socnv
   16. sotrd
   17. sotr3
   18. sotrine
   19. eqfunresadj
   20. eqfunressuc
   21. funeldmb
   22. elintfv
10. Properties of functions and mappings
    1. funpsstri
    2. fundmpss
    3. fvresval
    4. funsseq
    5. fununiq
    6. funbreq
    7. br1steq
    8. br2ndeq
    9. dfdm5
    10. dfrn5
    11. opelco3
    12. elima4
    13. fv1stcnv
    14. fv2ndcnv
    15. imaindm
11. Set induction (or epsilon induction)
    1. setinds
    2. setinds2f
    3. setinds2
12. Ordinal numbers
    1. elpotr
    2. dford5reg
    3. dfon2lem1
    4. dfon2lem2
    5. dfon2lem3
    6. dfon2lem4
    7. dfon2lem5
    8. dfon2lem6
    9. dfon2lem7
    10. dfon2lem8
    11. dfon2lem9
    12. dfon2
    13. rdgprc0
    14. rdgprc
    15. dfrdg2
    16. dfrdg3
13. Defined equality axioms
    1. axextdfeq
    2. ax8dfeq
    3. axextdist
    4. axextbdist
    5. 19.12b
    6. exnel
    7. distel
    8. axextndbi
14. Hypothesis builders
    1. hbntg
    2. hbimtg
    3. hbaltg
    4. hbng
    5. hbimg
15. (Trans)finite Recursion Theorems
    1. tfisg
16. Well-Founded Induction
    1. frpoins3xpg
    2. frpoins3xp3g
17. Ordering Cross Products, Part 2
    1. xpord2lem
    2. poxp2
    3. frxp2
    4. xpord2pred
    5. sexp2
    6. xpord2ind
    7. xpord3lem
    8. poxp3
    9. frxp3
    10. xpord3pred
    11. sexp3
    12. xpord3ind
18. Ordering Ordinal Sequences
    1. orderseqlem
    2. poseq
    3. soseq
19. Well-founded zero, successor, and limits
    1. cwsuc
    2. cwlim
    3. df-wsuc
    4. df-wlim
    5. wsuceq123
    6. wsuceq1
    7. wsuceq2
    8. wsuceq3
    9. nfwsuc
    10. wlimeq12
    11. wlimeq1
    12. wlimeq2
    13. nfwlim
    14. elwlim
    15. wzel
    16. wsuclem
    17. wsucex
    18. wsuccl
    19. wsuclb
    20. wlimss
20. Natural operations on ordinals
    1. cnadd
    2. df-nadd
    3. on2recsfn
    4. on2recsov
    5. on2ind
    6. on3ind
    7. naddfn
    8. naddcllem
    9. naddcl
    10. naddov
    11. naddov2
    12. naddcom
    13. naddid1
    14. naddssim
    15. naddelim
    16. naddel1
    17. naddel2
    18. naddss1
    19. naddss2
21. Surreal Numbers
    1. csur
    2. cslt
    3. cbday
    4. df-no
    5. df-slt
    6. df-bday
    7. elno
    8. sltval
    9. bdayval
    10. nofun
    11. nodmon
    12. norn
    13. nofnbday
    14. nodmord
    15. elno2
    16. elno3
    17. sltval2
    18. nofv
    19. nosgnn0
    20. nosgnn0i
    21. noreson
    22. sltintdifex
    23. sltres
    24. noxp1o
    25. noseponlem
    26. nosepon
    27. noextend
    28. noextendseq
    29. noextenddif
    30. noextendlt
    31. noextendgt
    32. nolesgn2o
    33. nolesgn2ores
    34. nogesgn1o
    35. nogesgn1ores
22. Surreal Numbers: Ordering
    1. sltsolem1
    2. sltso
23. Surreal Numbers: Birthday Function
    1. bdayfo
24. Surreal Numbers: Density
    1. fvnobday
    2. nosepnelem
    3. nosepne
    4. nosep1o
    5. nosep2o
    6. nosepdmlem
    7. nosepdm
    8. nosepeq
    9. nosepssdm
    10. nodenselem4
    11. nodenselem5
    12. nodenselem6
    13. nodenselem7
    14. nodenselem8
    15. nodense
25. Surreal Numbers: Full-Eta Property
    1. bdayimaon
    2. nolt02olem
    3. nolt02o
    4. nogt01o
    5. noresle
    6. nomaxmo
    7. nominmo
    8. nosupprefixmo
    9. noinfprefixmo
    10. nosupcbv
    11. nosupno
    12. nosupdm
    13. nosupbday
    14. nosupfv
    15. nosupres
    16. nosupbnd1lem1
    17. nosupbnd1lem2
    18. nosupbnd1lem3
    19. nosupbnd1lem4
    20. nosupbnd1lem5
    21. nosupbnd1lem6
    22. nosupbnd1
    23. nosupbnd2lem1
    24. nosupbnd2
    25. noinfcbv
    26. noinfno
    27. noinfdm
    28. noinfbday
    29. noinffv
    30. noinfres
    31. noinfbnd1lem1
    32. noinfbnd1lem2
    33. noinfbnd1lem3
    34. noinfbnd1lem4
    35. noinfbnd1lem5
    36. noinfbnd1lem6
    37. noinfbnd1
    38. noinfbnd2lem1
    39. noinfbnd2
    40. nosupinfsep
    41. noetasuplem1
    42. noetasuplem2
    43. noetasuplem3
    44. noetasuplem4
    45. noetainflem1
    46. noetainflem2
    47. noetainflem3
    48. noetainflem4
    49. noetalem1
    50. noetalem2
    51. noeta
26. Surreal numbers - ordering theorems
    1. csle
    2. df-sle
    3. sltirr
    4. slttr
    5. sltasym
    6. sltlin
    7. slttrieq2
    8. slttrine
    9. slenlt
    10. sltnle
    11. sleloe
    12. sletri3
    13. sltletr
    14. slelttr
    15. sletr
    16. slttrd
    17. sltletrd
    18. slelttrd
    19. sletrd
    20. slerflex
27. Surreal numbers - birthday theorems
    1. bdayfun
    2. bdayfn
    3. bdaydm
    4. bdayrn
    5. bdayelon
    6. nocvxminlem
    7. nocvxmin
    8. noprc
28. Surreal numbers: Conway cuts
    1. csslt
    2. df-sslt
    3. cscut
    4. df-scut
    5. noeta2
    6. brsslt
    7. ssltex1
    8. ssltex2
    9. ssltss1
    10. ssltss2
    11. ssltsep
    12. ssltd
    13. ssltsepc
    14. ssltsepcd
    15. sssslt1
    16. sssslt2
    17. nulsslt
    18. nulssgt
    19. conway
    20. scutval
    21. scutcut
    22. scutcl
    23. scutcld
    24. scutbday
    25. eqscut
    26. eqscut2
    27. sslttr
    28. ssltun1
    29. ssltun2
    30. scutun12
    31. dmscut
    32. scutf
    33. etasslt
    34. etasslt2
    35. scutbdaybnd
    36. scutbdaybnd2
    37. scutbdaybnd2lim
    38. scutbdaylt
    39. slerec
    40. sltrec
    41. ssltdisj
29. Surreal numbers - zero and one
    1. c0s
    2. c1s
    3. df-0s
    4. df-1s
    5. 0sno
    6. 1sno
    7. bday0s
    8. 0slt1s
    9. bday0b
    10. bday1s
30. Surreal numbers - cuts and options
    1. cmade
    2. cold
    3. cnew
    4. cleft
    5. cright
    6. df-made
    7. df-old
    8. df-new
    9. df-left
    10. df-right
    11. madeval
    12. madeval2
    13. oldval
    14. newval
    15. madef
    16. oldf
    17. newf
    18. old0
    19. madessno
    20. oldssno
    21. newssno
    22. leftval
    23. rightval
    24. leftf
    25. rightf
    26. elmade
    27. elmade2
    28. elold
    29. ssltleft
    30. ssltright
    31. lltropt
    32. made0
    33. new0
    34. madess
    35. oldssmade
    36. leftssold
    37. rightssold
    38. leftssno
    39. rightssno
    40. madecut
    41. madeun
    42. madeoldsuc
    43. oldsuc
    44. oldlim
    45. madebdayim
    46. oldbdayim
    47. oldirr
    48. leftirr
    49. rightirr
    50. left0s
    51. right0s
    52. lrold
    53. madebdaylemold
    54. madebdaylemlrcut
    55. madebday
    56. oldbday
    57. newbday
    58. lrcut
    59. scutfo
    60. sltn0
    61. lruneq
    62. sltlpss
31. Surreal numbers: Cofinality and coinitiality
    1. cofsslt
    2. coinitsslt
    3. cofcut1
    4. cofcut2
    5. cofcutr
    6. cofcutrtime
32. Surreal numbers: Induction and recursion on one variable
    1. cnorec
    2. df-norec
    3. lrrecval
    4. lrrecval2
    5. lrrecpo
    6. lrrecse
    7. lrrecfr
    8. lrrecpred
    9. noinds
    10. norecfn
    11. norecov
33. Surreal numbers: Induction and recursion on two variables
    1. cnorec2
    2. df-norec2
    3. noxpordpo
    4. noxpordfr
    5. noxpordse
    6. noxpordpred
    7. no2indslem
    8. no2inds
    9. norec2fn
    10. norec2ov
    11. no3inds
34. Surreal numbers - addition, negation, and subtraction
    1. cadds
    2. cnegs
    3. csubs
    4. df-adds
    5. df-negs
    6. df-subs
    7. negsfn
    8. negsval
    9. negs0s
    10. addsfn
    11. addsval
    12. addsid1
    13. addsid1d
    14. addscom
    15. addscomd
    16. addscllem1
35. Quantifier-free definitions
    1. ctxp
    2. cpprod
    3. csset
    4. ctrans
    5. cbigcup
    6. cfix
    7. climits
    8. cfuns
    9. csingle
    10. csingles
    11. cimage
    12. ccart
    13. cimg
    14. cdomain
    15. crange
    16. capply
    17. ccup
    18. ccap
    19. csuccf
    20. cfunpart
    21. cfullfn
    22. crestrict
    23. cub
    24. clb
    25. df-txp
    26. df-pprod
    27. df-sset
    28. df-trans
    29. df-bigcup
    30. df-fix
    31. df-limits
    32. df-funs
    33. df-singleton
    34. df-singles
    35. df-image
    36. df-cart
    37. df-img
    38. df-domain
    39. df-range
    40. df-cup
    41. df-cap
    42. df-restrict
    43. df-succf
    44. df-apply
    45. df-funpart
    46. df-fullfun
    47. df-ub
    48. df-lb
    49. txpss3v
    50. txprel
    51. brtxp
    52. brtxp2
    53. dfpprod2
    54. pprodcnveq
    55. pprodss4v
    56. brpprod
    57. brpprod3a
    58. brpprod3b
    59. relsset
    60. brsset
    61. idsset
    62. eltrans
    63. dfon3
    64. dfon4
    65. brtxpsd
    66. brtxpsd2
    67. brtxpsd3
    68. relbigcup
    69. brbigcup
    70. dfbigcup2
    71. fobigcup
    72. fnbigcup
    73. fvbigcup
    74. elfix
    75. elfix2
    76. dffix2
    77. fixssdm
    78. fixssrn
    79. fixcnv
    80. fixun
    81. ellimits
    82. limitssson
    83. dfom5b
    84. sscoid
    85. dffun10
    86. elfuns
    87. elfunsg
    88. brsingle
    89. elsingles
    90. fnsingle
    91. fvsingle
    92. dfsingles2
    93. snelsingles
    94. dfiota3
    95. dffv5
    96. unisnif
    97. brimage
    98. brimageg
    99. funimage
    100. fnimage
    101. imageval
    102. fvimage
    103. brcart
    104. brdomain
    105. brrange
    106. brdomaing
    107. brrangeg
    108. brimg
    109. brapply
    110. brcup
    111. brcap
    112. brsuccf
    113. funpartlem
    114. funpartfun
    115. funpartss
    116. funpartfv
    117. fullfunfnv
    118. fullfunfv
    119. brfullfun
    120. brrestrict
    121. dfrecs2
    122. dfrdg4
    123. dfint3
    124. imagesset
    125. brub
    126. brlb
36. Alternate ordered pairs
    1. caltop
    2. caltxp
    3. df-altop
    4. df-altxp
    5. altopex
    6. altopthsn
    7. altopeq12
    8. altopeq1
    9. altopeq2
    10. altopth1
    11. altopth2
    12. altopthg
    13. altopthbg
    14. altopth
    15. altopthb
    16. altopthc
    17. altopthd
    18. altxpeq1
    19. altxpeq2
    20. elaltxp
    21. altopelaltxp
    22. altxpsspw
    23. altxpexg
    24. rankaltopb
    25. nfaltop
    26. sbcaltop
37. Geometry in the Euclidean space
    1. Congruence properties
    2. Betweenness properties
    3. Segment Transportation
    4. Properties relating betweenness and congruence
    5. Connectivity of betweenness
    6. Segment less than or equal to
    7. Outside-of relationship
    8. Lines and Rays
38. Forward difference
    1. cfwddif
    2. df-fwddif
    3. cfwddifn
    4. df-fwddifn
    5. fwddifval
    6. fwddifnval
    7. fwddifn0
    8. fwddifnp1
39. Rank theorems
    1. rankung
    2. ranksng
    3. rankelg
    4. rankpwg
    5. rank0
    6. rankeq1o
40. Hereditarily Finite Sets
    1. chf
    2. df-hf
    3. elhf
    4. elhf2
    5. elhf2g
    6. 0hf
    7. hfun
    8. hfsn
    9. hfadj
    10. hfelhf
    11. hftr
    12. hfext
    13. hfuni
    14. hfpw
    15. hfninf