P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bdtru 13201	The truth value T. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED T.
Theorem	bdfal 13202	The truth value F. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED F.
Theorem	bdnth 13203	A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdnthALT 13204	Alternate proof of bdnth 13203 not using bdfal 13202. Then, bdfal 13202 can be proved from this theorem, using fal 1339. The total number of proof steps would be 17 (for bdnthALT 13204) + 3 = 20, which is more than 8 (for bdfal 13202) + 9 (for bdnth 13203) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdxor 13205	The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/_ ps )
Theorem	bj-bdcel 13206*	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
|- BOUNDED y = A   =>    |- BOUNDED A e. x
Theorem	bdab 13207	Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED x e. { y | ph }
Theorem	bdcdeq 13208	Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED CondEq ( x = y -> ph )
11.2.7.2  Bounded classes 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 13210. 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 13244), one can prove the boundedness of any concrete term using only setvars and bounded formulas, for instance, |- BOUNDED ph => |- BOUNDED <. { x | ph } , ( { y , suc z } X. <. t , (/) >. ) >.. 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 A => |- BOUNDED { A }.
Syntax	wbdc 13209	Syntax for the predicate BOUNDED.
wff BOUNDED A
Definition	df-bdc 13210*	Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A <-> A. xBOUNDED x e. A )
Theorem	bdceq 13211	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
|- A = B   =>    |- (BOUNDED A <-> BOUNDED B )
Theorem	bdceqi 13212	A class equal to a bounded one is bounded. Note the use of ax-ext 2122. See also bdceqir 13213. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- A = B   =>    |- BOUNDED B
Theorem	bdceqir 13213	A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13212) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 13194). (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- B = A   =>    |- BOUNDED B
Theorem	bdel 13214*	The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A -> BOUNDED x e. A )
Theorem	bdeli 13215*	Inference associated with bdel 13214. Its converse is bdelir 13216. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e. A
Theorem	bdelir 13216*	Inference associated with df-bdc 13210. Its converse is bdeli 13215. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x e. A   =>    |- BOUNDED A
Theorem	bdcv 13217	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x
Theorem	bdcab 13218	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 13219	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 13220*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 13191; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 13191. (Contributed by BJ, 19-Nov-2019.)
|- BOUNDED ph   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- BOUNDED ps
Theorem	bdcrab 13221*	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 13222	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x =/= y
Theorem	bdnel 13223*	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 13224*	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 13226, and |- ( A. x e. _V ph <-> A. x ph ) (in minimal propositional calculus), so by bd0 13193, 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 13225*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E* x e. y ph
Theorem	bdcvv 13226	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 13227	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 13228. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdsbcALT 13228	Alternate proof of bdsbc 13227. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdccsb 13229	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 13230	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A \ B )
Theorem	bdcun 13231	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A u. B )
Theorem	bdcin 13232	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 13233	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 13234	The empty class is bounded. See also bdcnulALT 13235. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED (/)
Theorem	bdcnulALT 13235	Alternate proof of bdcnul 13234. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 13213, or use the corresponding characterizations of its elements followed by bdelir 13216. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED (/)
Theorem	bdeq0 13236	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 13237	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
Theorem	bdcpw 13238	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED ~P A
Theorem	bdcsn 13239	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x }
Theorem	bdcpr 13240	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y }
Theorem	bdctp 13241	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y , z }
Theorem	bdsnss 13242*	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 13243*	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 13244	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <. x , y >.
Theorem	bdcuni 13245	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
|- BOUNDED U. x
Theorem	bdcint 13246	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED |^| x
Theorem	bdciun 13247*	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 13248*	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 13249	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED suc x
Theorem	bdeqsuc 13250*	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 13251	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 13252*	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 )
11.2.8  CZF: Bounded separation In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.
Axiom	ax-bdsep 13253*	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 4054. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep1 13254*	Version of ax-bdsep 13253 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 13255*	Version of ax-bdsep 13253 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 13254 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnft 13256*	Closed form of bdsepnf 13257. Version of ax-bdsep 13253 with one disjoint variable condition removed, the other disjoint variable condition replaced by a non-freeness antecedent, and without initial universal quantifier. Use bdsep1 13254 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 13257*	Version of ax-bdsep 13253 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 13258. Use bdsep1 13254 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 13258*	Alternate proof of bdsepnf 13257, not using bdsepnft 13256. (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 13259*	Closed form of the version of zfauscl 4056 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 13260*	Bounded version of bm1.3ii 4057. (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 13261*	Lemma for bj-axempty 13262 and bj-axempty2 13263. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4062 instead. (New usage is discouraged.)
|- E. x A. y ( y e. x -> F. )
Theorem	bj-axempty 13262*	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 4061. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4062 instead. (New usage is discouraged.)
|- E. x A. y e. x F.
Theorem	bj-axempty2 13263*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 13262. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4062 instead. (New usage is discouraged.)
|- E. x A. y -. y e. x
Theorem	bj-nalset 13264*	nalset 4066 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x A. y y e. x
Theorem	bj-vprc 13265	vprc 4068 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
Theorem	bj-nvel 13266	nvel 4069 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
Theorem	bj-vnex 13267	vnex 4067 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x x = _V
Theorem	bdinex1 13268	Bounded version of inex1 4070. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	bdinex2 13269	Bounded version of inex2 4071. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	bdinex1g 13270	Bounded version of inex1g 4072. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>    |- ( A e. V -> ( A i^i B ) e. _V )
Theorem	bdssex 13271	Bounded version of ssex 4073. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	bdssexi 13272	Bounded version of ssexi 4074. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	bdssexg 13273	Bounded version of ssexg 4075. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	bdssexd 13274	Bounded version of ssexd 4076. (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 13275*	Bounded version of rabexg 4079. (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 13276	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 13277	intexr 4083 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	bj-intnexr 13278	intnexr 4084 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A = _V -> -. |^| A e. _V )
Theorem	bj-zfpair2 13279	Proof of zfpair2 4140 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- { x , y } e. _V
Theorem	bj-prexg 13280	Proof of prexg 4141 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 13281	snexg 4116 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( A e. V -> { A } e. _V )
Theorem	bj-snex 13282	snex 4117 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- { A } e. _V
Theorem	bj-sels 13283*	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 13284*	axun2 4365 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 13285*	uniex2 4366 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y y = U. x
Theorem	bj-uniex 13286	uniex 4367 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- U. A e. _V
Theorem	bj-uniexg 13287	uniexg 4369 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> U. A e. _V )
Theorem	bj-unex 13288	unex 4370 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 13289	Bounded version of unexb 4371. (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 13290	unexg 4372 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 13291	sucexg 4422 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> suc A e. _V )
Theorem	bj-sucex 13292	sucex 4423 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- suc A e. _V
11.2.8.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 13293	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
|- BOUNDED ph   =>    |- DECID ph
Theorem	bj-d0clsepcl 13294	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
|- DECID ph
11.2.8.2  Inductive classes and the class of natural numbers (finite ordinals)
Syntax	wind 13295	Syntax for inductive classes.
wff Ind A
Definition	df-bj-ind 13296*	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 13297	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 13298	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
|- ( A = B -> (Ind A <-> Ind B ) )
Theorem	bj-bdind 13299	Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED Ind x
Theorem	bj-indint 13300*	The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
|- Ind |^| { x e. A | Ind x }