Metamath Proof Explorer

Table of Contents - 21.27. Mathbox for Peter Mazsa

1. Notations
   1. cxrn
   2. cqmap
   3. cadjliftmap
   4. cblockliftmap
   5. csucmap
   6. csuccl
   7. cpre
   8. cblockliftfix
   9. cshiftstable
   10. ccoss
   11. ccoels
   12. crels
   13. cssr
   14. crefs
   15. crefrels
   16. wrefrel
   17. ccnvrefs
   18. ccnvrefrels
   19. wcnvrefrel
   20. csyms
   21. csymrels
   22. wsymrel
   23. ctrs
   24. ctrrels
   25. wtrrel
   26. ceqvrels
   27. weqvrel
   28. ccoeleqvrels
   29. wcoeleqvrel
   30. credunds
   31. wredund
   32. wredundp
   33. cdmqss
   34. wdmqs
   35. cers
   36. werALTV
   37. cpeters
   38. cpet2ers
   39. ccomembers
   40. wcomember
   41. cfunss
   42. cfunsALTV
   43. wfunALTV
   44. cdisjss
   45. cdisjs
   46. wdisjALTV
   47. celdisjs
   48. weldisj
   49. wantisymrel
   50. cparts
   51. wpart
   52. cmembparts
   53. wmembpart
   54. cpetparts
   55. cpet2parts
2. Preparatory theorems
   1. el2v1
   2. el3v1
   3. el3v2
   4. el3v12
   5. el3v13
   6. el3v23
   7. anan
   8. triantru3
   9. biorfd
   10. eqbrtr
   11. eqbrb
   12. eqeltr
   13. eqelb
   14. eqeqan2d
   15. disjresin
   16. disjresdisj
   17. disjresdif
   18. disjresundif
   19. inres2
   20. coideq
   21. nexmo1
   22. eqab2
   23. r2alan
   24. ssrabi
   25. rabimbieq
   26. abeqin
   27. abeqinbi
   28. eqrabi
   29. rabeqel
   30. eqrelf
   31. br1cnvinxp
   32. releleccnv
   33. releccnveq
   34. xpv
   35. vxp
   36. opelvvdif
   37. vvdifopab
   38. brvdif
   39. brvdif2
   40. brvvdif
   41. brvbrvvdif
   42. brcnvep
   43. elecALTV
   44. brcnvepres
   45. brres2
   46. br1cnvres
   47. elec1cnvres
   48. ec1cnvres
   49. eldmres
   50. elrnres
   51. eldmressnALTV
   52. elrnressn
   53. eldm4
   54. eldmres2
   55. eldmres3
   56. eceq1i
   57. ecres
   58. eccnvepres
   59. eleccnvep
   60. eccnvep
   61. extep
   62. disjeccnvep
   63. eccnvepres2
   64. eccnvepres3
   65. eldmqsres
   66. eldmqsres2
   67. qsss1
   68. qseq1i
   69. brinxprnres
   70. inxprnres
   71. dfres4
   72. exan3
   73. exanres
   74. exanres3
   75. exanres2
   76. cnvepres
   77. eqrel2
   78. rncnv
   79. dfdm6
   80. dfrn6
   81. rncnvepres
   82. dmecd
   83. dmec2d
   84. brid
   85. ideq2
   86. idresssidinxp
   87. idreseqidinxp
   88. extid
   89. inxpss
   90. idinxpss
   91. ref5
   92. inxpss3
   93. inxpss2
   94. inxpssidinxp
   95. idinxpssinxp
   96. idinxpssinxp2
   97. idinxpssinxp3
   98. idinxpssinxp4
   99. relcnveq3
   100. relcnveq
   101. relcnveq2
   102. relcnveq4
   103. qsresid
   104. n0elqs
   105. n0elqs2
   106. rnresequniqs
   107. n0el2
   108. cnvepresex
   109. cnvepima
   110. inex3
   111. inxpex
   112. eqres
   113. brrabga
   114. brcnvrabga
   115. opideq
   116. iss2
   117. eldmcnv
   118. dfrel5
   119. dfrel6
   120. cnvresrn
   121. relssinxpdmrn
   122. cnvref4
   123. cnvref5
   124. ecin0
   125. ecinn0
   126. ineleq
   127. inecmo
   128. inecmo2
   129. ineccnvmo
   130. alrmomorn
   131. alrmomodm
   132. ralmo
   133. ralrnmo
   134. dmqsex
   135. raldmqsmo
   136. ralrmo3
   137. raldmqseu
   138. rsp3
   139. rsp3eq
   140. ineccnvmo2
   141. inecmo3
   142. moeu2
   143. mopickr
   144. moantr
   145. brabidgaw
   146. brabidga
   147. inxp2
   148. opabf
   149. ec0
   150. brcnvin
   151. ssdmral
