Metamath Proof Explorer

Table of Contents - 21.38.4. Short Studies

1. nlimsuc
2. nlim1NEW
3. nlim2NEW
4. nlim3
5. nlim4
6. oa1un
7. oa1cl
8. 0finon
9. 1finon
10. 2finon
11. 3finon
12. 4finon
13. finona1cl
14. finonex
15. fzunt
16. fzuntd
17. fzunt1d
18. fzuntgd
19. 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
20. Sophisms
    1. rp-fakeimass
    2. rp-fakeanorass
    3. rp-fakeoranass
    4. rp-fakeinunass
    5. rp-fakeuninass
21. Finite Sets
    1. rp-isfinite5
    2. rp-isfinite6
22. 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. minregex
    17. minregex2
    18. iscard5
    19. elrncard
    20. harval3
    21. harval3on
    22. omssrncard
    23. 0iscard
    24. 1iscard
    25. omiscard
    26. sucomisnotcard
    27. nna1iscard
    28. har2o
    29. en2pr
    30. pr2cv
    31. pr2el1
    32. pr2cv1
    33. pr2el2
    34. pr2cv2
    35. pren2
    36. pr2eldif1
    37. pr2eldif2
    38. pren2d
    39. aleph1min
    40. alephiso2
    41. alephiso3
23. Infinite Sets
    1. pwelg
    2. pwinfig
    3. pwinfi2
    4. pwinfi3
    5. pwinfi
24. Finite intersection property
    1. fipjust
    2. cllem0
    3. superficl
    4. superuncl
    5. ssficl
    6. ssuncl
    7. ssdifcl
    8. sssymdifcl
    9. fiinfi
25. RP ADDTO: Subclasses and subsets
    1. rababg
26. RP ADDTO: The intersection of a class
    1. elinintab
    2. elmapintrab
27. RP ADDTO: Theorems requiring subset and intersection existence
    1. elinintrab
    2. inintabss
    3. inintabd
28. 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
29. RP ADDTO: Functions
    1. elmapintab
    2. fvnonrel
    3. elinlem
    4. elcnvcnvlem
30. RP ADDTO: Finite induction (for finite ordinals)
    1. cnvcnvintabd
31. RP ADDTO: First and second members of an ordered pair
    1. elcnvlem
    2. elcnvintab
    3. cnvintabd
32. RP ADDTO: The reflexive and transitive properties of relations
    1. undmrnresiss
    2. reflexg
    3. cnvssco
    4. refimssco
33. 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
34. RP REPLACE: Definitions and basic properties of transitive closures
    1. trcleq2lemRP
35. 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