P. 157 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15601-15700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bdelir 15601*	Inference associated with df-bdc 15595. Its converse is bdeli 15600. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x e. A   =>    |- BOUNDED A
Theorem	bdcv 15602	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x
Theorem	bdcab 15603	A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED { x | ph }
Theorem	bdph 15604	A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED { x | ph }   =>    |- BOUNDED ph
Theorem	bds 15605*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 15576; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 15576. (Contributed by BJ, 19-Nov-2019.)
|- BOUNDED ph   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- BOUNDED ps
Theorem	bdcrab 15606*	A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED ph   =>    |- BOUNDED { x e. A | ph }
Theorem	bdne 15607	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x =/= y
Theorem	bdnel 15608*	Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e/ A
Theorem	bdreu 15609*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula A. x e. A ph need not be bounded even if A and ph are. Indeed, _V is bounded by bdcvv 15611, and |- ( A. x e. _V ph <-> A. x ph ) (in minimal propositional calculus), so by bd0 15578, if A. x e. _V ph were bounded when ph is bounded, then A. x ph would be bounded as well when ph is bounded, which is not the case. The same remark holds with E. , E! , E*. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E! x e. y ph
Theorem	bdrmo 15610*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E* x e. y ph
Theorem	bdcvv 15611	The universal class is bounded. The formulation may sound strange, but recall that here, "bounded" means "Δ0". (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED _V
Theorem	bdsbc 15612	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 15613. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdsbcALT 15613	Alternate proof of bdsbc 15612. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdccsb 15614	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 A   =>    |- BOUNDED [_ y / x ]_ A
Theorem	bdcdif 15615	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A \ B )
Theorem	bdcun 15616	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A u. B )
Theorem	bdcin 15617	The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A i^i B )
Theorem	bdss 15618	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 A   =>    |- BOUNDED x C_ A
Theorem	bdcnul 15619	The empty class is bounded. See also bdcnulALT 15620. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED (/)
Theorem	bdcnulALT 15620	Alternate proof of bdcnul 15619. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 15598, or use the corresponding characterizations of its elements followed by bdelir 15601. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED (/)
Theorem	bdeq0 15621	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = (/)
Theorem	bj-bd0el 15622	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
Theorem	bdcpw 15623	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED ~P A
Theorem	bdcsn 15624	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x }
Theorem	bdcpr 15625	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y }
Theorem	bdctp 15626	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y , z }
Theorem	bdsnss 15627*	Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED { x } C_ A
Theorem	bdvsn 15628*	Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x = { y }
Theorem	bdop 15629	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <. x , y >.
Theorem	bdcuni 15630	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
|- BOUNDED U. x
Theorem	bdcint 15631	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED |^| x
Theorem	bdciun 15632*	The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED U_ x e. y A
Theorem	bdciin 15633*	The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED |^|_ x e. y A
Theorem	bdcsuc 15634	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED suc x
Theorem	bdeqsuc 15635*	Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = suc y
Theorem	bj-bdsucel 15636	Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED suc x e. y
Theorem	bdcriota 15637*	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
|- BOUNDED ph   &    |- E! x e. y ph   =>    |- BOUNDED ( iota_ x e. y ph )
13.2.9  CZF: Bounded separation In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.
Axiom	ax-bdsep 15638*	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 4152. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep1 15639*	Version of ax-bdsep 15638 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep2 15640*	Version of ax-bdsep 15638 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 15639 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnft 15641*	Closed form of bdsepnf 15642. Version of ax-bdsep 15638 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness antecedent, and without initial universal quantifier. Use bdsep1 15639 when sufficient. (Contributed by BJ, 19-Oct-2019.)
|- BOUNDED ph   =>    |- ( A. x F/ b ph -> E. b A. x ( x e. b <-> ( x e. a /\ ph ) ) )
Theorem	bdsepnf 15642*	Version of ax-bdsep 15638 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 15643. Use bdsep1 15639 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnfALT 15643*	Alternate proof of bdsepnf 15642, not using bdsepnft 15641. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdzfauscl 15644*	Closed form of the version of zfauscl 4154 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
|- BOUNDED ph   =>    |- ( A e. V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )
Theorem	bdbm1.3ii 15645*	Bounded version of bm1.3ii 4155. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	bj-axemptylem 15646*	Lemma for bj-axempty 15647 and bj-axempty2 15648. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4160 instead. (New usage is discouraged.)
|- E. x A. y ( y e. x -> F. )
Theorem	bj-axempty 15647*	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 4159. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4160 instead. (New usage is discouraged.)
|- E. x A. y e. x F.
Theorem	bj-axempty2 15648*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 15647. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4160 instead. (New usage is discouraged.)
|- E. x A. y -. y e. x
Theorem	bj-nalset 15649*	nalset 4164 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x A. y y e. x
Theorem	bj-vprc 15650	vprc 4166 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
Theorem	bj-nvel 15651	nvel 4167 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
Theorem	bj-vnex 15652	vnex 4165 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x x = _V
Theorem	bdinex1 15653	Bounded version of inex1 4168. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	bdinex2 15654	Bounded version of inex2 4169. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	bdinex1g 15655	Bounded version of inex1g 4170. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>    |- ( A e. V -> ( A i^i B ) e. _V )
Theorem	bdssex 15656	Bounded version of ssex 4171. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	bdssexi 15657	Bounded version of ssexi 4172. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	bdssexg 15658	Bounded version of ssexg 4173. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	bdssexd 15659	Bounded version of ssexd 4174. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   &    |- BOUNDED A   =>    |- ( ph -> A e. _V )
Theorem	bdrabexg 15660*	Bounded version of rabexg 4177. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- BOUNDED A   =>    |- ( A e. V -> { x e. A | ph } e. _V )
Theorem	bj-inex 15661	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A i^i B ) e. _V )
Theorem	bj-intexr 15662	intexr 4184 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	bj-intnexr 15663	intnexr 4185 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A = _V -> -. |^| A e. _V )
Theorem	bj-zfpair2 15664	Proof of zfpair2 4244 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- { x , y } e. _V
Theorem	bj-prexg 15665	Proof of prexg 4245 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
Theorem	bj-snexg 15666	snexg 4218 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( A e. V -> { A } e. _V )
Theorem	bj-snex 15667	snex 4219 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- { A } e. _V
Theorem	bj-sels 15668*	If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.)
|- ( A e. V -> E. x A e. x )
Theorem	bj-axun2 15669*	axun2 4471 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
Theorem	bj-uniex2 15670*	uniex2 4472 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y y = U. x
Theorem	bj-uniex 15671	uniex 4473 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- U. A e. _V
Theorem	bj-uniexg 15672	uniexg 4475 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> U. A e. _V )
Theorem	bj-unex 15673	unex 4477 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A u. B ) e. _V
Theorem	bdunexb 15674	Bounded version of unexb 4478. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
Theorem	bj-unexg 15675	unexg 4479 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
Theorem	bj-sucexg 15676	sucexg 4535 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> suc A e. _V )
Theorem	bj-sucex 15677	sucex 4536 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- suc A e. _V
13.2.9.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 15678	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
|- BOUNDED ph   =>    |- DECID ph
Theorem	bj-d0clsepcl 15679	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
|- DECID ph
13.2.9.2  Inductive classes and the class of natural number ordinals
Syntax	wind 15680	Syntax for inductive classes.
wff Ind A
Definition	df-bj-ind 15681*	Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
Theorem	bj-indsuc 15682	A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
|- (Ind A -> ( B e. A -> suc B e. A ) )
Theorem	bj-indeq 15683	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
|- ( A = B -> (Ind A <-> Ind B ) )
Theorem	bj-bdind 15684	Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED Ind x
Theorem	bj-indint 15685*	The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
|- Ind |^| { x e. A | Ind x }
Theorem	bj-indind 15686*	If A is inductive and B is "inductive in A", then ( A i^i B ) is inductive. (Contributed by BJ, 25-Oct-2020.)
|- ( (Ind A /\ ( (/) e. B /\ A. x e. A ( x e. B -> suc x e. B ) ) ) -> Ind ( A i^i B ) )
Theorem	bj-dfom 15687	Alternate definition of om, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
|- om = |^| { x | Ind x }
Theorem	bj-omind 15688	om is an inductive class. (Contributed by BJ, 30-Nov-2019.)
|- Ind om
Theorem	bj-omssind 15689	om 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.)
|- ( A e. V -> (Ind A -> om C_ A ) )
Theorem	bj-ssom 15690*	A characterization of subclasses of om. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- ( A. x (Ind x -> A C_ x ) <-> A C_ om )
Theorem	bj-om 15691*	A set is equal to om if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> ( A = om <-> (Ind A /\ A. x (Ind x -> A C_ x ) ) ) )
Theorem	bj-2inf 15692*	Two formulations of the axiom of infinity (see ax-infvn 15695 and bj-omex 15696) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
|- ( om e. _V <-> E. x (Ind x /\ A. y (Ind y -> x C_ y ) ) )
13.2.9.3  The first three Peano postulates The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4631 and peano3 4633 already show this. In this section, we prove bj-peano2 15693 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms.
Theorem	bj-peano2 15693	Constructive proof of peano2 4632. Temporary note: another possibility is to simply replace sucexg 4535 with bj-sucexg 15676 in the proof of peano2 4632. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. om -> suc A e. om )
Theorem	peano5set 15694*	Version of peano5 4635 when om i^i A 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.)
|- ( ( om i^i A ) e. V -> ( ( (/) e. A /\ A. x e. om ( x e. A -> suc x e. A ) ) -> om C_ A ) )
13.2.10  CZF: Infinity 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.
13.2.10.1  The set of natural number ordinals In this section, we introduce the axiom of infinity in a constructive setting (ax-infvn 15695) and deduce that the class om of natural number ordinals is a set (bj-omex 15696).
Axiom	ax-infvn 15695*	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 4625) from which one then proves, using full separation, that the wanted set exists (omex 4630). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.)
|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
Theorem	bj-omex 15696	Proof of omex 4630 from ax-infvn 15695. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.)
|- om e. _V
13.2.10.2  Peano's fifth postulate In this section, we give constructive proofs of two versions of Peano's fifth postulate.
Theorem	bdpeano5 15697*	Bounded version of peano5 4635. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( (/) e. A /\ A. x e. om ( x e. A -> suc x e. A ) ) -> om C_ A )
Theorem	speano5 15698*	Version of peano5 4635 when A 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.)
|- ( ( A e. V /\ (/) e. A /\ A. x e. om ( x e. A -> suc x e. A ) ) -> om C_ A )
13.2.10.3  Bounded induction and Peano's fourth postulate 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 15699*	Bounded induction (principle of induction when A is assumed to be a set) allowing a proof from basic constructive axioms. See find 4636 for a nonconstructive proof of the general case. See bdfind 15700 for a proof when A is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> ( ( A C_ om /\ (/) e. A /\ A. x e. A suc x e. A ) -> A = om ) )
Theorem	bdfind 15700*	Bounded induction (principle of induction when A is assumed to be bounded), proved from basic constructive axioms. See find 4636 for a nonconstructive proof of the general case. See findset 15699 for a proof when A is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( A C_ om /\ (/) e. A /\ A. x e. A suc x e. A ) -> A = om )