Home | Metamath
Proof Explorer Theorem List (p. 403 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | frege44 40201 | Similar to a commuted pm2.62 896. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
Theorem | frege45 40202 | Deduce pm2.6 193 from con1 148. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) → ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))) | ||
Theorem | frege46 40203 | If 𝜓 holds when 𝜑 occurs as well as when 𝜑 does not occur, then 𝜓 holds. If 𝜓 or 𝜑 occurs and if the occurrences of 𝜑 has 𝜓 as a necessary consequence, then 𝜓 takes place. Identical to pm2.6 193. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | frege47 40204 | Deduce consequence follows from either path implied by a disjunction. If 𝜑, as well as 𝜓 is sufficient condition for 𝜒 and 𝜓 or 𝜑 takes place, then the proposition 𝜒 holds. Proposition 47 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜒) → ((𝜑 → 𝜒) → 𝜒))) | ||
Theorem | frege48 40205 | Closed form of syllogism with internal disjunction. If 𝜑 is a sufficient condition for the occurrence of 𝜒 or 𝜓 and if 𝜒, as well as 𝜓, is a sufficient condition for 𝜃, then 𝜑 is a sufficient condition for 𝜃. See application in frege101 40317. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → ((𝜒 → 𝜃) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))) | ||
Theorem | frege49 40206 | Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → 𝜒))) | ||
Theorem | frege50 40207 | Closed form of jaoi 853. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((¬ 𝜑 → 𝜒) → 𝜓))) | ||
Theorem | frege51 40208 | Compare with jaod 855. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜒) → (𝜑 → ((¬ 𝜓 → 𝜃) → 𝜒)))) | ||
Here we leverage df-ifp 1058 to partition a wff into two that are disjoint with the selector wff. Thus if we are given ⊢ (𝜑 ↔ if-(𝜓, 𝜒, 𝜃)) then we replace the concept (illegal in our notation ) (𝜑‘𝜓) with if-(𝜓, 𝜒, 𝜃) to reason about the values of the "function." Likewise, we replace the similarly illegal concept ∀𝜓𝜑 with (𝜒 ∧ 𝜃). | ||
Theorem | axfrege52a 40209 | Justification for ax-frege52a 40210. (Contributed by RP, 17-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
Axiom | ax-frege52a 40210 | The case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed (in this specific case the identity logical function) and the same proposition, this time where we substituted the content of 𝜓, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
Theorem | frege52aid 40211 | The case when the content of 𝜑 is identical with the content of 𝜓 and in which 𝜑 is affirmed and 𝜓 is denied does not take place. Identical to biimp 217. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | frege53aid 40212 | Specialization of frege53a 40213. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ((𝜑 ↔ 𝜓) → 𝜓)) | ||
Theorem | frege53a 40213 | Lemma for frege55a 40221. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜃, 𝜒) → ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜃, 𝜒))) | ||
Theorem | axfrege54a 40214 | Justification for ax-frege54a 40215. Identical to biid 263. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 ↔ 𝜑) | ||
Axiom | ax-frege54a 40215 | Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 263. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑) | ||
Theorem | frege54cor0a 40216 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege54cor1a 40217 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | frege55aid 40218 | Lemma for frege57aid 40225. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege55lem1a 40219 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑))) | ||
Theorem | frege55lem2a 40220 | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55a 40221 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55cor1a 40222 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege56aid 40223 | Lemma for frege57aid 40225. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓))) | ||
Theorem | frege56a 40224 | Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)))) | ||
Theorem | frege57aid 40225 | This is the all imporant formula which allows us to apply Frege-style definitions and explore their consequences. A closed form of biimpri 230. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | frege57a 40226 | Analogue of frege57aid 40225. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) | ||
Theorem | axfrege58a 40227 | Identical to anifp 1065. Justification for ax-frege58a 40228. (Contributed by RP, 28-Mar-2020.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Axiom | ax-frege58a 40228 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | frege58acor 40229 | Lemma for frege59a 40230. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | frege59a 40230 |
A kind of Aristotelian inference. Namely Felapton or Fesapo. Proposition
59 of [Frege1879] p. 51.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 40166 incorrectly referenced where frege30 40185 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)))) | ||
Theorem | frege60a 40231 | Swap antecedents of ax-frege58a 40228. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege61a 40232 | Lemma for frege65a 40236. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | frege62a 40233 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2748 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | frege63a 40234 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏)))) | ||
Theorem | frege64a 40235 | Lemma for frege65a 40236. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁)))) | ||
Theorem | frege65a 40236 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2748 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege66a 40237 | Swap antecedents of frege65a 40236. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege67a 40238 | Lemma for frege68a 40239. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒)))) | ||
Theorem | frege68a 40239 | Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒))) | ||
Theorem | axfrege52c 40240 | Justification for ax-frege52c 40241. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Axiom | ax-frege52c 40241 | One side of dfsbcq 3776. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege52b 40242 | The case when the content of 𝑥 is identical with the content of 𝑦 and in which a proposition controlled by an element for which we substitute the content of 𝑥 is affirmed and the same proposition, this time where we substitute the content of 𝑦, is denied does not take place. In [𝑥 / 𝑧]𝜑, 𝑥 can also occur in other than the argument (𝑧) places. Hence 𝑥 may still be contained in [𝑦 / 𝑧]𝜑. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | frege53b 40243 | Lemma for frege102 (via frege92 40308). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑)) | ||
Theorem | axfrege54c 40244 | Reflexive equality of classes. Identical to eqid 2823. Justification for ax-frege54c 40245. (Contributed by RP, 24-Dec-2019.) |
⊢ 𝐴 = 𝐴 | ||
Axiom | ax-frege54c 40245 | Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2823. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐴 | ||
Theorem | frege54b 40246 | Reflexive equality of sets. The content of 𝑥 is identical with the content of 𝑥. Part of Axiom 54 of [Frege1879] p. 50. Slightly specialized version of eqid 2823. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | frege54cor1b 40247 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) |
⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | ||
Theorem | frege55lem1b 40248* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧)) | ||
Theorem | frege55lem2b 40249 | Lemma for frege55b 40250. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55b 40250 |
Lemma for frege57b 40252. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2844 incorporates eqcom 2830 which is stronger than this proposition which is identical to equcomi 2024. Is it possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | frege56b 40251 | Lemma for frege57b 40252. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) → (𝑦 = 𝑥 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) | ||
Theorem | frege57b 40252 | Analogue of frege57aid 40225. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | ||
Theorem | axfrege58b 40253 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Justification for ax-frege58b 40254. (Contributed by RP, 28-Mar-2020.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Axiom | ax-frege58b 40254 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | frege58bid 40255 | If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2182. See ax-frege58b 40254 and frege58c 40274 for versions which more closely track the original. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | frege58bcor 40256 | Lemma for frege59b 40257. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | frege59b 40257 |
A kind of Aristotelian inference. Namely Felapton or Fesapo. Proposition
59 of [Frege1879] p. 51.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 40166 incorrectly referenced where frege30 40185 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60b 40258 | Swap antecedents of ax-frege58b 40254. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege61b 40259 | Lemma for frege65b 40263. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓)) | ||
Theorem | frege62b 40260 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2748 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [𝑦 / 𝑥]𝜓)) | ||
Theorem | frege63b 40261 | Lemma for frege91 40307. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege64b 40262 | Lemma for frege65b 40263. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒))) | ||
Theorem | frege65b 40263 |
A kind of Aristotelian inference. This judgement replaces the mode of
inference barbara 2748 when the minor premise has a general context.
Proposition 65 of [Frege1879] p. 53.
In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : ⊢ (∀𝑥([𝑥 / 𝑎]𝜑 → [𝑥 / 𝑏]𝜓) → (∀𝑦([𝑦 / 𝑏]𝜓 → [𝑦 / 𝑐]𝜒) → ([𝑧 / 𝑎]𝜑 → [𝑧 / 𝑐]𝜒))). But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege66b 40264 | Swap antecedents of frege65b 40263. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | frege67b 40265 | Lemma for frege68b 40266. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | frege68b 40266 | Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑)) | ||
Begriffsschrift Chapter II with equivalence of classes (where they are sets). | ||
Theorem | frege53c 40267 | Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege54cor1c 40268* | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ [𝐴 / 𝑥]𝑥 = 𝐴 | ||
Theorem | frege55lem1c 40269* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵)) | ||
Theorem | frege55lem2c 40270* | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55c 40271 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥) | ||
Theorem | frege56c 40272* | Lemma for frege57c 40273. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))) | ||
Theorem | frege57c 40273* | Swap order of implication in ax-frege52c 40241. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | frege58c 40274 | Principle related to sp 2182. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑) | ||
Theorem | frege59c 40275 |
A kind of Aristotelian inference. Proposition 59 of [Frege1879] p. 51.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 40166 incorrectly referenced where frege30 40185 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60c 40276 | Swap antecedents of frege58c 40274. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege61c 40277 | Lemma for frege65c 40281. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | frege62c 40278 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2748 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [𝐴 / 𝑥]𝜓)) | ||
Theorem | frege63c 40279 | Analogue of frege63b 40261. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege64c 40280 | Lemma for frege65c 40281. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege65c 40281 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2748 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege66c 40282 | Swap antecedents of frege65c 40281. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | frege67c 40283 | Lemma for frege68c 40284. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑))) | ||
Theorem | frege68c 40284 | Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑)) | ||
(𝑅 “ 𝐴) ⊆ 𝐴 means membership in 𝐴 is hereditary in the sequence dictated by relation 𝑅. This differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on. While the above notation is modern, it is cumbersome in the case when 𝐴 is complex and to more closely follow Frege, we abbreviate it with new notation 𝑅 hereditary 𝐴. This greatly shortens the statements for frege97 40313 and frege109 40325. dffrege69 40285 through frege75 40291 develop this, but translation to Metamath is pending some decisions. While Frege does not limit discussion to sets, we may have to depart from Frege by limiting 𝑅 or 𝐴 to sets when we quantify over all hereditary relations or all classes where membership is hereditary in a sequence dictated by 𝑅. | ||
Theorem | dffrege69 40285* | If from the proposition that 𝑥 has property 𝐴 it can be inferred generally, whatever 𝑥 may be, that every result of an application of the procedure 𝑅 to 𝑥 has property 𝐴, then we say " Property 𝐴 is hereditary in the 𝑅-sequence. Definition 69 of [Frege1879] p. 55. (Contributed by RP, 28-Mar-2020.) |
⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑥𝑅𝑦 → 𝑦 ∈ 𝐴)) ↔ 𝑅 hereditary 𝐴) | ||
Theorem | frege70 40286* | Lemma for frege72 40288. Proposition 70 of [Frege1879] p. 58. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑉 ⇒ ⊢ (𝑅 hereditary 𝐴 → (𝑋 ∈ 𝐴 → ∀𝑦(𝑋𝑅𝑦 → 𝑦 ∈ 𝐴))) | ||
Theorem | frege71 40287* | Lemma for frege72 40288. Proposition 71 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑉 ⇒ ⊢ ((∀𝑧(𝑋𝑅𝑧 → 𝑧 ∈ 𝐴) → (𝑋𝑅𝑌 → 𝑌 ∈ 𝐴)) → (𝑅 hereditary 𝐴 → (𝑋 ∈ 𝐴 → (𝑋𝑅𝑌 → 𝑌 ∈ 𝐴)))) | ||
Theorem | frege72 40288 | If property 𝐴 is hereditary in the 𝑅-sequence, if 𝑥 has property 𝐴, and if 𝑦 is a result of an application of the procedure 𝑅 to 𝑥, then 𝑦 has property 𝐴. Proposition 72 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ (𝑅 hereditary 𝐴 → (𝑋 ∈ 𝐴 → (𝑋𝑅𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege73 40289 | Lemma for frege87 40303. Proposition 73 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ ((𝑅 hereditary 𝐴 → 𝑋 ∈ 𝐴) → (𝑅 hereditary 𝐴 → (𝑋𝑅𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege74 40290 | If 𝑋 has a property 𝐴 that is hereditary in the 𝑅-sequence, then every result of a application of the procedure 𝑅 to 𝑋 has the property 𝐴. Proposition 74 of [Frege1879] p. 60. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ (𝑋 ∈ 𝐴 → (𝑅 hereditary 𝐴 → (𝑋𝑅𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege75 40291* | If from the proposition that 𝑥 has property 𝐴, whatever 𝑥 may be, it can be inferred that every result of an application of the procedure 𝑅 to 𝑥 has property 𝐴, then property 𝐴 is hereditary in the 𝑅-sequence. Proposition 75 of [Frege1879] p. 60. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑥𝑅𝑦 → 𝑦 ∈ 𝐴)) → 𝑅 hereditary 𝐴) | ||
𝑝(t+‘𝑅)𝑐 means 𝑐 follows 𝑝 in the 𝑅-sequence. dffrege76 40292 through frege98 40314 develop this. This will be shown to be the transitive closure of the relation 𝑅. But more work needs to be done on transitive closure of relations before this is ready for Metamath. | ||
Theorem | dffrege76 40292* |
If from the two propositions that every result of an application of
the procedure 𝑅 to 𝐵 has property 𝑓 and
that property
𝑓 is hereditary in the 𝑅-sequence, it can be inferred,
whatever 𝑓 may be, that 𝐸 has property 𝑓, then
we say
𝐸 follows 𝐵 in the 𝑅-sequence. Definition 76 of
[Frege1879] p. 60.
Each of 𝐵, 𝐸 and 𝑅 must be sets. (Contributed by RP, 2-Jul-2020.) |
⊢ 𝐵 ∈ 𝑈 & ⊢ 𝐸 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ (∀𝑓(𝑅 hereditary 𝑓 → (∀𝑎(𝐵𝑅𝑎 → 𝑎 ∈ 𝑓) → 𝐸 ∈ 𝑓)) ↔ 𝐵(t+‘𝑅)𝐸) | ||
Theorem | frege77 40293* | If 𝑌 follows 𝑋 in the 𝑅-sequence, if property 𝐴 is hereditary in the 𝑅-sequence, and if every result of an application of the procedure 𝑅 to 𝑋 has the property 𝐴, then 𝑌 has property 𝐴. Proposition 77 of [Frege1879] p. 62. (Contributed by RP, 29-Jun-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑋(t+‘𝑅)𝑌 → (𝑅 hereditary 𝐴 → (∀𝑎(𝑋𝑅𝑎 → 𝑎 ∈ 𝐴) → 𝑌 ∈ 𝐴))) | ||
Theorem | frege78 40294* | Commuted form of of frege77 40293. Proposition 78 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑅 hereditary 𝐴 → (∀𝑎(𝑋𝑅𝑎 → 𝑎 ∈ 𝐴) → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege79 40295* | Distributed form of frege78 40294. Proposition 79 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ((𝑅 hereditary 𝐴 → ∀𝑎(𝑋𝑅𝑎 → 𝑎 ∈ 𝐴)) → (𝑅 hereditary 𝐴 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege80 40296* | Add additional condition to both clauses of frege79 40295. Proposition 80 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ((𝑋 ∈ 𝐴 → (𝑅 hereditary 𝐴 → ∀𝑎(𝑋𝑅𝑎 → 𝑎 ∈ 𝐴))) → (𝑋 ∈ 𝐴 → (𝑅 hereditary 𝐴 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴)))) | ||
Theorem | frege81 40297 | If 𝑋 has a property 𝐴 that is hereditary in the 𝑅 -sequence, and if 𝑌 follows 𝑋 in the 𝑅-sequence, then 𝑌 has property 𝐴. This is a form of induction attributed to Jakob Bernoulli. Proposition 81 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑋 ∈ 𝐴 → (𝑅 hereditary 𝐴 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege82 40298 | Closed-form deduction based on frege81 40297. Proposition 82 of [Frege1879] p. 64. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ((𝜑 → 𝑋 ∈ 𝐴) → (𝑅 hereditary 𝐴 → (𝜑 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴)))) | ||
Theorem | frege83 40299 | Apply commuted form of frege81 40297 when the property 𝑅 is hereditary in a disjunction of two properties, only one of which is known to be held by 𝑋. Proposition 83 of [Frege1879] p. 65. Here we introduce the union of classes where Frege has a disjunction of properties which are represented by membership in either of the classes. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑆 & ⊢ 𝑌 ∈ 𝑇 & ⊢ 𝑅 ∈ 𝑈 & ⊢ 𝐵 ∈ 𝑉 & ⊢ 𝐶 ∈ 𝑊 ⇒ ⊢ (𝑅 hereditary (𝐵 ∪ 𝐶) → (𝑋 ∈ 𝐵 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ (𝐵 ∪ 𝐶)))) | ||
Theorem | frege84 40300 | Commuted form of frege81 40297. Proposition 84 of [Frege1879] p. 65. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑅 hereditary 𝐴 → (𝑋 ∈ 𝐴 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |