Metamath Proof Explorer


Table of Contents - 20.33.1. Short Studies

  1. Additional work on conditional logical operator
    1. ifpan123g
    2. ifpan23
    3. ifpdfor2
    4. ifporcor
    5. ifpdfan2
    6. ifpancor
    7. ifpdfor
    8. ifpdfan
    9. ifpbi2
    10. ifpbi3
    11. ifpim1
    12. ifpnot
    13. ifpid2
    14. ifpim2
    15. ifpbi23
    16. ifpbiidcor
    17. ifpbicor
    18. ifpxorcor
    19. ifpbi1
    20. ifpnot23
    21. ifpnotnotb
    22. ifpnorcor
    23. ifpnancor
    24. ifpnot23b
    25. ifpbiidcor2
    26. ifpnot23c
    27. ifpnot23d
    28. ifpdfnan
    29. ifpdfxor
    30. ifpbi12
    31. ifpbi13
    32. ifpbi123
    33. ifpidg
    34. ifpid3g
    35. ifpid2g
    36. ifpid1g
    37. ifpim23g
    38. ifpim3
    39. ifpnim1
    40. ifpim4
    41. ifpnim2
    42. ifpim123g
    43. ifpim1g
    44. ifp1bi
    45. ifpbi1b
    46. ifpimimb
    47. ifpororb
    48. ifpananb
    49. ifpnannanb
    50. ifpor123g
    51. ifpimim
    52. ifpbibib
    53. ifpxorxorb
  2. Sophisms
    1. rp-fakeimass
    2. rp-fakeanorass
    3. rp-fakeoranass
    4. rp-fakeinunass
    5. rp-fakeuninass
  3. Finite Sets
    1. rp-isfinite5
    2. rp-isfinite6
  4. General Observations
    1. intabssd
    2. eu0
    3. epelon2
    4. ontric3g
    5. dfsucon
    6. snen1g
    7. snen1el
    8. sn1dom
    9. pr2dom
    10. tr3dom
    11. ensucne0
    12. ensucne0OLD
    13. dfom6
    14. infordmin
    15. iscard4
    16. iscard5
    17. elrncard
    18. harval3
    19. harval3on
    20. en2pr
    21. pr2cv
    22. pr2el1
    23. pr2cv1
    24. pr2el2
    25. pr2cv2
    26. pren2
    27. pr2eldif1
    28. pr2eldif2
    29. pren2d
    30. aleph1min
    31. alephiso2
    32. alephiso3
  5. Infinite Sets
    1. pwelg
    2. pwinfig
    3. pwinfi2
    4. pwinfi3
    5. pwinfi
  6. Finite intersection property
    1. fipjust
    2. cllem0
    3. superficl
    4. superuncl
    5. ssficl
    6. ssuncl
    7. ssdifcl
    8. sssymdifcl
    9. fiinfi
  7. RP ADDTO: Subclasses and subsets
    1. rababg
  8. RP ADDTO: The intersection of a class
    1. elintabg
    2. elinintab
    3. elmapintrab
  9. RP ADDTO: Theorems requiring subset and intersection existence
    1. elinintrab
    2. inintabss
    3. inintabd
  10. RP ADDTO: Relations
    1. xpinintabd
    2. relintabex
    3. elcnvcnvintab
    4. relintab
    5. nonrel
    6. elnonrel
    7. cnvssb
    8. relnonrel
    9. cnvnonrel
    10. brnonrel
    11. dmnonrel
    12. rnnonrel
    13. resnonrel
    14. imanonrel
    15. cononrel1
    16. cononrel2
  11. RP ADDTO: Functions
    1. elmapintab
    2. fvnonrel
    3. elinlem
    4. elcnvcnvlem
  12. RP ADDTO: Finite induction (for finite ordinals)
    1. cnvcnvintabd
  13. RP ADDTO: First and second members of an ordered pair
    1. elcnvlem
    2. elcnvintab
    3. cnvintabd
  14. RP ADDTO: The reflexive and transitive properties of relations
    1. undmrnresiss
    2. reflexg
    3. cnvssco
    4. refimssco
  15. RP ADDTO: Basic properties of closures
    1. cleq2lem
    2. cbvcllem
    3. clublem
    4. clss2lem
    5. dfid7
    6. mptrcllem
    7. cotrintab
    8. rclexi
    9. rtrclexlem
    10. rtrclex
    11. trclubgNEW
    12. trclubNEW
    13. trclexi
    14. rtrclexi
    15. clrellem
    16. clcnvlem
    17. cnvtrucl0
    18. cnvrcl0
    19. cnvtrcl0
    20. dmtrcl
    21. rntrcl
    22. dfrtrcl5
  16. RP REPLACE: Definitions and basic properties of transitive closures
    1. trcleq2lemRP
  17. Additions for square root; absolute value
    1. sqrtcvallem1
    2. reabsifneg
    3. reabsifnpos
    4. reabsifpos
    5. reabsifnneg
    6. reabssgn
    7. sqrtcvallem2
    8. sqrtcvallem3
    9. sqrtcvallem4
    10. sqrtcvallem5
    11. sqrtcval
    12. sqrtcval2
    13. resqrtval
    14. imsqrtval
    15. resqrtvalex
    16. imsqrtvalex