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. 3orel2
   2. 3orel3
   3. 3pm3.2ni
   4. 3jaodd
   5. 3orit
   6. biimpexp
   7. 3orel13
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
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. pdivsq
   2. dvdspw
   3. gcd32
   4. gcdabsorb
9. Properties of relationships
   1. brtp
   2. dftr6
   3. coep
   4. coepr
   5. dffr5
   6. dfso2
   7. dfpo2
   8. br8
   9. br6
   10. br4
   11. cnvco1
   12. cnvco2
   13. eldm3
   14. elrn3
   15. pocnv
   16. socnv
   17. sotrd
   18. sotr3
   19. sotrine
   20. eqfunresadj
   21. eqfunressuc
   22. funeldmb
   23. 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. Transitive closure under a relationship
    1. ctrpred
    2. df-trpred
    3. dftrpred2
    4. trpredeq1
    5. trpredeq2
    6. trpredeq3
    7. trpredeq1d
    8. trpredeq2d
    9. trpredeq3d
    10. eltrpred
    11. trpredlem1
    12. trpredpred
    13. trpredss
    14. trpredtr
    15. trpredmintr
    16. trpredelss
    17. dftrpred3g
    18. dftrpred4g
    19. trpredpo
    20. trpred0
    21. trpredex
    22. trpredrec
17. Founded Induction
    1. frpomin
    2. frpomin2
    3. frpoind
    4. frpoinsg
    5. frpoins2fg
    6. frpoins2g
    7. frmin
    8. frind
    9. frindi
    10. frinsg
    11. frins
    12. frins2fg
    13. frins2f
    14. frins2g
    15. frins2
    16. frins3
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. Founded Partial Recursion
    1. cfrecs
    2. df-frecs
    3. frecseq123
    4. nffrecs
    5. frr3g
    6. fpr3g
    7. frrlem1
    8. frrlem2
    9. frrlem3
    10. frrlem4
    11. frrlem5
    12. frrlem6
    13. frrlem7
    14. frrlem8
    15. frrlem9
    16. frrlem10
    17. frrlem11
    18. frrlem12
    19. frrlem13
    20. frrlem14
    21. fprlem1
    22. fprlem2
    23. fpr1
    24. fpr2
    25. fpr3
    26. frrlem15
    27. frrlem16
    28. frr1
    29. frr2
    30. frr3
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
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. nosepdmlem
    6. nosepdm
    7. nosepeq
    8. nosepssdm
    9. nodenselem4
    10. nodenselem5
    11. nodenselem6
    12. nodenselem7
    13. nodenselem8
    14. nodense
25. Surreal Numbers: Full-Eta Property
    1. bdayimaon
    2. nolt02olem
    3. nolt02o
    4. noresle
    5. nomaxmo
    6. noprefixmo
    7. nosupno
    8. nosupdm
    9. nosupbday
    10. nosupfv
    11. nosupres
    12. nosupbnd1lem1
    13. nosupbnd1lem2
    14. nosupbnd1lem3
    15. nosupbnd1lem4
    16. nosupbnd1lem5
    17. nosupbnd1lem6
    18. nosupbnd1
    19. nosupbnd2lem1
    20. nosupbnd2
    21. noetalem1
    22. noetalem2
    23. noetalem3
    24. noetalem4
    25. noetalem5
    26. 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
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. brsslt
    6. ssltex1
    7. ssltex2
    8. ssltss1
    9. ssltss2
    10. ssltsep
    11. sssslt1
    12. sssslt2
    13. nulsslt
    14. nulssgt
    15. conway
    16. scutval
    17. scutcut
    18. scutbday
    19. sslttr
    20. ssltun1
    21. ssltun2
    22. scutun12
    23. dmscut
    24. scutf
    25. etasslt
    26. scutbdaybnd
    27. scutbdaylt
    28. slerec
    29. sltrec
29. 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
30. 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
31. 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
32. 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
33. Forward difference
    1. cfwddif
    2. df-fwddif
    3. cfwddifn
    4. df-fwddifn
    5. fwddifval
    6. fwddifnval
    7. fwddifn0
    8. fwddifnp1
34. Rank theorems
    1. rankung
    2. ranksng
    3. rankelg
    4. rankpwg
    5. rank0
    6. rankeq1o
35. 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