Home | Intuitionistic Logic Explorer Theorem List (p. 133 of 133) | < Previous Wrap > |
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 | bj-inf2vnlem4 13201* | Lemma for bj-inf2vn2 13203. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → 𝐴 ⊆ 𝑍)) | ||
Theorem | bj-inf2vn 13202* | A sufficient condition for ω to be a set. See bj-inf2vn2 13203 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω)) | ||
Theorem | bj-inf2vn2 13203* | A sufficient condition for ω to be a set; unbounded version of bj-inf2vn 13202. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω)) | ||
Axiom | ax-inf2 13204* | Another axiom of infinity in a constructive setting (see ax-infvn 13169). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.) |
⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦)) | ||
Theorem | bj-omex2 13205 | Using bounded set induction and the strong axiom of infinity, ω is a set, that is, we recover ax-infvn 13169 (see bj-2inf 13166 for the equivalence of the latter with bj-omex 13170). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ω ∈ V | ||
Theorem | bj-nn0sucALT 13206* | Alternate proof of bj-nn0suc 13192, also constructive but from ax-inf2 13204, hence requiring ax-bdsetind 13196. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
In this section, using the axiom of set induction, we prove full induction on the set of natural numbers. | ||
Theorem | bj-findis 13207* | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 13175 for a bounded version not requiring ax-setind 4452. See finds 4514 for a proof in IZF. From this version, it is easy to prove of finds 4514, finds2 4515, finds1 4516. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) | ||
Theorem | bj-findisg 13208* | Version of bj-findis 13207 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 13207 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜏 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜏)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → (𝐴 ∈ ω → 𝜏)) | ||
Theorem | bj-findes 13209 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 13207 for explanations. From this version, it is easy to prove findes 4517. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ (([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑 → [suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑) | ||
In this section, we state the axiom scheme of strong collection, which is part of CZF set theory. | ||
Axiom | ax-strcoll 13210* | Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcoll2 13211* | Version of ax-strcoll 13210 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcollnft 13212* | Closed form of strcollnf 13213. Version of ax-strcoll 13210 with one disjoint variable condition removed, the other disjoint variable condition replaced with a non-freeness antecedent, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.) |
⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))) | ||
Theorem | strcollnf 13213* | Version of ax-strcoll 13210 with one disjoint variable condition removed, the other disjoint variable condition replaced with a non-freeness hypothesis, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcollnfALT 13214* | Alternate proof of strcollnf 13213, not using strcollnft 13212. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
In this section, we state the axiom scheme of subset collection, which is part of CZF set theory. | ||
Axiom | ax-sscoll 13215* | Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | sscoll2 13216* | Version of ax-sscoll 13215 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Axiom | ax-ddkcomp 13217 | Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 13217 should be used in place of construction specific results. In particular, axcaucvg 7715 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) | ||
Theorem | el2oss1o 13218 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 13219. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (𝐴 ∈ 2_{o} → 𝐴 ⊆ 1_{o}) | ||
Theorem | ss1oel2o 13219 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4121 which more directly illustrates the contrast with el2oss1o 13218. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ 1_{o} → 𝑥 ∈ 2_{o})) | ||
Theorem | pw1dom2 13220 | The power set of 1_{o} dominates 2_{o}. Also see pwpw0ss 3731 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
⊢ 2_{o} ≼ 𝒫 1_{o} | ||
Theorem | nnti 13221 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
⊢ (𝜑 → 𝐴 ∈ ω) ⇒ ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢 E 𝑣 ∧ ¬ 𝑣 E 𝑢))) | ||
Theorem | pwtrufal 13222 | A subset of the singleton {∅} cannot be anything other than ∅ or {∅}. Removing the double negation would change the meaning, as seen at exmid01 4121. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4120), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.) |
⊢ (𝐴 ⊆ {∅} → ¬ ¬ (𝐴 = ∅ ∨ 𝐴 = {∅})) | ||
Theorem | pwle2 13223* | An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1_{o}) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1_{o}) → 𝑁 ⊆ 2_{o}) | ||
Theorem | pwf1oexmid 13224* | An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1_{o}) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1_{o}) → (ran 𝐺 = 𝒫 1_{o} ↔ (𝑁 = 2_{o} ∧ EXMID))) | ||
Theorem | exmid1stab 13225* | If any proposition is stable, excluded middle follows. We are thinking of 𝑥 as a proposition and 𝑥 = {∅} as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.) |
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → STAB 𝑥 = {∅}) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | subctctexmid 13226* | If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.) |
⊢ (𝜑 → ∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_{o}))) & ⊢ (𝜑 → ω ∈ Markov) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | 0nninf 13227 | The zero element of ℕ_{∞} (the constant sequence equal to ∅). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {∅}) ∈ ℕ_{∞} | ||
Theorem | nninff 13228 | An element of ℕ_{∞} is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝐴 ∈ ℕ_{∞} → 𝐴:ω⟶2_{o}) | ||
Theorem | nnsf 13229* | Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ_{∞}⟶ℕ_{∞} | ||
Theorem | peano4nninf 13230* | The successor function on ℕ_{∞} is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ_{∞}–1-1→ℕ_{∞} | ||
Theorem | peano3nninf 13231* | The successor function on ℕ_{∞} is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ (𝐴 ∈ ℕ_{∞} → (𝑆‘𝐴) ≠ (𝑥 ∈ ω ↦ ∅)) | ||
Theorem | nninfalllemn 13232* | Lemma for nninfall 13234. Mapping of a natural number to an element of ℕ_{∞}. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝜑 → 𝑃 ∈ ℕ_{∞}) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1_{o}) & ⊢ (𝜑 → (𝑃‘𝑁) = ∅) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) | ||
Theorem | nninfalllem1 13233* | Lemma for nninfall 13234. (Contributed by Jim Kingdon, 1-Aug-2022.) |
⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1_{o})) = 1_{o}) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = 1_{o}) & ⊢ (𝜑 → 𝑃 ∈ ℕ_{∞}) & ⊢ (𝜑 → (𝑄‘𝑃) = ∅) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑃‘𝑛) = 1_{o}) | ||
Theorem | nninfall 13234* | Given a decidable predicate on ℕ_{∞}, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which 𝑄 is a decidable predicate is that it assigns a value of either ∅ or 1_{o} (which can be thought of as false and true) to every element of ℕ_{∞}. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1_{o})) = 1_{o}) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = 1_{o}) ⇒ ⊢ (𝜑 → ∀𝑝 ∈ ℕ_{∞} (𝑄‘𝑝) = 1_{o}) | ||
Theorem | nninfex 13235 | ℕ_{∞} is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ ℕ_{∞} ∈ V | ||
Theorem | nninfsellemdc 13236* | Lemma for nninfself 13239. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝑁 ∈ ω) → DECID ∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}) | ||
Theorem | nninfsellemcl 13237* | Lemma for nninfself 13239. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝑁 ∈ ω) → if(∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅) ∈ 2_{o}) | ||
Theorem | nninfsellemsuc 13238* | Lemma for nninfself 13239. (Contributed by Jim Kingdon, 6-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝐽 ∈ ω) → if(∀𝑘 ∈ suc suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅) ⊆ if(∀𝑘 ∈ suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅)) | ||
Theorem | nninfself 13239* | Domain and range of the selection function for ℕ_{∞}. (Contributed by Jim Kingdon, 6-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) ⇒ ⊢ 𝐸:(2_{o} ↑_{𝑚} ℕ_{∞})⟶ℕ_{∞} | ||
Theorem | nninfsellemeq 13240* | Lemma for nninfsel 13243. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑁 (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}) & ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) = ∅) ⇒ ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) | ||
Theorem | nninfsellemqall 13241* | Lemma for nninfsel 13243. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) = 1_{o}) | ||
Theorem | nninfsellemeqinf 13242* | Lemma for nninfsel 13243. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) ⇒ ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ 1_{o})) | ||
Theorem | nninfsel 13243* | 𝐸 is a selection function for ℕ_{∞}. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) ⇒ ⊢ (𝜑 → ∀𝑝 ∈ ℕ_{∞} (𝑄‘𝑝) = 1_{o}) | ||
Theorem | nninfomnilem 13244* | Lemma for nninfomni 13245. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) ⇒ ⊢ ℕ_{∞} ∈ Omni | ||
Theorem | nninfomni 13245 | ℕ_{∞} is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ ℕ_{∞} ∈ Omni | ||
Theorem | nninffeq 13246* | Equality of two functions on ℕ_{∞} which agree at every integer and at the point at infinity. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 4-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ_{∞}⟶ℕ_{0}) & ⊢ (𝜑 → 𝐺:ℕ_{∞}⟶ℕ_{0}) & ⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1_{o})) = (𝐺‘(𝑥 ∈ ω ↦ 1_{o}))) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅)))) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | exmidsbthrlem 13247* | Lemma for exmidsbthr 13248. (Contributed by Jim Kingdon, 11-Aug-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID) | ||
Theorem | exmidsbthr 13248* | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID) | ||
Theorem | exmidsbth 13249* |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6855) is the
proof of the Schroeder-Bernstein Theorem from the Metamath Proof
Explorer database (in which excluded middle holds), but adapted to use
EXMID as an antecedent rather
than being unconditionally true, as in
the non-intuitionist proof at
https://us.metamath.org/mpeuni/sbth.html 6855.
The reverse direction (exmidsbthr 13248) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦)) | ||
Theorem | sbthomlem 13250 | Lemma for sbthom 13251. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
⊢ (𝜑 → ω ∈ Omni) & ⊢ (𝜑 → 𝑌 ⊆ {∅}) & ⊢ (𝜑 → 𝐹:ω–1-1-onto→(𝑌 ⊔ ω)) ⇒ ⊢ (𝜑 → (𝑌 = ∅ ∨ 𝑌 = {∅})) | ||
Theorem | sbthom 13251 | Schroeder-Bernstein is not possible even for ω. We know by exmidsbth 13249 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ω? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.) |
⊢ ((∀𝑥((𝑥 ≼ ω ∧ ω ≼ 𝑥) → 𝑥 ≈ ω) ∧ ω ∈ Omni) → EXMID) | ||
Theorem | qdencn 13252* | The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 10981 (and also would hold for ℝ × ℝ with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
⊢ 𝑄 = {𝑧 ∈ ℂ ∣ ((ℜ‘𝑧) ∈ ℚ ∧ (ℑ‘𝑧) ∈ ℚ)} ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ^{+}) → ∃𝑥 ∈ 𝑄 (abs‘(𝑥 − 𝐴)) < 𝐵) | ||
Theorem | refeq 13253* | Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑥 < 0 → (𝐹‘𝑥) = (𝐺‘𝑥))) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (0 < 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))) & ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | triap 13254 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) ↔ DECID 𝐴 # 𝐵)) | ||
Theorem | isomninnlem 13255* | Lemma for isomninn 13256. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) | ||
Theorem | isomninn 13256* | Omniscience stated in terms of natural numbers. Similar to isomnimap 7009 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1_{o}. (Contributed by Jim Kingdon, 30-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) | ||
Theorem | cvgcmp2nlemabs 13257* | Lemma for cvgcmp2n 13258. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting (seq1( + , 𝐺)‘𝑁) as the sum of (seq1( + , 𝐺)‘𝑀) and a term which gets smaller as 𝑀 gets large. (Contributed by Jim Kingdon, 25-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘𝑀)) ⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀)) | ||
Theorem | cvgcmp2n 13258* | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | trilpolemclim 13259* | Lemma for trilpo 13266. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | trilpolemcl 13260* | Lemma for trilpo 13266. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | trilpolemisumle 13261* | Lemma for trilpo 13266. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) & ⊢ 𝑍 = (ℤ_{≥}‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑖 ∈ 𝑍 ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ 𝑍 (1 / (2↑𝑖))) | ||
Theorem | trilpolemgt1 13262* | Lemma for trilpo 13266. The 1 < 𝐴 case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ⇒ ⊢ (𝜑 → ¬ 1 < 𝐴) | ||
Theorem | trilpolemeq1 13263* | Lemma for trilpo 13266. The 𝐴 = 1 case. This is proved by noting that if any (𝐹‘𝑥) is zero, then the infinite sum 𝐴 is less than one based on the term which is zero. We are using the fact that the 𝐹 sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) & ⊢ (𝜑 → 𝐴 = 1) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1) | ||
Theorem | trilpolemlt1 13264* | Lemma for trilpo 13266. The 𝐴 < 1 case. We can use the distance between 𝐴 and one (that is, 1 − 𝐴) to find a position in the sequence 𝑛 where terms after that point will not add up to as much as 1 − 𝐴. By finomni 7012 we know the terms up to 𝑛 either contain a zero or are all one. But if they are all one that contradicts the way we constructed 𝑛, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0) | ||
Theorem | trilpolemres 13265* | Lemma for trilpo 13266. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) & ⊢ (𝜑 → (𝐴 < 1 ∨ 𝐴 = 1 ∨ 1 < 𝐴)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0 ∨ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)) | ||
Theorem | trilpo 13266* |
Real number trichotomy implies the Limited Principle of Omniscience
(LPO). We expect that we'd need some form of countable choice to prove
the converse.
Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 13264 (which means the sequence contains a zero), trilpolemeq1 13263 (which means the sequence is all ones), and trilpolemgt1 13262 (which is not possible). (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ω ∈ Omni) | ||
Theorem | apdifflemf 13267 | Lemma for apdiff 13269. Being apart from the point halfway between 𝑄 and 𝑅 suffices for 𝐴 to be a different distance from 𝑄 and from 𝑅. (Contributed by Jim Kingdon, 18-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑄 ∈ ℚ) & ⊢ (𝜑 → 𝑅 ∈ ℚ) & ⊢ (𝜑 → 𝑄 < 𝑅) & ⊢ (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅))) | ||
Theorem | apdifflemr 13268 | Lemma for apdiff 13269. (Contributed by Jim Kingdon, 19-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑆 ∈ ℚ) & ⊢ (𝜑 → (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1))) & ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆)))) ⇒ ⊢ (𝜑 → 𝐴 # 𝑆) | ||
Theorem | apdiff 13269* | The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.) |
⊢ (𝐴 ∈ ℝ → (∀𝑞 ∈ ℚ 𝐴 # 𝑞 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟))))) | ||
Theorem | supfz 13270 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
Theorem | inffz 13271 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
Theorem | taupi 13272 | Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
⊢ τ = (2 · π) | ||
Theorem | ax1hfs 13273 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) |
⊢ (𝜑 → (𝜑 ∧ 𝜑)) | ||
Theorem | dftest 13274 |
A proposition is testable iff its negative or double-negative is true.
See Chapter 2 [Moschovakis] p. 2.
We do not formally define testability with a new token, but instead use DECID ¬ before the formula in question. For example, DECID ¬ 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) For statements about testable propositions, search for the keyword "testable" in the comments of statements, for instance using the Metamath command "MM> SEARCH * "testable" / COMMENTS". (New usage is discouraged.) |
⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑)) | ||
These are definitions and proofs involving an experimental "allsome" quantifier (aka "all some"). In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like ∀𝑥𝜑 → 𝜓 do not imply that 𝜑 is ever true, leading to vacuous truths. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem. The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines. I do not expect this to be used much in metamath, because in metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it. The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow ∀!𝑥(𝜑 → 𝜓), and when restricted (applied to a class) we allow ∀!𝑥 ∈ 𝐴𝜑. The first symbol after the setvar variable must always be ∈ if it is the form applied to a class, and since ∈ cannot begin a wff, it is unambiguous. The → looks like it would be a problem because 𝜑 or 𝜓 might include implications, but any implication arrow → within any wff must be surrounded by parentheses, so only the implication arrow of ∀! can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html I hope that others will eventually agree that allsome is awesome. | ||
Syntax | walsi 13275 | Extend wff definition to include "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and there is at least least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.) |
wff ∀!𝑥(𝜑 → 𝜓) | ||
Syntax | walsc 13276 | Extend wff definition to include "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.) |
wff ∀!𝑥 ∈ 𝐴𝜑 | ||
Definition | df-alsi 13277 | Define "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and there is at least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑)) | ||
Definition | df-alsc 13278 | Define "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴 and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | alsconv 13279 | There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.) |
⊢ (∀!𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀!𝑥 ∈ 𝐴𝜑) | ||
Theorem | alsi1d 13280 | Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒)) | ||
Theorem | alsi2d 13281 | Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | alsc1d 13282 | Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | alsc2d 13283 | Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
< Previous Wrap > |
Copyright terms: Public domain | < Previous Wrap > |