3. Range Cartesian product
   1. df-xrn
   2. xrnss3v
   3. xrnrel
   4. brxrn
   5. brxrn2
   6. dfxrn2
   7. brxrncnvep
   8. dmxrn
   9. dmcnvep
   10. dmxrncnvep
   11. dmcnvepres
   12. dmuncnvepres
   13. dmxrnuncnvepres
   14. ecun
   15. ecunres
   16. ecuncnvepres
   17. xrneq1
   18. xrneq1i
   19. xrneq1d
   20. xrneq2
   21. xrneq2i
   22. xrneq2d
   23. xrneq12
   24. xrneq12i
   25. xrneq12d
   26. elecxrn
   27. ecxrn
   28. relecxrn
   29. ecxrn2
   30. ecxrncnvep
   31. ecxrncnvep2
   32. disjressuc2
   33. disjecxrn
   34. disjecxrncnvep
   35. disjsuc2
   36. xrninxp
   37. xrninxp2
   38. xrninxpex
   39. inxpxrn
   40. br1cnvxrn2
   41. elec1cnvxrn2
   42. rnxrn
   43. rnxrnres
   44. rnxrncnvepres
   45. rnxrnidres
   46. xrnres
   47. xrnres2
   48. xrnres3
   49. xrnres4
   50. xrnresex
   51. xrnidresex
   52. xrncnvepresex
   53. dmxrncnvepres
   54. dmxrncnvepres2
   55. eldmxrncnvepres
   56. eldmxrncnvepres2
   57. eceldmqsxrncnvepres
   58. eceldmqsxrncnvepres2
   59. brin2
   60. brin3
4. Relations
   1. df-rels
   2. elrels2
   3. elrelsrel
   4. elrelsrelim
   5. elrels5
   6. elrels6
5. Quotient map (coset map)
   1. df-qmap
   2. dfqmap2
   3. dfqmap3
   4. ecqmap
   5. ecqmap2
   6. qmapex
   7. relqmap
   8. dmqmap
   9. rnqmap
6. Lifts, shifts, successor, and predecessor
   1. df-adjliftmap
   2. dfadjliftmap
   3. dfadjliftmap2
   4. blockadjliftmap
   5. df-blockliftmap
   6. dfblockliftmap
   7. dfblockliftmap2
   8. df-sucmap
   9. dfsucmap3
   10. dfsucmap2
   11. dfsucmap4
   12. brsucmap
   13. relsucmap
   14. dmsucmap
   15. df-succl
   16. dfsuccl2
   17. mopre
   18. exeupre2
   19. dfsuccl3
   20. dfsuccl4
   21. df-pre
   22. dfpre
   23. dfpre2
   24. dfpre3
   25. dfpred4
   26. dfpre4
   27. df-blockliftfix
   28. df-shiftstable
   29. shiftstableeq2
   30. suceqsneq
   31. sucdifsn2
   32. sucdifsn
   33. ressucdifsn2
   34. ressucdifsn
   35. sucmapsuc
   36. sucmapleftuniq
   37. exeupre
   38. preex
   39. eupre2
   40. eupre
   41. presucmap
   42. preuniqval
   43. sucpre
   44. presuc
   45. press
   46. preel
