Metamath Proof Explorer

Table of Contents - 20.23. Mathbox for Peter Mazsa

1. Notations
   1. cxrn
   2. ccoss
   3. ccoels
   4. crels
   5. cssr
   6. crefs
   7. crefrels
   8. wrefrel
   9. ccnvrefs
   10. ccnvrefrels
   11. wcnvrefrel
   12. csyms
   13. csymrels
   14. wsymrel
   15. ctrs
   16. ctrrels
   17. wtrrel
   18. ceqvrels
   19. weqvrel
   20. ccoeleqvrels
   21. wcoeleqvrel
   22. credunds
   23. wredund
   24. wredundp
   25. cdmqss
   26. wdmqs
   27. cers
   28. werALTV
   29. cmembers
   30. wmember
   31. cfunss
   32. cfunsALTV
   33. wfunALTV
   34. cdisjss
   35. cdisjs
   36. wdisjALTV
   37. celdisjs
   38. weldisj
2. Preparatory theorems
   1. el2v1
   2. el3v
   3. el3v1
   4. el3v2
   5. el3v3
   6. el3v12
   7. el3v13
   8. el3v23
   9. an2anr
   10. anan
   11. triantru3
   12. eqeltr
   13. eqelb
   14. eqeqan2d
   15. inres2
   16. coideq
   17. nexmo1
   18. 3albii
   19. 3ralbii
   20. ssrabi
   21. rabbieq
   22. rabimbieq
   23. abeqin
   24. abeqinbi
   25. rabeqel
   26. eqrelf
   27. releleccnv
   28. releccnveq
   29. opelvvdif
   30. vvdifopab
   31. brvdif
   32. brvdif2
   33. brvvdif
   34. brvbrvvdif
   35. brcnvep
   36. elecALTV
   37. brcnvepres
   38. brres2
   39. eldmres
   40. eldm4
   41. eldmres2
   42. eceq1i
   43. elecres
   44. ecres
   45. ecres2
   46. eccnvepres
   47. eleccnvep
   48. eccnvep
   49. extep
   50. eccnvepres2
   51. eccnvepres3
   52. eldmqsres
   53. eldmqsres2
   54. qsss1
   55. qseq1i
   56. qseq1d
   57. brinxprnres
   58. inxprnres
   59. dfres4
   60. exan3
   61. exanres
   62. exanres3
   63. exanres2
   64. cnvepres
   65. ssrel3
   66. eqrel2
   67. rncnv
   68. dfdm6
   69. dfrn6
   70. rncnvepres
   71. dmecd
   72. dmec2d
   73. brid
   74. ideq2
   75. idresssidinxp
   76. idreseqidinxp
   77. extid
   78. inxpss
   79. idinxpss
   80. inxpss3
   81. inxpss2
   82. inxpssidinxp
   83. idinxpssinxp
   84. idinxpssinxp2
   85. idinxpssinxp3
   86. idinxpssinxp4
   87. relcnveq3
   88. relcnveq
   89. relcnveq2
   90. relcnveq4
   91. qsresid
   92. n0elqs
   93. n0elqs2
   94. ecex2
   95. uniqsALTV
   96. imaexALTV
   97. ecexALTV
   98. rnresequniqs
   99. n0el2
   100. cnvepresex
   101. eccnvepex
   102. cnvepimaex
   103. cnvepima
   104. inex3
   105. inxpex
   106. eqres
   107. brrabga
   108. brcnvrabga
   109. opideq
   110. iss2
   111. eldmcnv
   112. dfrel5
   113. dfrel6
   114. cnvresrn
   115. ecin0
   116. ecinn0
   117. ineleq
   118. inecmo
   119. inecmo2
   120. ineccnvmo
   121. alrmomorn
   122. alrmomodm
   123. ineccnvmo2
   124. inecmo3
   125. moantr
   126. brabidgaw
   127. brabidga
   128. inxp2
   129. opabf
   130. ec0
   131. 0qs
3. Range Cartesian product
   1. df-xrn
   2. xrnss3v
   3. xrnrel
   4. brxrn
   5. brxrn2
   6. dfxrn2
   7. xrneq1
   8. xrneq1i
   9. xrneq1d
   10. xrneq2
   11. xrneq2i
   12. xrneq2d
   13. xrneq12
   14. xrneq12i
   15. xrneq12d
   16. elecxrn
   17. ecxrn
   18. xrninxp
   19. xrninxp2
   20. xrninxpex
   21. inxpxrn
   22. br1cnvxrn2
   23. elec1cnvxrn2
   24. rnxrn
   25. rnxrnres
   26. rnxrncnvepres
   27. rnxrnidres
   28. xrnres
   29. xrnres2
   30. xrnres3
   31. xrnres4
   32. xrnresex
   33. xrnidresex
   34. xrncnvepresex
   35. brin2
   36. brin3
