Metamath Proof Explorer

Table of Contents - 20.43. Mathbox for Alexander van der Vekens

  1. General auxiliary theorems (1)
    1. Unordered and ordered pairs - extension for singletons
    2. Unordered and ordered pairs - extension for unordered pairs
    3. Unordered and ordered pairs - extension for ordered pairs
    4. Relations - extension
    5. Definite description binder (inverted iota) - extension
    6. Functions - extension
  2. Alternative for Russell's definition of a description binder
    1. caiota
    2. aiotajust
    3. df-aiota
    4. dfaiota2
    5. reuabaiotaiota
    6. reuaiotaiota
    7. aiotaexb
    8. aiotavb
    9. iotan0aiotaex
    10. aiotaexaiotaiota
    11. aiotaval
    12. aiota0def
    13. aiota0ndef
  3. Double restricted existential uniqueness
    1. Restricted quantification (extension)
    2. Restricted uniqueness and "at most one" quantification
    3. Analogs to Existential uniqueness (double quantification)
    4. Additional theorems for double restricted existential uniqueness
  4. Alternative definitions of function and operation values
    1. wdfat
    2. cafv
    3. caov
    4. df-dfat
    5. df-afv
    6. df-aov
    7. Restricted quantification (extension)
    8. The universal class (extension)
    9. Introduce the Axiom of Power Sets (extension)
    10. Predicate "defined at"
    11. Alternative definition of the value of a function
    12. Alternative definition of the value of an operation
  5. Alternative definitions of function values (2)
    1. cafv2
    2. df-afv2
    3. dfatafv2iota
    4. ndfatafv2
    5. ndfatafv2undef
    6. dfatafv2ex
    7. afv2ex
    8. afv2eq12d
    9. afv2eq1
    10. afv2eq2
    11. nfafv2
    12. csbafv212g
    13. fexafv2ex
    14. ndfatafv2nrn
    15. ndmafv2nrn
    16. funressndmafv2rn
    17. afv2ndefb
    18. nfunsnafv2
    19. afv2prc
    20. dfatafv2rnb
    21. afv2orxorb
    22. dmafv2rnb
    23. fundmafv2rnb
    24. afv2elrn
    25. afv20defat
    26. fnafv2elrn
    27. fafv2elrn
    28. fafv2elrnb
    29. frnvafv2v
    30. tz6.12-2-afv2
    31. afv2eu
    32. afv2res
    33. tz6.12-afv2
    34. tz6.12-1-afv2
    35. tz6.12c-afv2
    36. tz6.12i-afv2
    37. funressnbrafv2
    38. dfatbrafv2b
    39. dfatopafv2b
    40. funbrafv2
    41. fnbrafv2b
    42. fnopafv2b
    43. funbrafv22b
    44. funopafv2b
    45. dfatsnafv2
    46. dfafv23
    47. dfatdmfcoafv2
    48. dfatcolem
    49. dfatco
    50. afv2co2
    51. rlimdmafv2
    52. dfafv22
    53. afv2ndeffv0
    54. dfatafv2eqfv
    55. afv2rnfveq
    56. afv20fv0
    57. afv2fvn0fveq
    58. afv2fv0
    59. afv2fv0b
    60. afv2fv0xorb
  6. General auxiliary theorems (2)
    1. Logical conjunction - extension
    2. Abbreviated conjunction and disjunction of three wff's - extension
    3. Negated membership (alternative)
    4. The empty set - extension
    5. Indexed union and intersection - extension
    6. Functions - extension
    7. Maps-to notation - extension
    8. Ordering on reals - extension
    9. Subtraction - extension
    10. Ordering on reals (cont.) - extension
    11. Imaginary and complex number properties - extension
    12. Nonnegative integers (as a subset of complex numbers) - extension
    13. Integers (as a subset of complex numbers) - extension
    14. Decimal arithmetic - extension
    15. Upper sets of integers - extension
    16. Infinity and the extended real number system (cont.) - extension
    17. Finite intervals of integers - extension
    18. Half-open integer ranges - extension
    19. The modulo (remainder) operation - extension
    20. The infinite sequence builder "seq"
    21. Finite and infinite sums - extension
    22. Extensible structures - extension
  7. Preimages of function values
    1. preimafvsnel
    2. preimafvn0
    3. uniimafveqt
    4. uniimaprimaeqfv
    5. setpreimafvex
    6. elsetpreimafvb
    7. elsetpreimafv
    8. elsetpreimafvssdm
    9. fvelsetpreimafv
    10. preimafvelsetpreimafv
    11. preimafvsspwdm
    12. 0nelsetpreimafv
    13. elsetpreimafvbi
    14. elsetpreimafveqfv
    15. eqfvelsetpreimafv
    16. elsetpreimafvrab
    17. imaelsetpreimafv
    18. uniimaelsetpreimafv
    19. elsetpreimafveq
    20. fundcmpsurinjlem1
    21. fundcmpsurinjlem2
    22. fundcmpsurinjlem3
    23. imasetpreimafvbijlemf
    24. imasetpreimafvbijlemfv
    25. imasetpreimafvbijlemfv1
    26. imasetpreimafvbijlemf1
    27. imasetpreimafvbijlemfo
    28. imasetpreimafvbij
    29. fundcmpsurbijinjpreimafv
    30. fundcmpsurinjpreimafv
    31. fundcmpsurinj
    32. fundcmpsurbijinj
    33. fundcmpsurinjimaid
    34. fundcmpsurinjALT
  8. Partitions of real intervals
    1. ciccp
    2. df-iccp
    3. iccpval
    4. iccpart
    5. iccpartimp
    6. iccpartres
    7. iccpartxr
    8. iccpartgtprec
    9. iccpartipre
    10. iccpartiltu
    11. iccpartigtl
    12. iccpartlt
    13. iccpartltu
    14. iccpartgtl
    15. iccpartgt
    16. iccpartleu
    17. iccpartgel
    18. iccpartrn
    19. iccpartf
    20. iccpartel
    21. iccelpart
    22. iccpartiun
    23. icceuelpartlem
    24. icceuelpart
    25. iccpartdisj
    26. iccpartnel
  9. Shifting functions with an integer range domain
    1. fargshiftfv
    2. fargshiftf
    3. fargshiftf1
    4. fargshiftfo
    5. fargshiftfva
  10. Words over a set (extension)
    1. Last symbol of a word - extension
  11. Unordered pairs
    1. Interchangeable setvar variables
    2. Set of unordered pairs
    3. Proper (unordered) pairs
    4. Set of proper unordered pairs
  12. Number theory (extension)
    1. Fermat numbers
    2. Mersenne primes
    3. Proth's theorem
    4. Solutions of quadratic equations
  13. Even and odd numbers
    1. Definitions and basic properties
    2. Alternate definitions using the "divides" relation
    3. Alternate definitions using the "modulo" operation
    4. Alternate definitions using the "gcd" operation
    5. Theorems of part 5 revised
    6. Theorems of part 6 revised
    7. Theorems of AV's mathbox revised
    8. Additional theorems
    9. Perfect Number Theorem (revised)
  14. Number theory (extension 2)
    1. Fermat pseudoprimes
    2. Goldbach's conjectures
  15. Graph theory (extension)
    1. Isomorphic graphs
    2. Loop-free graphs - extension
    3. Walks - extension
    4. Edges of graphs expressed as sets of unordered pairs
  16. Monoids (extension)
    1. Auxiliary theorems
    2. Magmas, Semigroups and Monoids (extension)
    3. Magma homomorphisms and submagmas
    4. Examples and counterexamples for magmas, semigroups and monoids (extension)
    5. Group sum operation (extension 1)
  17. Magmas and internal binary operations (alternate approach)
    1. Laws for internal binary operations
    2. Internal binary operations
    3. Alternative definitions for magmas and semigroups
  18. Categories (extension)
    1. Subcategories (extension)
  19. Rings (extension)
    1. Nonzero rings (extension)
    2. Non-unital rings ("rngs")
    3. Rng homomorphisms
    4. Ring homomorphisms (extension)
    5. Ideals as non-unital rings
    6. The non-unital ring of even integers
    7. A constructed not unital ring
    8. The category of non-unital rings
    9. The category of (unital) rings
    10. Subcategories of the category of rings
  20. Basic algebraic structures (extension)
    1. Auxiliary theorems
    2. The binomial coefficient operation (extension)
    3. The ` ZZ `-module ` ZZ X. ZZ `
    4. Group sum operation (extension 2)
    5. Symmetric groups (extension)
    6. Divisibility (extension)
    7. The support of functions (extension)
    8. Finitely supported functions (extension)
    9. Left modules (extension)
    10. Associative algebras (extension)
    11. Univariate polynomials (extension)
    12. Univariate polynomials (examples)
  21. Linear algebra (extension)
    1. The subalgebras of diagonal and scalar matrices (extension)
    2. Linear combinations
    3. Linear independence
    4. Simple left modules and the ` ZZ `-module
    5. Differences between (left) modules and (left) vector spaces
  22. Complexity theory
    1. Auxiliary theorems
    2. The modulo (remainder) operation (extension)
    3. Even and odd integers
    4. The natural logarithm on complex numbers (extension)
    5. Division of functions
    6. Upper bounds
    7. Logarithm to an arbitrary base (extension)
    8. The binary logarithm
    9. Binary length
    10. Digits
    11. Nonnegative integer as sum of its shifted digits
    12. Algorithms for the multiplication of nonnegative integers
  23. Elementary geometry (extension)
    1. Auxiliary theorems
    2. Real euclidean space of dimension 2
    3. Spheres and lines in real Euclidean spaces