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
  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. sspreima
    24. opfv
    25. xppreima
    26. xppreima2
    27. elunirn2
    28. abfmpunirn
    29. rabfmpunirn
    30. abfmpeld
    31. abfmpel
    32. fmptdF
    33. fmptcof2
    34. fcomptf
    35. acunirnmpt
    36. acunirnmpt2
    37. acunirnmpt2f
    38. aciunf1lem
    39. aciunf1
    40. ofoprabco
    41. ofpreima
    42. ofpreima2
    43. funcnvmpt
    44. funcnv5mpt
    45. funcnv4mpt
    46. preimane
    47. fnpreimac
    48. fgreu
    49. fcnvgreu
    50. rnmposs
    51. mptssALT
    52. partfun
    53. dfcnv2
    54. fnimatp
    55. fnunres2
  3. Operations - misc additions
    1. mpomptxf
    2. suppovss
    3. fvdifsupp
    4. fmptssfisupp
  4. Explicit Functions with one or two points as a domain
    1. brsnop
    2. cosnopne
    3. cosnop
    4. cnvprop
    5. brprop
    6. mptprop
    7. 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
  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