 Home Intuitionistic Logic ExplorerTheorem List (p. 94 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

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

Theorembdeli 9301* Inference associated with bdel 9300. Its converse is bdelir 9302. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A       BOUNDED x A

Theorembdelir 9302* Inference associated with df-bdc 9296. Its converse is bdeli 9301. (Contributed by BJ, 3-Oct-2019.)
BOUNDED x A       BOUNDED A

Theorembdcv 9303 A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
BOUNDED x

Theorembdcab 9304 A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
BOUNDED φ       BOUNDED {xφ}

Theorembdph 9305 A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
BOUNDED {xφ}       BOUNDED φ

Theorembds 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 φ    &   (x = y → (φψ))       BOUNDED ψ

Theorembdcrab 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 φ       BOUNDED {x Aφ}

Theorembdne 9308 Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED xy

Theorembdnel 9309* Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED xA

Theorembdreu 9310* Boundedness of existential uniqueness.

Remark regarding restricted quantifiers: the formula x Aφ need not be bounded even if A and φ are. Indeed, V is bounded by bdcvv 9312, and (x Vφxφ) (in minimal propositional calculus), so by bd0 9279, if x Vφ were bounded when φ is bounded, then xφ would be bounded as well when φ is bounded, which is not the case. The same remark holds with , ∃!, ∃*. (Contributed by BJ, 16-Oct-2019.)

BOUNDED φ       BOUNDED ∃!x y φ

Theorembdrmo 9311* Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
BOUNDED φ       BOUNDED ∃*x y φ

Theorembdcvv 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

Theorembdsbc 9313 A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 9314. (Contributed by BJ, 16-Oct-2019.)
BOUNDED φ       BOUNDED [y / x]φ

TheorembdsbcALT 9314 Alternate proof of bdsbc 9313. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
BOUNDED φ       BOUNDED [y / x]φ

Theorembdccsb 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 / xA

Theorembdcdif 9316 The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

Theorembdcun 9317 The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

Theorembdcin 9318 The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

Theorembdss 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 xA

Theorembdcnul 9320 The empty class is bounded. See also bdcnulALT 9321. (Contributed by BJ, 3-Oct-2019.)
BOUNDED

TheorembdcnulALT 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

Theorembdeq0 9322 Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = ∅

Theorembj-bd0el 9323 Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
BOUNDED x

Theorembdcpw 9324 The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A       BOUNDED 𝒫 A

Theorembdcsn 9325 The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x}

Theorembdcpr 9326 The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x, y}

Theorembdctp 9327 The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x, y, z}

Theorembdsnss 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} ⊆ A

Theorembdvsn 9329* Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED x = {y}

Theorembdop 9330 The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
BOUNDEDx, y

Theorembdcuni 9331 The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
BOUNDED x

Theorembdcint 9332 The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED x

Theorembdciun 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 x y A

Theorembdciin 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 y A

Theorembdcsuc 9335 The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED suc x

Theorembdeqsuc 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

Theorembj-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 y

Theorembdcriota 9338* A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
BOUNDED φ    &   ∃!x y φ       BOUNDED (x y φ)

5.3.6  Bounded separation

In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.

Axiomax-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 φ       𝑎𝑏x(x 𝑏 ↔ (x 𝑎 φ))

Theorembdsep1 9340* Version of ax-bdsep 9339 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

Theorembdsep2 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 φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

Theorembdsepnft 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 φ       (x𝑏φ𝑏x(x 𝑏 ↔ (x 𝑎 φ)))

Theorembdsepnf 9343* Version of ax-bdsep 9339 with one DV condition removed, the other DV condition replaced by a non-freeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 9344. Use bdsep1 9340 when sufficient. (Contributed by BJ, 5-Oct-2019.)
𝑏φ    &   BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

TheorembdsepnfALT 9344* Alternate proof of bdsepnf 9343, not using bdsepnft 9342. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝑏φ    &   BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

Theorembdzfauscl 9345* Closed form of the version of zfauscl 3868 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
BOUNDED φ       (A 𝑉yx(x y ↔ (x A φ)))

Theorembdbm1.3ii 9346* Bounded version of bm1.3ii 3869. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xy(φy x)       xy(y xφ)

Theorembj-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.)
xy(y x → ⊥ )

Theorembj-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.)
xy x

Theorembj-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.)
xy ¬ y x

Theorembj-nalset 9350* nalset 3878 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ xy y x

Theorembj-vprc 9351 vprc 3879 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V V

Theorembj-nvel 9352 nvel 3880 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V A

Theorembj-vnex 9353 vnex 3881 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ x x = V

Theorembdinex1 9354 Bounded version of inex1 3882. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B    &   A V       (AB) V

Theorembdinex2 9355 Bounded version of inex2 3883. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B    &   A V       (BA) V

Theorembdinex1g 9356 Bounded version of inex1g 3884. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B       (A 𝑉 → (AB) V)

Theorembdssex 9357 Bounded version of ssex 3885. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   B V       (ABA V)

Theorembdssexi 9358 Bounded version of ssexi 3886. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   B V    &   AB       A V

Theorembdssexg 9359 Bounded version of ssexg 3887. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A       ((AB B 𝐶) → A V)

Theorembdssexd 9360 Bounded version of ssexd 3888. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(φB 𝐶)    &   (φAB)    &   BOUNDED A       (φA V)

Theorembdrabexg 9361* Bounded version of rabexg 3891. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   BOUNDED A       (A 𝑉 → {x Aφ} V)

Theorembj-inex 9362 The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
((A 𝑉 B 𝑊) → (AB) V)

Theorembj-intexr 9363 intexr 3895 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( A V → A ≠ ∅)

Theorembj-intnexr 9364 intnexr 3896 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( A = V → ¬ A V)

Theorembj-zfpair2 9365 Proof of zfpair2 3936 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
{x, y} V

Theorembj-prexg 9366 Proof of prexg 3938 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
((A 𝑉 B 𝑊) → {A, B} V)

Theorembj-snexg 9367 snexg 3927 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
(A 𝑉 → {A} V)

Theorembj-snex 9368 snex 3928 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
A V       {A} V

Theorembj-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 𝑉x A x)

Theorembj-axun2 9370* axun2 4138 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
yz(z yw(z w w x))

Theorembj-uniex2 9371* uniex2 4139 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
y y = x

Theorembj-uniex 9372 uniex 4140 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V        A V

Theorembj-uniexg 9373 uniexg 4141 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 A V)

Theorembj-unex 9374 unex 4142 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V    &   B V       (AB) V

Theorembdunexb 9375 Bounded version of unexb 4143. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   BOUNDED B       ((A V B V) ↔ (AB) V)

Theorembj-unexg 9376 unexg 4144 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
((A 𝑉 B 𝑊) → (AB) V)

Theorembj-sucexg 9377 sucexg 4190 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → suc A V)

Theorembj-sucex 9378 sucex 4191 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V       suc A V

5.3.6.1  Delta_0-classical logic

Axiomax-bj-d0cl 9379 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED φ       DECID φ

Theorembj-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.)
((φψ) → (¬ φ ↔ ¬ ψ))

Theorembj-notbii 9381 Inference associated with bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
(φψ)       φ ↔ ¬ ψ)

Theorembj-notbid 9382 Deduction form of bj-notbi 9380. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
(φ → (ψχ))       (φ → (¬ ψ ↔ ¬ χ))

Theorembj-dcbi 9383 Equivalence property for DECID. TODO: solve conflict with dcbi 843; minimize dcbii 746 and dcbid 747 with it, as well as theorems using those. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
((φψ) → (DECID φDECID ψ))

Theorembj-d0clsepcl 9384 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
DECID φ

5.3.6.2  Inductive classes and the class of natural numbers (finite ordinals)

Syntaxwind 9385 Syntax for inductive classes.
wff Ind A

Definitiondf-bj-ind 9386* Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
(Ind A ↔ (∅ A x A suc x A))

Theorembj-indsuc 9387 A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
(Ind A → (B A → suc B A))

Theorembj-indeq 9388 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
(A = B → (Ind A ↔ Ind B))

Theorembj-bdind 9389 Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
BOUNDED Ind x

Theorembj-indint 9390* The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
Ind {x A ∣ Ind x}

Theorembj-indind 9391* If A is inductive and B is "inductive in A", then (AB) is inductive. (Contributed by BJ, 25-Oct-2020.)
((Ind A (∅ B x A (x B → suc x B))) → Ind (AB))

Theorembj-dfom 9392 Alternate definition of 𝜔, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
𝜔 = {x ∣ Ind x}

Theorembj-omind 9393 𝜔 is an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind 𝜔

Theorembj-omssind 9394 𝜔 is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → (Ind A → 𝜔 ⊆ A))

Theorembj-ssom 9395* A characterization of subclasses of 𝜔. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(x(Ind xAx) ↔ A ⊆ 𝜔)

Theorembj-om 9396* A set is equal to 𝜔 if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → (A = 𝜔 ↔ (Ind A x(Ind xAx))))

Theorembj-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.)
(𝜔 V ↔ x(Ind x y(Ind yxy)))

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.

Theorembj-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 𝜔 → suc A 𝜔)

Theorempeano5set 9399* Version of peano5 4264 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) 𝑉 → ((∅ A x 𝜔 (x A → suc x A)) → 𝜔 ⊆ A))

Theorempeano5setOLD 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.)
((𝜔 ∩ A) 𝑉 → ((∅ A x 𝜔 (x A → suc x A)) → 𝜔 ⊆ A))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9457
 Copyright terms: Public domain < Previous  Next >