7. Cosets by ` R `
   1. df-coss
   2. df-coels
   3. dfcoss2
   4. dfcoss3
   5. dfcoss4
   6. cosscnv
   7. coss1cnvres
   8. coss2cnvepres
   9. cossex
   10. cosscnvex
   11. 1cosscnvepresex
   12. 1cossxrncnvepresex
   13. relcoss
   14. relcoels
   15. cossss
   16. cosseq
   17. cosseqi
   18. cosseqd
   19. 1cossres
   20. dfcoels
   21. brcoss
   22. brcoss2
   23. brcoss3
   24. brcosscnvcoss
   25. brcoels
   26. cocossss
   27. cnvcosseq
   28. br2coss
   29. br1cossres
   30. br1cossres2
   31. brressn
   32. ressn2
   33. refressn
   34. antisymressn
   35. trressn
   36. relbrcoss
   37. br1cossinres
   38. br1cossxrnres
   39. br1cossinidres
   40. br1cossincnvepres
   41. br1cossxrnidres
   42. br1cossxrncnvepres
   43. dmcoss3
   44. dmcoss2
   45. rncossdmcoss
   46. dm1cosscnvepres
   47. dmcoels
   48. eldmcoss
   49. eldmcoss2
   50. eldm1cossres
   51. eldm1cossres2
   52. refrelcosslem
   53. refrelcoss3
   54. refrelcoss2
   55. symrelcoss3
   56. symrelcoss2
   57. cossssid
   58. cossssid2
   59. cossssid3
   60. cossssid4
   61. cossssid5
   62. brcosscnv
   63. brcosscnv2
   64. br1cosscnvxrn
   65. 1cosscnvxrn
   66. cosscnvssid3
   67. cosscnvssid4
   68. cosscnvssid5
   69. coss0
   70. cossid
   71. cosscnvid
   72. trcoss
   73. eleccossin
   74. trcoss2
   75. cosselrels
   76. cnvelrels
   77. cosscnvelrels
8. Subset relations
   1. df-ssr
   2. dfssr2
   3. relssr
   4. brssr
   5. brssrid
   6. issetssr
   7. brssrres
   8. br1cnvssrres
   9. brcnvssr
   10. brcnvssrid
   11. br1cossxrncnvssrres
   12. extssr
9. Reflexivity
   1. df-refs
   2. df-refrels
   3. df-refrel
   4. dfrefrels2
   5. dfrefrels3
   6. dfrefrel2
   7. dfrefrel3
   8. dfrefrel5
   9. elrefrels2
   10. elrefrels3
   11. elrefrelsrel
   12. refreleq
   13. refrelid
   14. refrelcoss
   15. refrelressn
10. Converse reflexivity
    1. df-cnvrefs
    2. df-cnvrefrels
    3. df-cnvrefrel
    4. dfcnvrefrels2
    5. dfcnvrefrels3
    6. dfcnvrefrel2
    7. dfcnvrefrel3
    8. dfcnvrefrel4
    9. dfcnvrefrel5
    10. elcnvrefrels2
    11. elcnvrefrels3
    12. elcnvrefrelsrel
    13. cnvrefrelcoss2
    14. cosselcnvrefrels2
    15. cosselcnvrefrels3
    16. cosselcnvrefrels4
    17. cosselcnvrefrels5
11. Symmetry
    1. df-syms
    2. df-symrels
    3. df-symrel
    4. dfsymrels2
    5. dfsymrels3
    6. elrelscnveq3
    7. elrelscnveq
    8. elrelscnveq2
    9. elrelscnveq4
    10. dfsymrels4
    11. dfsymrels5
    12. dfsymrel2
    13. dfsymrel3
    14. dfsymrel4
    15. dfsymrel5
    16. elsymrels2
    17. elsymrels3
    18. elsymrels4
    19. elsymrels5
    20. elsymrelsrel
    21. symreleq
    22. symrelim
    23. symrelcoss
    24. idsymrel
    25. epnsymrel
12. Reflexivity and symmetry
    1. symrefref2
    2. symrefref3
    3. refsymrels2
    4. refsymrels3
    5. refsymrel2
    6. refsymrel3
    7. elrefsymrels2
    8. elrefsymrels3
    9. elrefsymrelsrel
13. Transitivity
    1. df-trs
    2. df-trrels
    3. df-trrel
    4. dftrrels2
    5. dftrrels3
    6. dftrrel2
    7. dftrrel3
    8. eltrrels2
    9. eltrrels3
    10. eltrrelsrel
    11. trreleq
    12. trrelressn
