Home | Intuitionistic Logic Explorer Theorem List (p. 127 of 129) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-bdsb 12601 | A formula resulting from proper substitution in a bounded formula is bounded. This probably cannot be proved from the other axioms, since neither the definiens in df-sb 1704, nor probably any other equivalent formula, is syntactically bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdeq 12602 | Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bd0 12603 | A formula equivalent to a bounded one is bounded. See also bd0r 12604. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bd0r 12604 | A formula equivalent to a bounded one is bounded. Stated with a commuted (compared with bd0 12603) biconditional in the hypothesis, to work better with definitions ( is the definiendum that one wants to prove bounded). (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdbi 12605 | A biconditional between two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdstab 12606 | Stability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED STAB | ||
Theorem | bddc 12607 | Decidability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED DECID | ||
Theorem | bd3or 12608 | A disjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED BOUNDED | ||
Theorem | bd3an 12609 | A conjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED BOUNDED | ||
Theorem | bdth 12610 | A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED | ||
Theorem | bdtru 12611 | The truth value is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdfal 12612 | The truth value is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdnth 12613 | A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED | ||
Theorem | bdnthALT 12614 | Alternate proof of bdnth 12613 not using bdfal 12612. Then, bdfal 12612 can be proved from this theorem, using fal 1306. The total number of proof steps would be 17 (for bdnthALT 12614) + 3 = 20, which is more than 8 (for bdfal 12612) + 9 (for bdnth 12613) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED | ||
Theorem | bdxor 12615 | The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bj-bdcel 12616* | Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdab 12617 | Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcdeq 12618 | Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED CondEq | ||
In line with our definitions of classes as extensions of predicates, it is useful to define a predicate for bounded classes, which is done in df-bdc 12620. Note that this notion is only a technical device which can be used to shorten proofs of (semantic) boundedness of formulas. As will be clear by the end of this subsection (see for instance bdop 12654), one can prove the boundedness of any concrete term using only setvars and bounded formulas, for instance, BOUNDED BOUNDED . The proofs are long since one has to prove boundedness at each step of the construction, without being able to prove general theorems like BOUNDED BOUNDED . | ||
Syntax | wbdc 12619 | Syntax for the predicate BOUNDED. |
BOUNDED | ||
Definition | df-bdc 12620* | Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdceq 12621 | Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdceqi 12622 | A class equal to a bounded one is bounded. Note the use of ax-ext 2082. See also bdceqir 12623. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdceqir 12623 | A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 12622) equality in the hypothesis, to work better with definitions ( is the definiendum that one wants to prove bounded; see comment of bd0r 12604). (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdel 12624* | The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdeli 12625* | Inference associated with bdel 12624. Its converse is bdelir 12626. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdelir 12626* | Inference associated with df-bdc 12620. Its converse is bdeli 12625. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcv 12627 | A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdcab 12628 | A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdph 12629 | A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bds 12630* | Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 12601; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 12601. (Contributed by BJ, 19-Nov-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcrab 12631* | A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdne 12632 | Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdnel 12633* | Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdreu 12634* |
Boundedness of existential uniqueness.
Remark regarding restricted quantifiers: the formula need not be bounded even if and are. Indeed, is bounded by bdcvv 12636, and (in minimal propositional calculus), so by bd0 12603, if were bounded when is bounded, then would be bounded as well when is bounded, which is not the case. The same remark holds with . (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdrmo 12635* | Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcvv 12636 | The universal class is bounded. The formulation may sound strange, but recall that here, "bounded" means "Δ_{0}". (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdsbc 12637 | A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 12638. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdsbcALT 12638 | Alternate proof of bdsbc 12637. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bdccsb 12639 | A class resulting from proper substitution of a setvar for a setvar in a bounded class is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcdif 12640 | The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdcun 12641 | The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdcin 12642 | The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdss 12643 | The inclusion of a setvar in a bounded class is a bounded formula. Note: apparently, we cannot prove from the present axioms that equality of two bounded classes is a bounded formula. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcnul 12644 | The empty class is bounded. See also bdcnulALT 12645. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdcnulALT 12645 | Alternate proof of bdcnul 12644. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 12623, or use the corresponding characterizations of its elements followed by bdelir 12626. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED | ||
Theorem | bdeq0 12646 | Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
Theorem | bj-bd0el 12647 | Boundedness of the formula "the empty set belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
Theorem | bdcpw 12648 | The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcsn 12649 | The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdcpr 12650 | The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdctp 12651 | The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdsnss 12652* | Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdvsn 12653* | Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdop 12654 | The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
Theorem | bdcuni 12655 | The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.) |
BOUNDED | ||
Theorem | bdcint 12656 | The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdciun 12657* | The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdciin 12658* | The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcsuc 12659 | The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdeqsuc 12660* | Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
Theorem | bj-bdsucel 12661 | Boundedness of the formula "the successor of the setvar belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
Theorem | bdcriota 12662* | A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.) |
BOUNDED BOUNDED | ||
In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory. | ||
Axiom | ax-bdsep 12663* | Axiom scheme of bounded (or restricted, or Δ_{0}) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 3986. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsep1 12664* | Version of ax-bdsep 12663 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsep2 12665* | Version of ax-bdsep 12663 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 12664 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnft 12666* | Closed form of bdsepnf 12667. Version of ax-bdsep 12663 with one disjoint variable condition removed, the other disjoint variable condition replaced by a non-freeness antecedent, and without initial universal quantifier. Use bdsep1 12664 when sufficient. (Contributed by BJ, 19-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnf 12667* | Version of ax-bdsep 12663 with one disjoint variable condition removed, the other disjoint variable condition replaced by a non-freeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 12668. Use bdsep1 12664 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnfALT 12668* | Alternate proof of bdsepnf 12667, not using bdsepnft 12666. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED | ||
Theorem | bdzfauscl 12669* | Closed form of the version of zfauscl 3988 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.) |
BOUNDED | ||
Theorem | bdbm1.3ii 12670* | Bounded version of bm1.3ii 3989. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bj-axemptylem 12671* | Lemma for bj-axempty 12672 and bj-axempty2 12673. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.) |
Theorem | bj-axempty 12672* | Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a nonempty universe. See axnul 3993. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.) |
Theorem | bj-axempty2 12673* | Axiom of the empty set from bounded separation, alternate version to bj-axempty 12672. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.) |
Theorem | bj-nalset 12674* | nalset 3998 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-vprc 12675 | vprc 4000 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-nvel 12676 | nvel 4001 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-vnex 12677 | vnex 3999 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bdinex1 12678 | Bounded version of inex1 4002. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdinex2 12679 | Bounded version of inex2 4003. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdinex1g 12680 | Bounded version of inex1g 4004. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssex 12681 | Bounded version of ssex 4005. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexi 12682 | Bounded version of ssexi 4006. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexg 12683 | Bounded version of ssexg 4007. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexd 12684 | Bounded version of ssexd 4008. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdrabexg 12685* | Bounded version of rabexg 4011. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bj-inex 12686 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-intexr 12687 | intexr 4015 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-intnexr 12688 | intnexr 4016 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-zfpair2 12689 | Proof of zfpair2 4070 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-prexg 12690 | Proof of prexg 4071 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-snexg 12691 | snexg 4048 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-snex 12692 | snex 4049 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-sels 12693* | If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.) |
Theorem | bj-axun2 12694* | axun2 4295 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniex2 12695* | uniex2 4296 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniex 12696 | uniex 4297 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniexg 12697 | uniexg 4299 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-unex 12698 | unex 4300 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bdunexb 12699 | Bounded version of unexb 4301. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bj-unexg 12700 | unexg 4302 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |