Metamath Proof Explorer

Table of Contents - 7.1. Extensible structures

1. Basic definitions
   1. cstr
   2. cnx
   3. csts
   4. cslot
   5. cbs
   6. cress
   7. df-struct
   8. df-ndx
   9. df-slot
   10. sloteq
   11. df-base
   12. df-sets
   13. df-ress
   14. brstruct
   15. isstruct2
   16. structex
   17. structn0fun
   18. isstruct
   19. structcnvcnv
   20. structfung
   21. structfun
   22. structfn
   23. slotfn
   24. strfvnd
   25. basfn
   26. wunndx
   27. strfvn
   28. strfvss
   29. wunstr
   30. ndxarg
   31. ndxid
   32. strndxid
   33. reldmsets
   34. setsvalg
   35. setsval
   36. setsidvald
   37. fvsetsid
   38. fsets
   39. setsdm
   40. setsfun
   41. setsfun0
   42. setsn0fun
   43. setsstruct2
   44. setsexstruct2
   45. setsstruct
   46. wunsets
   47. setsres
   48. setsabs
   49. setscom
   50. strfvd
   51. strfv2d
   52. strfv2
   53. strfv
   54. strfv3
   55. strssd
   56. strss
   57. str0
   58. base0
   59. strfvi
   60. setsid
   61. setsnid
   62. sbcie2s
   63. sbcie3s
   64. baseval
   65. baseid
   66. elbasfv
   67. elbasov
   68. strov2rcl
   69. basendx
   70. basendxnn
   71. basprssdmsets
   72. reldmress
   73. ressval
   74. ressid2
   75. ressval2
   76. ressbas
   77. ressbas2
   78. ressbasss
   79. resslem
   80. ress0
   81. ressid
   82. ressinbas
   83. ressval3d
   84. ressress
   85. ressabs
   86. wunress
2. Slot definitions
   1. cplusg
   2. cmulr
   3. cstv
   4. csca
   5. cvsca
   6. cip
   7. cts
   8. cple
   9. coc
   10. cds
   11. cunif
   12. chom
   13. cco
   14. df-plusg
   15. df-mulr
   16. df-starv
   17. df-sca
   18. df-vsca
   19. df-ip
   20. df-tset
   21. df-ple
   22. df-ocomp
   23. df-ds
   24. df-unif
   25. df-hom
   26. df-cco
   27. strleun
   28. strle1
   29. strle2
   30. strle3
   31. plusgndx
   32. plusgid
   33. opelstrbas
   34. 1strstr
   35. 1strbas
   36. 1strwunbndx
   37. 1strwun
   38. 2strstr
   39. 2strbas
   40. 2strop
   41. 2strstr1
   42. 2strbas1
   43. 2strop1
   44. basendxnplusgndx
   45. grpstr
   46. grpbase
   47. grpplusg
   48. ressplusg
   49. grpbasex
   50. grpplusgx
   51. mulrndx
   52. mulrid
   53. plusgndxnmulrndx
   54. basendxnmulrndx
   55. rngstr
   56. rngbase
   57. rngplusg
   58. rngmulr
   59. starvndx
   60. starvid
   61. ressmulr
   62. ressstarv
   63. srngstr
   64. srngbase
   65. srngplusg
   66. srngmulr
   67. srnginvl
   68. scandx
   69. scaid
   70. vscandx
   71. vscaid
   72. lmodstr
   73. lmodbase
   74. lmodplusg
   75. lmodsca
   76. lmodvsca
   77. ipndx
   78. ipid
   79. ipsstr
   80. ipsbase
   81. ipsaddg
   82. ipsmulr
   83. ipssca
   84. ipsvsca
   85. ipsip
   86. resssca
   87. ressvsca
   88. ressip
   89. phlstr
   90. phlbase
   91. phlplusg
   92. phlsca
   93. phlvsca
   94. phlip
   95. tsetndx
   96. tsetid
   97. topgrpstr
   98. topgrpbas
   99. topgrpplusg
   100. topgrptset
   101. resstset
   102. plendx
   103. pleid
   104. otpsstr
   105. otpsbas
   106. otpstset
   107. otpsle
   108. ressle
   109. ocndx
   110. ocid
   111. dsndx
   112. dsid
   113. unifndx
   114. unifid
   115. odrngstr
   116. odrngbas
   117. odrngplusg
   118. odrngmulr
   119. odrngtset
   120. odrngle
   121. odrngds
   122. ressds
   123. homndx
   124. homid
   125. ccondx
   126. ccoid
   127. resshom
   128. ressco
   129. slotsbhcdif
3. Definition of the structure product
   1. crest
   2. ctopn
   3. df-rest
   4. df-topn
   5. restfn
   6. topnfn
   7. restval
   8. elrest
   9. elrestr
   10. 0rest
   11. restid2
   12. restsspw
   13. firest
   14. restid
   15. topnval
   16. topnid
   17. topnpropd
   18. ctg
   19. cpt
   20. c0g
   21. cgsu
   22. df-0g
   23. df-gsum
   24. df-topgen
   25. df-pt
   26. cprds
   27. cpws
   28. df-prds
   29. reldmprds
   30. df-pws
   31. prdsbasex
   32. imasvalstr
   33. prdsvalstr
   34. prdsvallem
   35. prdsval
   36. prdssca
   37. prdsbas
   38. prdsplusg
   39. prdsmulr
   40. prdsvsca
   41. prdsip
   42. prdsle
   43. prdsless
   44. prdsds
   45. prdsdsfn
   46. prdstset
   47. prdshom
   48. prdsco
   49. prdsbas2
   50. prdsbasmpt
   51. prdsbasfn
   52. prdsbasprj
   53. prdsplusgval
   54. prdsplusgfval
   55. prdsmulrval
   56. prdsmulrfval
   57. prdsleval
   58. prdsdsval
   59. prdsvscaval
   60. prdsvscafval
   61. prdsbas3
   62. prdsbasmpt2
   63. prdsbascl
   64. prdsdsval2
   65. prdsdsval3
   66. pwsval
   67. pwsbas
   68. pwselbasb
   69. pwselbas
   70. pwsplusgval
   71. pwsmulrval
   72. pwsle
   73. pwsleval
   74. pwsvscafval
   75. pwsvscaval
   76. pwssca
   77. pwsdiagel
   78. pwssnf1o
4. Definition of the structure quotient
   1. cordt
   2. cxrs
   3. df-ordt
   4. df-xrs
   5. cqtop
   6. cimas
   7. cqus
   8. cxps
   9. df-qtop
   10. df-imas
   11. df-qus
   12. df-xps
   13. imasval
   14. imasbas
   15. imasds
   16. imasdsfn
   17. imasdsval
   18. imasdsval2
   19. imasplusg
   20. imasmulr
   21. imassca
   22. imasvsca
   23. imasip
   24. imastset
   25. imasle
   26. f1ocpbllem
   27. f1ocpbl
   28. f1ovscpbl
   29. f1olecpbl
   30. imasaddfnlem
   31. imasaddvallem
   32. imasaddflem
   33. imasaddfn
   34. imasaddval
   35. imasaddf
   36. imasmulfn
   37. imasmulval
   38. imasmulf
   39. imasvscafn
   40. imasvscaval
   41. imasvscaf
   42. imasless
   43. imasleval
   44. qusval
   45. quslem
   46. qusin
   47. qusbas
   48. quss
   49. divsfval
   50. ercpbllem
   51. ercpbl
   52. erlecpbl
   53. qusaddvallem
   54. qusaddflem
   55. qusaddval
   56. qusaddf
   57. qusmulval
   58. qusmulf
   59. fnpr2o
   60. fnpr2ob
   61. fvpr0o
   62. fvpr1o
   63. fvprif
   64. xpsfrnel
   65. xpsfeq
   66. xpsfrnel2
   67. xpscf
   68. xpsfval
   69. xpsff1o
   70. xpsfrn
   71. xpsff1o2
   72. xpsval
   73. xpsrnbas
   74. xpsbas
   75. xpsaddlem
   76. xpsadd
   77. xpsmul
   78. xpssca
   79. xpsvsca
   80. xpsless
   81. xpsle