Home | Intuitionistic Logic Explorer Theorem List (p. 94 of 95) | < 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 | ||
Theorem | bdeli 9301* | Inference associated with bdel 9300. Its converse is bdelir 9302. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdelir 9302* | Inference associated with df-bdc 9296. Its converse is bdeli 9301. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcv 9303 | A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdcab 9304 | A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdph 9305 | A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bds 9306* | Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 9277; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 9277. (Contributed by BJ, 19-Nov-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcrab 9307* | 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 9308 | Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdnel 9309* | Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdreu 9310* |
Boundedness of existential uniqueness.
Remark regarding restricted quantifiers: the formula need not be bounded even if and are. Indeed, is bounded by bdcvv 9312, and (in minimal propositional calculus), so by bd0 9279, 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 9311* | Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcvv 9312 | 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 9313 | A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 9314. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdsbcALT 9314 | Alternate proof of bdsbc 9313. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bdccsb 9315 | 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 9316 | The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdcun 9317 | The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdcin 9318 | The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED BOUNDED | ||
Theorem | bdss 9319 | 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 9320 | The empty class is bounded. See also bdcnulALT 9321. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED | ||
Theorem | bdcnulALT 9321 | Alternate proof of bdcnul 9320. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 9299, or use the corresponding characterizations of its elements followed by bdelir 9302. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED | ||
Theorem | bdeq0 9322 | Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
Theorem | bj-bd0el 9323 | Boundedness of the formula "the empty set belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
Theorem | bdcpw 9324 | The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.) |
BOUNDED BOUNDED | ||
Theorem | bdcsn 9325 | The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdcpr 9326 | The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdctp 9327 | The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdsnss 9328* | 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 9329* | Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdop 9330 | The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
Theorem | bdcuni 9331 | The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.) |
BOUNDED | ||
Theorem | bdcint 9332 | The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdciun 9333* | 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 9334* | 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 9335 | The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
BOUNDED | ||
Theorem | bdeqsuc 9336* | 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 9337 | Boundedness of the formula "the successor of the setvar belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
Theorem | bdcriota 9338* | 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 9339* | 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 3866. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsep1 9340* | Version of ax-bdsep 9339 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsep2 9341* | Version of ax-bdsep 9339 with one DV condition removed and without initial universal quantifier. Use bdsep1 9340 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnft 9342* | Closed form of bdsepnf 9343. Version of ax-bdsep 9339 with one DV condition removed, the other DV condition replaced by a non-freeness antecedent, and without initial universal quantifier. Use bdsep1 9340 when sufficient. (Contributed by BJ, 19-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnf 9343* | Version of ax-bdsep 9339 with one DV condition removed, the other DV condition replaced by a non-freeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 9344. Use bdsep1 9340 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
BOUNDED | ||
Theorem | bdsepnfALT 9344* | Alternate proof of bdsepnf 9343, not using bdsepnft 9342. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
BOUNDED | ||
Theorem | bdzfauscl 9345* | Closed form of the version of zfauscl 3868 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.) |
BOUNDED | ||
Theorem | bdbm1.3ii 9346* | Bounded version of bm1.3ii 3869. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bj-axemptylem 9347* | Lemma for bj-axempty 9348 and bj-axempty2 9349. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
Theorem | bj-axempty 9348* | Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a non-empty universe. See axnul 3873. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
Theorem | bj-axempty2 9349* | Axiom of the empty set from bounded separation, alternate version to bj-axempty 9348. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.) |
Theorem | bj-nalset 9350* | nalset 3878 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-vprc 9351 | vprc 3879 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-nvel 9352 | nvel 3880 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-vnex 9353 | vnex 3881 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bdinex1 9354 | Bounded version of inex1 3882. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdinex2 9355 | Bounded version of inex2 3883. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdinex1g 9356 | Bounded version of inex1g 3884. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssex 9357 | Bounded version of ssex 3885. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexi 9358 | Bounded version of ssexi 3886. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexg 9359 | Bounded version of ssexg 3887. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdssexd 9360 | Bounded version of ssexd 3888. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bdrabexg 9361* | Bounded version of rabexg 3891. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bj-inex 9362 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-intexr 9363 | intexr 3895 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-intnexr 9364 | intnexr 3896 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-zfpair2 9365 | Proof of zfpair2 3936 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-prexg 9366 | Proof of prexg 3938 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-snexg 9367 | snexg 3927 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-snex 9368 | snex 3928 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-sels 9369* | 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 9370* | axun2 4138 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniex2 9371* | uniex2 4139 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniex 9372 | uniex 4140 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-uniexg 9373 | uniexg 4141 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-unex 9374 | unex 4142 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bdunexb 9375 | Bounded version of unexb 4143. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
Theorem | bj-unexg 9376 | unexg 4144 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-sucexg 9377 | sucexg 4190 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-sucex 9378 | sucex 4191 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
Axiom | ax-bj-d0cl 9379 | Axiom for Δ_{0}-classical logic. (Contributed by BJ, 2-Jan-2020.) |
BOUNDED DECID | ||
Theorem | bj-notbi 9380 | Equivalence property for negation. TODO: minimize all theorems using notbid 591 and notbii 593. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) |
Theorem | bj-notbii 9381 | Inference associated with bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) |
Theorem | bj-notbid 9382 | Deduction form of bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) |
Theorem | bj-dcbi 9383 | Equivalence property for DECID. TODO: solve conflict with dcbi 843; minimize dcbii 746 and dcbid 747 with it, as well as theorems using those. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) |
DECID DECID | ||
Theorem | bj-d0clsepcl 9384 | Δ_{0}-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) |
DECID | ||
Syntax | wind 9385 | Syntax for inductive classes. |
Ind | ||
Definition | df-bj-ind 9386* | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
Theorem | bj-indsuc 9387 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
Theorem | bj-indeq 9388 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) |
Ind Ind | ||
Theorem | bj-bdind 9389 | Boundedness of the formula "the setvar is an inductive class". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED Ind | ||
Theorem | bj-indint 9390* | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) |
Ind Ind | ||
Theorem | bj-indind 9391* | If is inductive and is "inductive in ", then is inductive. (Contributed by BJ, 25-Oct-2020.) |
Ind Ind | ||
Theorem | bj-dfom 9392 | Alternate definition of , as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
Theorem | bj-omind 9393 | is an inductive class. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
Theorem | bj-omssind 9394 | is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind | ||
Theorem | bj-ssom 9395* | A characterization of subclasses of . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind | ||
Theorem | bj-om 9396* | A set is equal to if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind Ind | ||
Theorem | bj-2inf 9397* | Two formulations of the axiom of infinity (see ax-infvn 9401 and bj-omex 9402) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind Ind | ||
The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4260 and peano3 4262 already show this. In this section, we prove bj-peano2 9398 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms. | ||
Theorem | bj-peano2 9398 | Constructive proof of peano2 4261. Temporary note: another possibility is to simply replace sucexg 4190 with bj-sucexg 9377 in the proof of peano2 4261. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
Theorem | peano5set 9399* | Version of peano5 4264 when is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
Theorem | peano5setOLD 9400* | Obsolete version of peano5set 9399 as of 26-Oct-2020. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |