Metamath Proof Explorer

Table of Contents - 20.3.4. Relations and Functions

1. Relations - misc additions
   1. xpdisjres
   2. opeldifid
   3. difres
   4. imadifxp
   5. relfi
   6. reldisjun
   7. 0res
   8. funresdm1
   9. fnunres1
   10. fcoinver
   11. fcoinvbr
   12. brabgaf
   13. brelg
   14. br8d
   15. opabdm
   16. opabrn
   17. opabssi
   18. opabid2ss
   19. ssrelf
   20. eqrelrd2
   21. erbr3b
   22. iunsnima
   23. iunsnima2
2. Functions - misc additions
   1. ac6sf2
   2. fnresin
   3. f1o3d
   4. eldmne0
   5. f1rnen
   6. rinvf1o
   7. fresf1o
   8. nfpconfp
   9. fmptco1f1o
   10. cofmpt2
   11. f1mptrn
   12. dfimafnf
   13. funimass4f
   14. elimampt
   15. suppss2f
   16. fovcld
   17. ofrn
   18. ofrn2
   19. off2
   20. ofresid
   21. fimarab
   22. unipreima
   23. opfv
   24. xppreima
   25. 2ndimaxp
   26. djussxp2
   27. 2ndresdju
   28. 2ndresdjuf1o
   29. xppreima2
   30. abfmpunirn
   31. rabfmpunirn
   32. abfmpeld
   33. abfmpel
   34. fmptdF
   35. fmptcof2
   36. fcomptf
   37. acunirnmpt
   38. acunirnmpt2
   39. acunirnmpt2f
   40. aciunf1lem
   41. aciunf1
   42. ofoprabco
   43. ofpreima
   44. ofpreima2
   45. funcnvmpt
   46. funcnv5mpt
   47. funcnv4mpt
   48. preimane
   49. fnpreimac
   50. fgreu
   51. fcnvgreu
   52. rnmposs
   53. mptssALT
   54. dfcnv2
   55. fnimatp
   56. fnunres2
3. Operations - misc additions
   1. mpomptxf
   2. suppovss
   3. fvdifsupp
   4. fmptssfisupp
   5. suppiniseg
   6. fsuppinisegfi
   7. fressupp
   8. fdifsuppconst
   9. ressupprn
   10. supppreima
   11. fsupprnfi
4. Explicit Functions with one or two points as a domain
   1. cosnopne
   2. cosnop
   3. cnvprop
   4. brprop
   5. mptprop
   6. coprprop
5. Isomorphisms - misc. add.
   1. gtiso
   2. isoun
6. Disjointness (additional proof requiring functions)
   1. disjdsct
7. First and second members of an ordered pair - misc additions
   1. df1stres
   2. df2ndres
   3. 1stpreimas
   4. 1stpreima
   5. 2ndpreima
   6. curry2ima
   7. preiman0
   8. intimafv
8. Supremum - misc additions
   1. supssd
   2. infssd
9. Finite Sets
   1. imafi2
   2. unifi3
10. Countable Sets
    1. snct
    2. prct
    3. mpocti
    4. abrexct
    5. mptctf
    6. abrexctf
    7. padct
    8. cnvoprabOLD
    9. f1od2
    10. fcobij
    11. fcobijfs
    12. suppss3
    13. fsuppcurry1
    14. fsuppcurry2
    15. offinsupp1
    16. ffs2
    17. ffsrn
    18. resf1o
    19. maprnin
    20. fpwrelmapffslem
    21. fpwrelmap
    22. fpwrelmapffs