4. Cosets by ` R `
   1. df-coss
   2. df-coels
   3. dfcoss2
   4. dfcoss3
   5. dfcoss4
   6. cossex
   7. cosscnvex
   8. 1cosscnvepresex
   9. 1cossxrncnvepresex
   10. relcoss
   11. relcoels
   12. cossss
   13. cosseq
   14. cosseqi
   15. cosseqd
   16. 1cossres
   17. dfcoels
   18. brcoss
   19. brcoss2
   20. brcoss3
   21. brcosscnvcoss
   22. brcoels
   23. cocossss
   24. cnvcosseq
   25. br2coss
   26. br1cossres
   27. br1cossres2
   28. relbrcoss
   29. br1cossinres
   30. br1cossxrnres
   31. br1cossinidres
   32. br1cossincnvepres
   33. br1cossxrnidres
   34. br1cossxrncnvepres
   35. dmcoss3
   36. dmcoss2
   37. rncossdmcoss
   38. dm1cosscnvepres
   39. dmcoels
   40. eldmcoss
   41. eldmcoss2
   42. eldm1cossres
   43. eldm1cossres2
   44. refrelcosslem
   45. refrelcoss3
   46. refrelcoss2
   47. symrelcoss3
   48. symrelcoss2
   49. cossssid
   50. cossssid2
   51. cossssid3
   52. cossssid4
   53. cossssid5
   54. brcosscnv
   55. brcosscnv2
   56. br1cosscnvxrn
   57. 1cosscnvxrn
   58. cosscnvssid3
   59. cosscnvssid4
   60. cosscnvssid5
   61. coss0
   62. cossid
   63. cosscnvid
   64. trcoss
   65. eleccossin
   66. trcoss2
5. Relations
   1. df-rels
   2. elrels2
   3. elrelsrel
   4. elrelsrelim
   5. elrels5
   6. elrels6
   7. elrelscnveq3
   8. elrelscnveq
   9. elrelscnveq2
   10. elrelscnveq4
   11. cnvelrels
   12. cosselrels
   13. cosscnvelrels
6. 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
7. Reflexivity
   1. df-refs
   2. df-refrels
   3. df-refrel
   4. dfrefrels2
   5. dfrefrels3
   6. dfrefrel2
   7. dfrefrel3
   8. elrefrels2
   9. elrefrels3
   10. elrefrelsrel
   11. refreleq
   12. refrelid
   13. refrelcoss
8. Converse reflexivity
   1. df-cnvrefs
   2. df-cnvrefrels
   3. df-cnvrefrel
   4. dfcnvrefrels2
   5. dfcnvrefrels3
   6. dfcnvrefrel2
   7. dfcnvrefrel3
   8. elcnvrefrels2
   9. elcnvrefrels3
   10. elcnvrefrelsrel
   11. cnvrefrelcoss2
   12. cosselcnvrefrels2
   13. cosselcnvrefrels3
   14. cosselcnvrefrels4
   15. cosselcnvrefrels5
9. Symmetry
   1. df-syms
   2. df-symrels
   3. df-symrel
   4. dfsymrels2
   5. dfsymrels3
   6. dfsymrels4
   7. dfsymrels5
   8. dfsymrel2
   9. dfsymrel3
   10. dfsymrel4
   11. dfsymrel5
   12. elsymrels2
   13. elsymrels3
   14. elsymrels4
   15. elsymrels5
   16. elsymrelsrel
   17. symreleq
   18. symrelim
   19. symrelcoss
   20. idsymrel
   21. epnsymrel
10. Reflexivity and symmetry
    1. symrefref2
    2. symrefref3
    3. refsymrels2
    4. refsymrels3
    5. refsymrel2
    6. refsymrel3
    7. elrefsymrels2
    8. elrefsymrels3
    9. elrefsymrelsrel
11. 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. 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
13. 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
14. 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. n0eldmqseq
    13. n0el3
    14. cnvepresdmqss
    15. cnvepresdmqs
    16. unidmqs
    17. unidmqseq
    18. dmqseqim
    19. dmqseqim2
    20. releldmqs
    21. eldmqs1cossres
    22. releldmqscoss
    23. dmqscoelseq
    24. dmqs1cosscnvepreseq
15. Equivalence relations on domain quotients
    1. df-ers
    2. df-erALTV
    3. df-members
    4. df-member
    5. brers
    6. dferALTV2
    7. erALTVeq1
    8. erALTVeq1i
    9. erALTVeq1d
    10. dfmember
    11. dfmember2
    12. dfmember3
    13. eqvreldmqs
    14. brerser
    15. erim2
    16. erim
16. 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
17. 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. dfeldisj2
    17. dfeldisj3
    18. dfeldisj4
    19. dfeldisj5
    20. eldisjs
    21. eldisjs2
    22. eldisjs3
    23. eldisjs4
    24. eldisjs5
    25. eldisjsdisj
    26. eleldisjs
    27. eleldisjseldisj
    28. disjrel
    29. disjss
    30. disjssi
    31. disjssd
    32. disjeq
    33. disjeqi
    34. disjeqd
    35. disjdmqseqeq1
    36. eldisjss
    37. eldisjssi
    38. eldisjssd
    39. eldisjeq
    40. eldisjeqi
    41. eldisjeqd
    42. disjxrn
    43. disjorimxrn
    44. disjimxrn
    45. disjimres
    46. disjimin
    47. disjiminres
    48. disjimxrnres
    49. disjALTV0
    50. disjALTVid
    51. disjALTVidres
    52. disjALTVinidres
    53. disjALTVxrnidres