14. Equivalence relations
    1. df-eqvrels
    2. df-eqvrel
    3. df-coeleqvrels
    4. df-coeleqvrel
    5. dfeqvrels2
    6. dfeqvrels3
    7. dfeqvrel2
    8. dfeqvrel3
    9. eleqvrels2
    10. eleqvrels3
    11. eleqvrelsrel
    12. elcoeleqvrels
    13. elcoeleqvrelsrel
    14. eqvrelrel
    15. eqvrelrefrel
    16. eqvrelsymrel
    17. eqvreltrrel
    18. eqvrelim
    19. eqvreleq
    20. eqvreleqi
    21. eqvreleqd
    22. eqvrelsym
    23. eqvrelsymb
    24. eqvreltr
    25. eqvreltrd
    26. eqvreltr4d
    27. eqvrelref
    28. eqvrelth
    29. eqvrelcl
    30. eqvrelthi
    31. eqvreldisj
    32. qsdisjALTV
    33. eqvrelqsel
    34. eqvrelcoss
    35. eqvrelcoss3
    36. eqvrelcoss2
    37. eqvrelcoss4
    38. dfcoeleqvrels
    39. dfcoeleqvrel
15. Redundancy
    1. df-redunds
    2. df-redund
    3. df-redundp
    4. brredunds
    5. brredundsredund
    6. redundss3
    7. redundeq1
    8. redundpim3
    9. redundpbi1
    10. refrelsredund4
    11. refrelsredund2
    12. refrelsredund3
    13. refrelredund4
    14. refrelredund2
    15. refrelredund3
16. Domain quotients
    1. df-dmqss
    2. df-dmqs
    3. dmqseq
    4. dmqseqi
    5. dmqseqd
    6. dmqseqeq1
    7. dmqseqeq1i
    8. dmqseqeq1d
    9. brdmqss
    10. brdmqssqs
    11. n0eldmqs
    12. qseq
    13. n0eldmqseq
    14. n0elim
    15. n0el3
    16. cnvepresdmqss
    17. cnvepresdmqs
    18. unidmqs
    19. unidmqseq
    20. dmqseqim
    21. dmqseqim2
    22. releldmqs
    23. eldmqs1cossres
    24. releldmqscoss
    25. dmqscoelseq
    26. dmqs1cosscnvepreseq
17. Equivalence relations on domain quotients
    1. df-ers
    2. df-erALTV
    3. df-comembers
    4. df-comember
    5. brers
    6. dferALTV2
    7. erALTVeq1
    8. erALTVeq1i
    9. erALTVeq1d
    10. dfcomember
    11. dfcomember2
    12. dfcomember3
    13. eqvreldmqs
    14. eqvreldmqs2
    15. brerser
    16. erimeq2
    17. erimeq
18. Functions
    1. df-funss
    2. df-funsALTV
    3. df-funALTV
    4. dffunsALTV
    5. dffunsALTV2
    6. dffunsALTV3
    7. dffunsALTV4
    8. dffunsALTV5
    9. dffunALTV2
    10. dffunALTV3
    11. dffunALTV4
    12. dffunALTV5
    13. elfunsALTV
    14. elfunsALTV2
    15. elfunsALTV3
    16. elfunsALTV4
    17. elfunsALTV5
    18. elfunsALTVfunALTV
    19. funALTVfun
    20. funALTVss
    21. funALTVeq
    22. funALTVeqi
    23. funALTVeqd
19. Disjoints vs. converse functions
    1. df-disjss
    2. df-disjs
    3. df-disjALTV
    4. df-eldisjs
    5. df-eldisj
    6. dfdisjs
    7. dfdisjs2
    8. dfdisjs3
    9. dfdisjs4
    10. dfdisjs5
    11. dfdisjALTV
    12. dfdisjALTV2
    13. dfdisjALTV3
    14. dfdisjALTV4
    15. dfdisjALTV5
    16. dfdisjALTV5a
    17. disjimeceqim
    18. disjimeceqim2
    19. disjimeceqbi
    20. disjimeceqbi2
    21. disjimrmoeqec
    22. disjimdmqseq
    23. dfeldisj2
    24. dfeldisj3
    25. dfeldisj4
    26. dfeldisj5
    27. dfeldisj5a
    28. eldisjim3
    29. eldisjdmqsim2
    30. eldisjdmqsim
    31. suceldisj
    32. eldisjs
    33. eldisjs2
    34. eldisjs3
    35. eldisjs4
    36. eldisjs5
    37. eldisjsdisj
    38. qmapeldisjs
    39. disjqmap2
    40. disjqmap
    41. eleldisjs
    42. eleldisjseldisj
    43. disjrel
    44. disjss
    45. disjssi
    46. disjssd
    47. disjeq
    48. disjeqi
    49. disjeqd
    50. disjdmqseqeq1
    51. eldisjss
    52. eldisjssi
    53. eldisjssd
    54. eldisjeq
    55. eldisjeqi
    56. eldisjeqd
    57. disjres
    58. eldisjn0elb
    59. disjxrn
    60. disjxrnres5
    61. disjorimxrn
    62. disjimxrn
    63. disjimres
    64. disjimin
    65. disjiminres
    66. disjimxrnres
    67. disjALTV0
    68. disjALTVid
    69. disjALTVidres
    70. disjALTVinidres
    71. disjALTVxrnidres
    72. disjsuc
    73. qmapeldisjsim
    74. qmapeldisjsbi
    75. rnqmapeleldisjsim
20. Antisymmetry
    1. df-antisymrel
    2. dfantisymrel4
    3. dfantisymrel5
    4. antisymrelres
    5. antisymrelressn
21. Partitions: disjoints on domain quotients
    1. df-parts
    2. df-part
    3. df-membparts
    4. df-membpart
    5. dfpart2
    6. dfmembpart2
    7. brparts
    8. brparts2
    9. brpartspart
    10. parteq1
    11. parteq2
    12. parteq12
    13. parteq1i
    14. parteq1d
    15. partsuc2
    16. partsuc
22. Partition-Equivalence Theorems
    1. disjim
    2. disjimi
    3. detlem
    4. eldisjim
    5. eldisjim2
    6. eqvrel0
    7. det0
    8. eqvrelcoss0
    9. eqvrelid
    10. eqvrel1cossidres
    11. eqvrel1cossinidres
    12. eqvrel1cossxrnidres
    13. detid
    14. eqvrelcossid
    15. detidres
    16. detinidres
    17. detxrnidres
    18. disjlem14
    19. disjlem17
    20. disjlem18
    21. disjlem19
    22. disjdmqsss
    23. disjdmqscossss
    24. disjdmqs
    25. disjdmqseq
    26. eldisjn0el
    27. partim2
    28. partim
    29. partimeq
    30. eldisjlem19
    31. membpartlem19
    32. petlem
    33. petlemi
    34. pet02
    35. pet0
    36. petid2
    37. petid
    38. petidres2
    39. petidres
    40. petinidres2
    41. petinidres
    42. petxrnidres2
    43. petxrnidres
    44. eqvreldisj1
    45. eqvreldisj2
    46. eqvreldisj3
    47. eqvreldisj4
    48. eqvreldisj5
    49. eqvrelqseqdisj2
    50. disjimeldisjdmqs
    51. eldisjsim1
    52. eldisjsim2
    53. disjsssrels
    54. eldisjsim3
    55. eldisjsim4
    56. eldisjsim5
    57. eldisjs6
    58. eldisjs7
    59. dfdisjs6
    60. dfdisjs7
    61. fences3
    62. eqvrelqseqdisj3
    63. eqvrelqseqdisj4
    64. eqvrelqseqdisj5
    65. mainer
    66. partimcomember
    67. mpet3
    68. cpet2
    69. cpet
    70. mpet
    71. mpet2
    72. mpets2
    73. mpets
    74. mainpart
    75. fences
    76. fences2
    77. mainer2
    78. mainerim
    79. petincnvepres2
    80. petincnvepres
    81. pet2
    82. pet
    83. pets
    84. dmqsblocks
23. Type-safe Partition-Equivalence: PetParts, PetErs, Pet2Parts, Pet2Ers
    1. df-petparts
    2. df-peters
    3. df-pet2parts
    4. df-pet2ers
    5. dfpetparts2
    6. dfpet2parts2
    7. dfpeters2
    8. typesafepets
    9. petseq
    10. pets2eq