P. 94 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9301-9400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bdeli 9301*	Inference associated with bdel 9300. Its converse is bdelir 9302. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>   |- BOUNDED x e. A
Theorem	bdelir 9302*	Inference associated with df-bdc 9296. Its converse is bdeli 9301. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x e. A   =>   |- BOUNDED A
Theorem	bdcv 9303	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x
Theorem	bdcab 9304	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 9305	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 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 ph   &   |- (x = y -> (ph <-> ps))   =>   |- BOUNDED ps
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 A   &   |- BOUNDED ph   =>   |- BOUNDED {x e. A | ph }
Theorem	bdne 9308	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x =/= y
Theorem	bdnel 9309*	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 9310*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula A.x e. Aph need not be bounded even if A and ph are. Indeed, _V is bounded by bdcvv 9312, and |- (A.x e. _Vph <-> A.xph) (in minimal propositional calculus), so by bd0 9279, if A.x e. _Vph were bounded when ph is bounded, then A.xph 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 9311*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>   |- BOUNDED E*x e. y ph
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 _V
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 ph   =>   |- BOUNDED [.y / x ].ph
Theorem	bdsbcALT 9314	Alternate proof of bdsbc 9313. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED ph   =>   |- BOUNDED [.y / x ].ph
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 A   =>   |- BOUNDED [_y / x ]_A
Theorem	bdcdif 9316	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &   |- BOUNDED B   =>   |- BOUNDED (A \ B)
Theorem	bdcun 9317	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &   |- BOUNDED B   =>   |- BOUNDED (A u. B)
Theorem	bdcin 9318	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 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 A   =>   |- BOUNDED x C_ A
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 x = (/)
Theorem	bj-bd0el 9323	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
Theorem	bdcpw 9324	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>   |- BOUNDED ~PA
Theorem	bdcsn 9325	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED {x }
Theorem	bdcpr 9326	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED {x , y }
Theorem	bdctp 9327	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED {x , y , z }
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 A   =>   |- BOUNDED {x } C_ A
Theorem	bdvsn 9329*	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 9330	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <.x , y >.
Theorem	bdcuni 9331	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
|- BOUNDED U.x
Theorem	bdcint 9332	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED |^|x
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 A   =>   |- BOUNDED U_x e. y A
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 A   =>   |- BOUNDED |^|_x e. y A
Theorem	bdcsuc 9335	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED suc x
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 x = suc y
Theorem	bj-bdsucel 9337	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 9338*	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)
5.3.6  Bounded separation 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 ph   =>   |- A. aE. bA.x(x e. b <-> (x e. a /\ ph))
Theorem	bdsep1 9340*	Version of ax-bdsep 9339 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>   |- E. bA.x(x e. b <-> (x e. a /\ ph))
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 ph   =>   |- E. bA.x(x e. b <-> (x e. a /\ ph))
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 ph   =>   |- (A.x F/ bph -> E. bA.x(x e. b <-> (x e. a /\ ph)))
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.)
|- F/ bph   &   |- BOUNDED ph   =>   |- E. bA.x(x e. b <-> (x e. a /\ ph))
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.)
|- F/ bph   &   |- BOUNDED ph   =>   |- E. bA.x(x e. b <-> (x e. a /\ ph))
Theorem	bdzfauscl 9345*	Closed form of the version of zfauscl 3868 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
|- BOUNDED ph   =>   |- (A e. V -> E.yA.x(x e. y <-> (x e. A /\ ph)))
Theorem	bdbm1.3ii 9346*	Bounded version of bm1.3ii 3869. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &   |- E.xA.y(ph -> y e. x)   =>   |- E.xA.y(y e. x <-> ph)
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.)
|- E.xA.y(y e. x -> F. )
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.)
|- E.xA.y e. x F.
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.)
|- E.xA.y -. y e. x
Theorem	bj-nalset 9350*	nalset 3878 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E.xA.y y e. x
Theorem	bj-vprc 9351	vprc 3879 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
Theorem	bj-nvel 9352	nvel 3880 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
Theorem	bj-vnex 9353	vnex 3881 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E.x x = _V
Theorem	bdinex1 9354	Bounded version of inex1 3882. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &   |- A e. _V   =>   |- (A i^i B) e. _V
Theorem	bdinex2 9355	Bounded version of inex2 3883. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &   |- A e. _V   =>   |- (B i^i A) e. _V
Theorem	bdinex1g 9356	Bounded version of inex1g 3884. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>   |- (A e. V -> (A i^i B) e. _V)
Theorem	bdssex 9357	Bounded version of ssex 3885. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- B e. _V   =>   |- (A C_ B -> A e. _V)
Theorem	bdssexi 9358	Bounded version of ssexi 3886. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &   |- B e. _V   &   |- A C_ B   =>   |- A e. _V
Theorem	bdssexg 9359	Bounded version of ssexg 3887. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>   |- ((A C_ B /\ B e. C) -> A e. _V)
Theorem	bdssexd 9360	Bounded version of ssexd 3888. (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 9361*	Bounded version of rabexg 3891. (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 9362	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 9363	intexr 3895 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^|A e. _V -> A =/= (/))
Theorem	bj-intnexr 9364	intnexr 3896 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^|A = _V -> -. |^|A e. _V)
Theorem	bj-zfpair2 9365	Proof of zfpair2 3936 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- {x , y } e. _V
Theorem	bj-prexg 9366	Proof of prexg 3938 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 9367	snexg 3927 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- (A e. V -> {A } e. _V)
Theorem	bj-snex 9368	snex 3928 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   =>   |- {A } e. _V
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.)
|- (A e. V -> E.x A e. x)
Theorem	bj-axun2 9370*	axun2 4138 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E.yA.z(z e. y <-> E.w(z e. w /\ w e. x))
Theorem	bj-uniex2 9371*	uniex2 4139 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E.y y = U.x
Theorem	bj-uniex 9372	uniex 4140 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>   |- U.A e. _V
Theorem	bj-uniexg 9373	uniexg 4141 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> U.A e. _V)
Theorem	bj-unex 9374	unex 4142 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 9375	Bounded version of unexb 4143. (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 9376	unexg 4144 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 9377	sucexg 4190 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- (A e. V -> suc A e. _V)
Theorem	bj-sucex 9378	sucex 4191 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>   |- suc A e. _V
5.3.6.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 9379	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
|- BOUNDED ph   =>   |- DECID ph
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.)
|- ((ph <-> ps) -> (-. ph <-> -. ps))
Theorem	bj-notbii 9381	Inference associated with bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
|- (ph <-> ps)   =>   |- (-. ph <-> -. ps)
Theorem	bj-notbid 9382	Deduction form of bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (-. ps <-> -. ch))
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.)
|- ((ph <-> ps) -> (DECID ph <-> DECID ps))
Theorem	bj-d0clsepcl 9384	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
|- DECID ph
5.3.6.2  Inductive classes and the class of natural numbers (finite ordinals)
Syntax	wind 9385	Syntax for inductive classes.
wff Ind A
Definition	df-bj-ind 9386*	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 9387	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 9388	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
|- (A = B -> (Ind A <-> Ind B))
Theorem	bj-bdind 9389	Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED Ind x
Theorem	bj-indint 9390*	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 9391*	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 9392	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 9393	om is an inductive class. (Contributed by BJ, 30-Nov-2019.)
|- Ind om
Theorem	bj-omssind 9394	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 9395*	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 9396*	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 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.)
|- ( om e. _V <-> E.x(Ind x /\ A.y(Ind y -> x C_ y)))
5.3.6.3  The first three Peano postulates 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.)
|- (A e. om -> suc A e. om)
Theorem	peano5set 9399*	Version of peano5 4264 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))
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.)
|- (( om i^i A) e. V -> (( (/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om C_ A))