![]() |
Intuitionistic Logic Explorer Theorem List (p. 144 of 145) | < 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 | bj-axempty 14301* | 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 4125. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4126 instead. (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-axempty2 14302* | Axiom of the empty set from bounded separation, alternate version to bj-axempty 14301. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4126 instead. (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nalset 14303* | nalset 4130 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-vprc 14304 | vprc 4132 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nvel 14305 | nvel 4133 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-vnex 14306 | vnex 4131 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdinex1 14307 | Bounded version of inex1 4134. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdinex2 14308 | Bounded version of inex2 4135. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdinex1g 14309 | Bounded version of inex1g 4136. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdssex 14310 | Bounded version of ssex 4137. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdssexi 14311 | Bounded version of ssexi 4138. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdssexg 14312 | Bounded version of ssexg 4139. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdssexd 14313 | Bounded version of ssexd 4140. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdrabexg 14314* | Bounded version of rabexg 4143. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inex 14315 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-intexr 14316 | intexr 4147 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-intnexr 14317 | intnexr 4148 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-zfpair2 14318 | Proof of zfpair2 4207 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-prexg 14319 | Proof of prexg 4208 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-snexg 14320 | snexg 4181 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-snex 14321 | snex 4182 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-sels 14322* | 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 14323* | axun2 4432 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-uniex2 14324* | uniex2 4433 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-uniex 14325 | uniex 4434 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-uniexg 14326 | uniexg 4436 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-unex 14327 | unex 4438 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdunexb 14328 | Bounded version of unexb 4439. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-unexg 14329 | unexg 4440 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-sucexg 14330 | sucexg 4494 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-sucex 14331 | sucex 4495 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-bj-d0cl 14332 | Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-d0clsepcl 14333 | Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) |
![]() ![]() | ||
Syntax | wind 14334 | Syntax for inductive classes. |
![]() ![]() | ||
Definition | df-bj-ind 14335* | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-indsuc 14336 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-indeq 14337 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-bdind 14338 |
Boundedness of the formula "the setvar ![]() |
![]() ![]() | ||
Theorem | bj-indint 14339* | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-indind 14340* |
If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-dfom 14341 |
Alternate definition of ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omind 14342 |
![]() |
![]() ![]() | ||
Theorem | bj-omssind 14343 |
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-ssom 14344* |
A characterization of subclasses of ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-om 14345* |
A set is equal to ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-2inf 14346* | Two formulations of the axiom of infinity (see ax-infvn 14349 and bj-omex 14350) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4590 and peano3 4592 already show this. In this section, we prove bj-peano2 14347 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms. | ||
Theorem | bj-peano2 14347 | Constructive proof of peano2 4591. Temporary note: another possibility is to simply replace sucexg 4494 with bj-sucexg 14330 in the proof of peano2 4591. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | peano5set 14348* |
Version of peano5 4594 when ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In the absence of full separation, the axiom of infinity has to be stated more precisely, as the existence of the smallest class containing the empty set and the successor of each of its elements. | ||
In this section, we introduce the axiom of infinity in a constructive setting
(ax-infvn 14349) and deduce that the class | ||
Axiom | ax-infvn 14349* | Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4584) from which one then proves, using full separation, that the wanted set exists (omex 4589). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omex 14350 | Proof of omex 4589 from ax-infvn 14349. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() | ||
In this section, we give constructive proofs of two versions of Peano's fifth postulate. | ||
Theorem | bdpeano5 14351* | Bounded version of peano5 4594. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | speano5 14352* |
Version of peano5 4594 when ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In this section, we prove various versions of bounded induction from the basic axioms of CZF (in particular, without the axiom of set induction). We also prove Peano's fourth postulate. Together with the results from the previous sections, this proves from the core axioms of CZF (with infinity) that the set of natural number ordinals satisfies the five Peano postulates and thus provides a model for the set of natural numbers. | ||
Theorem | findset 14353* |
Bounded induction (principle of induction when ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdfind 14354* |
Bounded induction (principle of induction when ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-bdfindis 14355* | Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4596 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4596, finds2 4597, finds1 4598. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-bdfindisg 14356* | Version of bj-bdfindis 14355 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 14355 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-bdfindes 14357 | Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 14355 for explanations. From this version, it is easy to prove the bounded version of findes 4599. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nn0suc0 14358* | Constructive proof of a variant of nn0suc 4600. For a constructive proof of nn0suc 4600, see bj-nn0suc 14372. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nntrans 14359 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nntrans2 14360 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nnelirr 14361 | A natural number does not belong to itself. Version of elirr 4537 for natural numbers, which does not require ax-setind 4533. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nnen2lp 14362 |
A version of en2lp 4550 for natural numbers, which does not require
ax-setind 4533.
Note: using this theorem and bj-nnelirr 14361, one can remove dependency on ax-setind 4533 from nntri2 6489 and nndcel 6495; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-peano4 14363 | Remove from peano4 4593 dependency on ax-setind 4533. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omtrans 14364 |
The set ![]() ![]()
The idea is to use bounded induction with the formula |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omtrans2 14365 |
The set ![]() |
![]() ![]() ![]() | ||
Theorem | bj-nnord 14366 | A natural number is an ordinal class. Constructive proof of nnord 4608. Can also be proved from bj-nnelon 14367 if the latter is proved from bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-nnelon 14367 | A natural number is an ordinal. Constructive proof of nnon 4606. Can also be proved from bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omord 14368 |
The set ![]() |
![]() ![]() ![]() | ||
Theorem | bj-omelon 14369 |
The set ![]() |
![]() ![]() ![]() ![]() | ||
Theorem | bj-omsson 14370 | Constructive proof of omsson 4609. See also bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged. |
![]() ![]() ![]() ![]() | ||
Theorem | bj-omssonALT 14371 | Alternate proof of bj-omsson 14370. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() | ||
Theorem | bj-nn0suc 14372* |
Proof of (biconditional form of) nn0suc 4600 from the core axioms of CZF.
See also bj-nn0sucALT 14386. As a characterization of the elements of
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In this section, we add the axiom of set induction to the core axioms of CZF. | ||
In this section, we prove some variants of the axiom of set induction. | ||
Theorem | setindft 14373* | Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | setindf 14374* | Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | setindis 14375* | Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-bdsetind 14376* | Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bdsetindis 14377* | Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vnlem1 14378* | Lemma for bj-inf2vn 14382. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vnlem2 14379* | Lemma for bj-inf2vnlem3 14380 and bj-inf2vnlem4 14381. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vnlem3 14380* | Lemma for bj-inf2vn 14382. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vnlem4 14381* | Lemma for bj-inf2vn2 14383. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vn 14382* |
A sufficient condition for ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-inf2vn2 14383* |
A sufficient condition for ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-inf2 14384* | Another axiom of infinity in a constructive setting (see ax-infvn 14349). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-omex2 14385 |
Using bounded set induction and the strong axiom of infinity, ![]() |
![]() ![]() ![]() ![]() | ||
Theorem | bj-nn0sucALT 14386* | Alternate proof of bj-nn0suc 14372, also constructive but from ax-inf2 14384, hence requiring ax-bdsetind 14376. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In this section, using the axiom of set induction, we prove full induction on the set of natural numbers. | ||
Theorem | bj-findis 14387* | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 14355 for a bounded version not requiring ax-setind 4533. See finds 4596 for a proof in IZF. From this version, it is easy to prove of finds 4596, finds2 4597, finds1 4598. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-findisg 14388* | Version of bj-findis 14387 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 14387 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bj-findes 14389 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 14387 for explanations. From this version, it is easy to prove findes 4599. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In this section, we state the axiom scheme of strong collection, which is part of CZF set theory. | ||
Axiom | ax-strcoll 14390* |
Axiom scheme of strong collection. It is stated with all possible
disjoint variable conditions, to show that this weak form is sufficient.
The antecedent means that ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | strcoll2 14391* | Version of ax-strcoll 14390 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | strcollnft 14392* | Closed form of strcollnf 14393. (Contributed by BJ, 21-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | strcollnf 14393* |
Version of ax-strcoll 14390 with one disjoint variable condition
removed,
the other disjoint variable condition replaced with a nonfreeness
hypothesis, and without initial universal quantifier. Version of
strcoll2 14391 with the disjoint variable condition on ![]() ![]() ![]()
This proof aims to demonstrate a standard technique, but strcoll2 14391 will
generally suffice: since the theorem asserts the existence of a set
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | strcollnfALT 14394* | Alternate proof of strcollnf 14393, not using strcollnft 14392. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
In this section, we state the axiom scheme of subset collection, which is part of CZF set theory. | ||
Axiom | ax-sscoll 14395* |
Axiom scheme of subset collection. It is stated with all possible
disjoint variable conditions, to show that this weak form is sufficient.
The antecedent means that ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | sscoll2 14396* | Version of ax-sscoll 14395 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-ddkcomp 14397 | Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then Axiom ax-ddkcomp 14397 should be used in place of construction specific results. In particular, axcaucvg 7890 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nnnotnotr 14398 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 850, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ss1oel2o 14399 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4195 which more directly illustrates the contrast with el2oss1o 6438. (Contributed by Jim Kingdon, 8-Aug-2022.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nnti 14400 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |