Metamath Proof Explorer

Table of Contents - 20.16. Mathbox for BJ

In this mathbox, we try to respect the ordering of the sections of the main part. There are strengthenings of theorems of the main part, as well as work on reducing axiom dependencies.

1. Propositional calculus
   1. Derived rules of inference
   2. A syntactic theorem
   3. Minimal implicational calculus
   4. Positive calculus
   5. Implication and negation
   6. Disjunction
   7. Logical equivalence
   8. The conditional operator for propositions
   9. Propositional calculus: miscellaneous
2. Modal logic
   1. bj-axdd2
   2. bj-axd2d
   3. bj-axtd
   4. bj-gl4
   5. bj-axc4
3. Provability logic
   1. cprvb
   2. ax-prv1
   3. ax-prv2
   4. ax-prv3
   5. prvlem1
   6. prvlem2
   7. bj-babygodel
   8. bj-babylob
   9. bj-godellob
4. First-order logic
   1. Universal and existential quantifiers, nonfreeness predicate
   2. Adding ax-gen
   3. Adding ax-4
   4. Adding ax-5
   5. Equality and substitution
   6. Adding ax-6
   7. Adding ax-7
   8. Membership predicate, ax-8 and ax-9
   9. Logical redundancy of ax-10--13
   10. Adding ax-10
   11. Adding ax-11
   12. Adding ax-12
   13. Really adding ax-12
   14. Nonfreeness
   15. Adding ax-13
   16. Removing dependencies on ax-13 (and ax-11)
   17. Strengthenings of theorems of the main part
   18. Distinct var metavariables
   19. Around ~ equsal
   20. Some Principia Mathematica proofs
   21. Alternate definition of substitution
   22. Lemmas for substitution
   23. Existential uniqueness
   24. First-order logic: miscellaneous
5. Set theory
   1. Eliminability of class terms
   2. Classes without the axiom of extensionality
   3. Characterization among sets versus among classes
   4. The nonfreeness quantifier for classes
   5. Lemmas for class substitution
   6. Removing some axiom requirements and disjoint variable conditions
   7. Class abstractions
   8. Generalized class abstractions
   9. Restricted nonfreeness
   10. Russell's paradox
   11. Curry's paradox in set theory
   12. Some disjointness results
   13. Complements on direct products
   14. "Singletonization" and tagging
   15. Tuples of classes
   16. Set theory: elementary operations relative to a universe
   17. Set theory: miscellaneous
   18. Evaluation at a class
   19. Elementwise operations
   20. Elementwise intersection (families of sets induced on a subset)
   21. Moore collections (complements)
   22. Maps-to notation for functions with three arguments
   23. Currying
   24. Setting components of extensible structures
6. Extended real and complex numbers, real and complex projective lines
   1. Complements on class abstractions of ordered pairs and binary relations
   2. Identity relation (complements)
   3. Functionalized identity (diagonal in a Cartesian square)
   4. Direct image and inverse image
   5. Extended numbers and projective lines as sets
   6. Addition and opposite
   7. Order relation on the extended reals
   8. Argument, multiplication and inverse
   9. The canonical bijection from the finite ordinals
   10. Divisibility
7. Monoids
   1. bj-smgrpssmgm
   2. bj-smgrpssmgmel
   3. bj-mndsssmgrp
   4. bj-mndsssmgrpel
   5. bj-cmnssmnd
   6. bj-cmnssmndel
   7. bj-grpssmnd
   8. bj-grpssmndel
   9. bj-ablssgrp
   10. bj-ablssgrpel
   11. bj-ablsscmn
   12. bj-ablsscmnel
   13. bj-modssabl
   14. bj-vecssmod
   15. bj-vecssmodel
   16. Finite sums in monoids
8. Affine, Euclidean, and Cartesian geometry
   1. Real vector spaces
   2. Complex numbers (supplements)
   3. Barycentric coordinates
9. Monoid of endomorphisms
   1. cend
   2. df-bj-end
   3. bj-endval
   4. bj-endbase
   5. bj-endcomp
   6. bj-endmnd