Home | Intuitionistic Logic Explorer Theorem List (p. 139 of 141) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bdceqir 13801 | A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13800) equality in the hypothesis, to work better with definitions (𝐵 is the definiendum that one wants to prove bounded; see comment of bd0r 13782). (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 & ⊢ 𝐵 = 𝐴 ⇒ ⊢ BOUNDED 𝐵 | ||
Theorem | bdel 13802* | The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.) |
⊢ (BOUNDED 𝐴 → BOUNDED 𝑥 ∈ 𝐴) | ||
Theorem | bdeli 13803* | Inference associated with bdel 13802. Its converse is bdelir 13804. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED 𝑥 ∈ 𝐴 | ||
Theorem | bdelir 13804* | Inference associated with df-bdc 13798. Its converse is bdeli 13803. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝑥 ∈ 𝐴 ⇒ ⊢ BOUNDED 𝐴 | ||
Theorem | bdcv 13805 | A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝑥 | ||
Theorem | bdcab 13806 | A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED {𝑥 ∣ 𝜑} | ||
Theorem | bdph 13807 | A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.) |
⊢ BOUNDED {𝑥 ∣ 𝜑} ⇒ ⊢ BOUNDED 𝜑 | ||
Theorem | bds 13808* | Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 13779; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 13779. (Contributed by BJ, 19-Nov-2019.) |
⊢ BOUNDED 𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ BOUNDED 𝜓 | ||
Theorem | bdcrab 13809* | A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | bdne 13810 | Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝑥 ≠ 𝑦 | ||
Theorem | bdnel 13811* | Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED 𝑥 ∉ 𝐴 | ||
Theorem | bdreu 13812* |
Boundedness of existential uniqueness.
Remark regarding restricted quantifiers: the formula ∀𝑥 ∈ 𝐴𝜑 need not be bounded even if 𝐴 and 𝜑 are. Indeed, V is bounded by bdcvv 13814, and ⊢ (∀𝑥 ∈ V𝜑 ↔ ∀𝑥𝜑) (in minimal propositional calculus), so by bd0 13781, if ∀𝑥 ∈ V𝜑 were bounded when 𝜑 is bounded, then ∀𝑥𝜑 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 ∃!𝑥 ∈ 𝑦 𝜑 | ||
Theorem | bdrmo 13813* | Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED ∃*𝑥 ∈ 𝑦 𝜑 | ||
Theorem | bdcvv 13814 | 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 13815 | A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 13816. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED [𝑦 / 𝑥]𝜑 | ||
Theorem | bdsbcALT 13816 | Alternate proof of bdsbc 13815. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED [𝑦 / 𝑥]𝜑 | ||
Theorem | bdccsb 13817 | 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 𝐴 ⇒ ⊢ BOUNDED ⦋𝑦 / 𝑥⦌𝐴 | ||
Theorem | bdcdif 13818 | The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝐵 ⇒ ⊢ BOUNDED (𝐴 ∖ 𝐵) | ||
Theorem | bdcun 13819 | The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝐵 ⇒ ⊢ BOUNDED (𝐴 ∪ 𝐵) | ||
Theorem | bdcin 13820 | The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝐵 ⇒ ⊢ BOUNDED (𝐴 ∩ 𝐵) | ||
Theorem | bdss 13821 | 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 𝐴 ⇒ ⊢ BOUNDED 𝑥 ⊆ 𝐴 | ||
Theorem | bdcnul 13822 | The empty class is bounded. See also bdcnulALT 13823. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED ∅ | ||
Theorem | bdcnulALT 13823 | Alternate proof of bdcnul 13822. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 13801, or use the corresponding characterizations of its elements followed by bdelir 13804. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ BOUNDED ∅ | ||
Theorem | bdeq0 13824 | Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.) |
⊢ BOUNDED 𝑥 = ∅ | ||
Theorem | bj-bd0el 13825 | Boundedness of the formula "the empty set belongs to the setvar 𝑥". (Contributed by BJ, 30-Nov-2019.) |
⊢ BOUNDED ∅ ∈ 𝑥 | ||
Theorem | bdcpw 13826 | The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED 𝒫 𝐴 | ||
Theorem | bdcsn 13827 | The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED {𝑥} | ||
Theorem | bdcpr 13828 | The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED {𝑥, 𝑦} | ||
Theorem | bdctp 13829 | The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED {𝑥, 𝑦, 𝑧} | ||
Theorem | bdsnss 13830* | Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED {𝑥} ⊆ 𝐴 | ||
Theorem | bdvsn 13831* | Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝑥 = {𝑦} | ||
Theorem | bdop 13832 | The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.) |
⊢ BOUNDED 〈𝑥, 𝑦〉 | ||
Theorem | bdcuni 13833 | The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.) |
⊢ BOUNDED ∪ 𝑥 | ||
Theorem | bdcint 13834 | The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED ∩ 𝑥 | ||
Theorem | bdciun 13835* | The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED ∪ 𝑥 ∈ 𝑦 𝐴 | ||
Theorem | bdciin 13836* | The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED ∩ 𝑥 ∈ 𝑦 𝐴 | ||
Theorem | bdcsuc 13837 | The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.) |
⊢ BOUNDED suc 𝑥 | ||
Theorem | bdeqsuc 13838* | Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.) |
⊢ BOUNDED 𝑥 = suc 𝑦 | ||
Theorem | bj-bdsucel 13839 | Boundedness of the formula "the successor of the setvar 𝑥 belongs to the setvar 𝑦". (Contributed by BJ, 30-Nov-2019.) |
⊢ BOUNDED suc 𝑥 ∈ 𝑦 | ||
Theorem | bdcriota 13840* | A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.) |
⊢ BOUNDED 𝜑 & ⊢ ∃!𝑥 ∈ 𝑦 𝜑 ⇒ ⊢ BOUNDED (℩𝑥 ∈ 𝑦 𝜑) | ||
In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory. | ||
Axiom | ax-bdsep 13841* | 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 4105. (Contributed by BJ, 5-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) | ||
Theorem | bdsep1 13842* | Version of ax-bdsep 13841 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) | ||
Theorem | bdsep2 13843* | Version of ax-bdsep 13841 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 13842 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) | ||
Theorem | bdsepnft 13844* | Closed form of bdsepnf 13845. Version of ax-bdsep 13841 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness antecedent, and without initial universal quantifier. Use bdsep1 13842 when sufficient. (Contributed by BJ, 19-Oct-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ (∀𝑥Ⅎ𝑏𝜑 → ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))) | ||
Theorem | bdsepnf 13845* | Version of ax-bdsep 13841 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 13846. Use bdsep1 13842 when sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ Ⅎ𝑏𝜑 & ⊢ BOUNDED 𝜑 ⇒ ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) | ||
Theorem | bdsepnfALT 13846* | Alternate proof of bdsepnf 13845, not using bdsepnft 13844. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑏𝜑 & ⊢ BOUNDED 𝜑 ⇒ ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) | ||
Theorem | bdzfauscl 13847* | Closed form of the version of zfauscl 4107 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Theorem | bdbm1.3ii 13848* | Bounded version of bm1.3ii 4108. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ⇒ ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) | ||
Theorem | bj-axemptylem 13849* | Lemma for bj-axempty 13850 and bj-axempty2 13851. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4113 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 → ⊥) | ||
Theorem | bj-axempty 13850* | 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 4112. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4113 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦 ∈ 𝑥 ⊥ | ||
Theorem | bj-axempty2 13851* | Axiom of the empty set from bounded separation, alternate version to bj-axempty 13850. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4113 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
Theorem | bj-nalset 13852* | nalset 4117 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥 | ||
Theorem | bj-vprc 13853 | vprc 4119 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ ¬ V ∈ V | ||
Theorem | bj-nvel 13854 | nvel 4120 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ ¬ V ∈ 𝐴 | ||
Theorem | bj-vnex 13855 | vnex 4118 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑥 𝑥 = V | ||
Theorem | bdinex1 13856 | Bounded version of inex1 4121. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐵 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ V | ||
Theorem | bdinex2 13857 | Bounded version of inex2 4122. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐵 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∩ 𝐴) ∈ V | ||
Theorem | bdinex1g 13858 | Bounded version of inex1g 4123. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | bdssex 13859 | Bounded version of ssex 4124. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) | ||
Theorem | bdssexi 13860 | Bounded version of ssexi 4125. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | bdssexg 13861 | Bounded version of ssexg 4126. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | bdssexd 13862 | Bounded version of ssexd 4127. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ BOUNDED 𝐴 ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | bdrabexg 13863* | Bounded version of rabexg 4130. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ BOUNDED 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | bj-inex 13864 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | bj-intexr 13865 | intexr 4134 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) | ||
Theorem | bj-intnexr 13866 | intnexr 4135 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V) | ||
Theorem | bj-zfpair2 13867 | Proof of zfpair2 4193 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | bj-prexg 13868 | Proof of prexg 4194 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | bj-snexg 13869 | snexg 4168 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | bj-snex 13870 | snex 4169 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ∈ V | ||
Theorem | bj-sels 13871* | 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 13872* | axun2 4418 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) | ||
Theorem | bj-uniex2 13873* | uniex2 4419 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | bj-uniex 13874 | uniex 4420 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | bj-uniexg 13875 | uniexg 4422 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | bj-unex 13876 | unex 4424 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | bdunexb 13877 | Bounded version of unexb 4425. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝐵 ⇒ ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-unexg 13878 | unexg 4426 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-sucexg 13879 | sucexg 4480 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | bj-sucex 13880 | sucex 4481 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Axiom | ax-bj-d0cl 13881 | Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ DECID 𝜑 | ||
Theorem | bj-d0clsepcl 13882 | Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) |
⊢ DECID 𝜑 | ||
Syntax | wind 13883 | Syntax for inductive classes. |
wff Ind 𝐴 | ||
Definition | df-bj-ind 13884* | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) |
⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | bj-indsuc 13885 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) |
⊢ (Ind 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) | ||
Theorem | bj-indeq 13886 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (Ind 𝐴 ↔ Ind 𝐵)) | ||
Theorem | bj-bdind 13887 | Boundedness of the formula "the setvar 𝑥 is an inductive class". (Contributed by BJ, 30-Nov-2019.) |
⊢ BOUNDED Ind 𝑥 | ||
Theorem | bj-indint 13888* | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) |
⊢ Ind ∩ {𝑥 ∈ 𝐴 ∣ Ind 𝑥} | ||
Theorem | bj-indind 13889* | If 𝐴 is inductive and 𝐵 is "inductive in 𝐴", then (𝐴 ∩ 𝐵) is inductive. (Contributed by BJ, 25-Oct-2020.) |
⊢ ((Ind 𝐴 ∧ (∅ ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → suc 𝑥 ∈ 𝐵))) → Ind (𝐴 ∩ 𝐵)) | ||
Theorem | bj-dfom 13890 | Alternate definition of ω, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.) |
⊢ ω = ∩ {𝑥 ∣ Ind 𝑥} | ||
Theorem | bj-omind 13891 | ω is an inductive class. (Contributed by BJ, 30-Nov-2019.) |
⊢ Ind ω | ||
Theorem | bj-omssind 13892 | ω 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.) |
⊢ (𝐴 ∈ 𝑉 → (Ind 𝐴 → ω ⊆ 𝐴)) | ||
Theorem | bj-ssom 13893* | A characterization of subclasses of ω. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(Ind 𝑥 → 𝐴 ⊆ 𝑥) ↔ 𝐴 ⊆ ω) | ||
Theorem | bj-om 13894* | 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.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ω ↔ (Ind 𝐴 ∧ ∀𝑥(Ind 𝑥 → 𝐴 ⊆ 𝑥)))) | ||
Theorem | bj-2inf 13895* | Two formulations of the axiom of infinity (see ax-infvn 13898 and bj-omex 13899) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (ω ∈ V ↔ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))) | ||
The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4576 and peano3 4578 already show this. In this section, we prove bj-peano2 13896 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms. | ||
Theorem | bj-peano2 13896 | Constructive proof of peano2 4577. Temporary note: another possibility is to simply replace sucexg 4480 with bj-sucexg 13879 in the proof of peano2 4577. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) | ||
Theorem | peano5set 13897* | Version of peano5 4580 when ω ∩ 𝐴 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.) |
⊢ ((ω ∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)) | ||
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 13898) and deduce that the class ω of natural number ordinals is a set (bj-omex 13899). | ||
Axiom | ax-infvn 13898* | 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 4570) from which one then proves, using full separation, that the wanted set exists (omex 4575). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.) |
⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) | ||
Theorem | bj-omex 13899 | Proof of omex 4575 from ax-infvn 13898. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) |
⊢ ω ∈ V | ||
In this section, we give constructive proofs of two versions of Peano's fifth postulate. | ||
Theorem | bdpeano5 13900* | Bounded version of peano5 4580. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |