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. ineqcom
   16. ineqcomi
   17. inres2
   18. coideq
   19. nexmo1
   20. 3albii
   21. 3ralbii
   22. ssrabi
   23. rabbieq
   24. rabimbieq
   25. abeqin
   26. abeqinbi
   27. rabeqel
   28. eqrelf
   29. releleccnv
   30. releccnveq
   31. opelvvdif
   32. vvdifopab
   33. brvdif
   34. brvdif2
   35. brvvdif
   36. brvbrvvdif
   37. brcnvep
   38. elecALTV
   39. brcnvepres
   40. brres2
   41. eldmres
   42. eldm4
   43. eldmres2
   44. eceq1i
   45. elecres
   46. ecres
   47. ecres2
   48. eccnvepres
   49. eleccnvep
   50. eccnvep
   51. extep
   52. eccnvepres2
   53. eccnvepres3
   54. eldmqsres
   55. eldmqsres2
   56. qsss1
   57. qseq1i
   58. qseq1d
   59. brinxprnres
   60. inxprnres
   61. dfres4
   62. exan3
   63. exanres
   64. exanres3
   65. exanres2
   66. cnvepres
   67. ssrel3
   68. eqrel2
   69. rncnv
   70. dfdm6
   71. dfrn6
   72. rncnvepres
   73. dmecd
   74. dmec2d
   75. brid
   76. ideq2
   77. idresssidinxp
   78. idreseqidinxp
   79. extid
   80. inxpss
   81. idinxpss
   82. inxpss3
   83. inxpss2
   84. inxpssidinxp
   85. idinxpssinxp
   86. idinxpssinxp2
   87. idinxpssinxp3
   88. idinxpssinxp4
   89. relcnveq3
   90. relcnveq
   91. relcnveq2
   92. relcnveq4
   93. qsresid
   94. n0elqs
   95. n0elqs2
   96. ecex2
   97. uniqsALTV
   98. imaexALTV
   99. ecexALTV
   100. rnresequniqs
   101. n0el2
   102. cnvepresex
   103. eccnvepex
   104. cnvepimaex
   105. cnvepima
   106. inex3
   107. inxpex
   108. eqres
   109. brrabga
   110. brcnvrabga
   111. opideq
   112. iss2
   113. eldmcnv
   114. dfrel5
   115. dfrel6
   116. cnvresrn
   117. ecin0
   118. ecinn0
   119. ineleq
   120. inecmo
   121. inecmo2
   122. ineccnvmo
   123. alrmomorn
   124. alrmomodm
   125. ineccnvmo2
   126. inecmo3
   127. moantr
   128. brabidgaw
   129. brabidga
   130. inxp2
   131. opabf
   132. ec0
   133. 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