Home | Metamath
Proof Explorer Theorem List (p. 418 of 468) | < 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-29329) |
Hilbert Space Explorer
(29330-30852) |
Users' Mathboxes
(30853-46765) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | frege62a 41701 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2662 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 41702 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏)))) | ||
Theorem | frege64a 41703 | Lemma for frege65a 41704. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁)))) | ||
Theorem | frege65a 41704 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2662 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 41705 | Swap antecedents of frege65a 41704. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege67a 41706 | Lemma for frege68a 41707. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒)))) | ||
Theorem | frege68a 41707 | 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 41708 | Justification for ax-frege52c 41709. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Axiom | ax-frege52c 41709 | One side of dfsbcq 3723. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege52b 41710 | 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 41711 | Lemma for frege102 (via frege92 41776). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑)) | ||
Theorem | axfrege54c 41712 | Reflexive equality of classes. Identical to eqid 2736. Justification for ax-frege54c 41713. (Contributed by RP, 24-Dec-2019.) |
⊢ 𝐴 = 𝐴 | ||
Axiom | ax-frege54c 41713 | Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2736. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐴 | ||
Theorem | frege54b 41714 | 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 2736. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | frege54cor1b 41715 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) |
⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | ||
Theorem | frege55lem1b 41716* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧)) | ||
Theorem | frege55lem2b 41717 | Lemma for frege55b 41718. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55b 41718 |
Lemma for frege57b 41720. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2760 incorporates eqcom 2743 which is stronger than this proposition which is identical to equcomi 2018. 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 41719 | Lemma for frege57b 41720. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) → (𝑦 = 𝑥 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) | ||
Theorem | frege57b 41720 | Analogue of frege57aid 41693. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | ||
Theorem | axfrege58b 41721 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2069. Justification for ax-frege58b 41722. (Contributed by RP, 28-Mar-2020.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Axiom | ax-frege58b 41722 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2069. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | frege58bid 41723 | If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2174. See ax-frege58b 41722 and frege58c 41742 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 41724 | Lemma for frege59b 41725. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | frege59b 41725 |
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 41634 incorrectly referenced where frege30 41653 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60b 41726 | Swap antecedents of ax-frege58b 41722. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege61b 41727 | Lemma for frege65b 41731. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓)) | ||
Theorem | frege62b 41728 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2662 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 41729 | Lemma for frege91 41775. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege64b 41730 | Lemma for frege65b 41731. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒))) | ||
Theorem | frege65b 41731 |
A kind of Aristotelian inference. This judgement replaces the mode of
inference barbara 2662 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 41732 | Swap antecedents of frege65b 41731. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | frege67b 41733 | Lemma for frege68b 41734. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | frege68b 41734 | 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 41735 | Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege54cor1c 41736* | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ [𝐴 / 𝑥]𝑥 = 𝐴 | ||
Theorem | frege55lem1c 41737* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵)) | ||
Theorem | frege55lem2c 41738* | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55c 41739 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥) | ||
Theorem | frege56c 41740* | Lemma for frege57c 41741. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))) | ||
Theorem | frege57c 41741* | Swap order of implication in ax-frege52c 41709. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | frege58c 41742 | Principle related to sp 2174. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑) | ||
Theorem | frege59c 41743 |
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 41634 incorrectly referenced where frege30 41653 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60c 41744 | Swap antecedents of frege58c 41742. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege61c 41745 | Lemma for frege65c 41749. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | frege62c 41746 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2662 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 41747 | Analogue of frege63b 41729. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege64c 41748 | Lemma for frege65c 41749. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege65c 41749 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2662 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 41750 | Swap antecedents of frege65c 41749. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | frege67c 41751 | Lemma for frege68c 41752. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑))) | ||
Theorem | frege68c 41752 | 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 41781 and frege109 41793. dffrege69 41753 through frege75 41759 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 41753* | 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 41754* | Lemma for frege72 41756. 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 41755* | Lemma for frege72 41756. 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 41756 | 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 41757 | Lemma for frege87 41771. 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 41758 | 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 41759* | 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 41760 through frege98 41782 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 41760* |
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 41761* | 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 41762* | Commuted form of of frege77 41761. 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 41763* | Distributed form of frege78 41762. 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 41764* | Add additional condition to both clauses of frege79 41763. 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 41765 | 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 41766 | Closed-form deduction based on frege81 41765. 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 41767 | Apply commuted form of frege81 41765 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 41768 | Commuted form of frege81 41765. Proposition 84 of [Frege1879] p. 65. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑅 hereditary 𝐴 → (𝑋 ∈ 𝐴 → (𝑋(t+‘𝑅)𝑌 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege85 41769* | Commuted form of frege77 41761. Proposition 85 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑋(t+‘𝑅)𝑌 → (∀𝑧(𝑋𝑅𝑧 → 𝑧 ∈ 𝐴) → (𝑅 hereditary 𝐴 → 𝑌 ∈ 𝐴))) | ||
Theorem | frege86 41770* | Conclusion about element one past 𝑌 in the 𝑅-sequence. Proposition 86 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (((𝑅 hereditary 𝐴 → 𝑌 ∈ 𝐴) → (𝑅 hereditary 𝐴 → (𝑌𝑅𝑍 → 𝑍 ∈ 𝐴))) → (𝑋(t+‘𝑅)𝑌 → (∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝐴) → (𝑅 hereditary 𝐴 → (𝑌𝑅𝑍 → 𝑍 ∈ 𝐴))))) | ||
Theorem | frege87 41771* | If 𝑍 is a result of an application of the procedure 𝑅 to an object 𝑌 that follows 𝑋 in the 𝑅-sequence and if every result of an application of the procedure 𝑅 to 𝑋 has a property 𝐴 that is hereditary in the 𝑅-sequence, then 𝑍 has property 𝐴. Proposition 87 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑍 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑋(t+‘𝑅)𝑌 → (∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝐴) → (𝑅 hereditary 𝐴 → (𝑌𝑅𝑍 → 𝑍 ∈ 𝐴)))) | ||
Theorem | frege88 41772* | Commuted form of frege87 41771. Proposition 88 of [Frege1879] p. 67. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑍 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 & ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (𝑌𝑅𝑍 → (𝑋(t+‘𝑅)𝑌 → (∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝐴) → (𝑅 hereditary 𝐴 → 𝑍 ∈ 𝐴)))) | ||
Theorem | frege89 41773* | One direction of dffrege76 41760. Proposition 89 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ (∀𝑓(𝑅 hereditary 𝑓 → (∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝑓) → 𝑌 ∈ 𝑓)) → 𝑋(t+‘𝑅)𝑌) | ||
Theorem | frege90 41774* | Add antecedent to frege89 41773. Proposition 90 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ ((𝜑 → ∀𝑓(𝑅 hereditary 𝑓 → (∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝑓) → 𝑌 ∈ 𝑓))) → (𝜑 → 𝑋(t+‘𝑅)𝑌)) | ||
Theorem | frege91 41775 | Every result of an application of a procedure 𝑅 to an object 𝑋 follows that 𝑋 in the 𝑅-sequence. Proposition 91 of [Frege1879] p. 68. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ (𝑋𝑅𝑌 → 𝑋(t+‘𝑅)𝑌) | ||
Theorem | frege92 41776 | Inference from frege91 41775. Proposition 92 of [Frege1879] p. 69. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ (𝑋 = 𝑍 → (𝑋𝑅𝑌 → 𝑍(t+‘𝑅)𝑌)) | ||
Theorem | frege93 41777* | Necessary condition for two elements to be related by the transitive closure. Proposition 93 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ (∀𝑓(∀𝑧(𝑋𝑅𝑧 → 𝑧 ∈ 𝑓) → (𝑅 hereditary 𝑓 → 𝑌 ∈ 𝑓)) → 𝑋(t+‘𝑅)𝑌) | ||
Theorem | frege94 41778* | Looking one past a pair related by transitive closure of a relation. Proposition 94 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑍 ∈ 𝑉 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ ((𝑌𝑅𝑍 → (𝑋(t+‘𝑅)𝑌 → ∀𝑓(∀𝑤(𝑋𝑅𝑤 → 𝑤 ∈ 𝑓) → (𝑅 hereditary 𝑓 → 𝑍 ∈ 𝑓)))) → (𝑌𝑅𝑍 → (𝑋(t+‘𝑅)𝑌 → 𝑋(t+‘𝑅)𝑍))) | ||
Theorem | frege95 41779 | Looking one past a pair related by transitive closure of a relation. Proposition 95 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑍 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝐴 ⇒ ⊢ (𝑌𝑅𝑍 → (𝑋(t+‘𝑅)𝑌 → 𝑋(t+‘𝑅)𝑍)) | ||
Theorem | frege96 41780 | Every result of an application of the procedure 𝑅 to an object that follows 𝑋 in the 𝑅-sequence follows 𝑋 in the 𝑅 -sequence. Proposition 96 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑍 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝐴 ⇒ ⊢ (𝑋(t+‘𝑅)𝑌 → (𝑌𝑅𝑍 → 𝑋(t+‘𝑅)𝑍)) | ||
Theorem | frege97 41781 |
The property of following 𝑋 in the 𝑅-sequence is hereditary
in the 𝑅-sequence. Proposition 97 of [Frege1879] p. 71.
Here we introduce the image of a singleton under a relation as class which stands for the property of following 𝑋 in the 𝑅 -sequence. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑅 ∈ 𝑊 ⇒ ⊢ 𝑅 hereditary ((t+‘𝑅) “ {𝑋}) | ||
Theorem | frege98 41782 | If 𝑌 follows 𝑋 and 𝑍 follows 𝑌 in the 𝑅-sequence then 𝑍 follows 𝑋 in the 𝑅-sequence because the transitive closure of a relation has the transitive property. Proposition 98 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 6-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑍 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (𝑋(t+‘𝑅)𝑌 → (𝑌(t+‘𝑅)𝑍 → 𝑋(t+‘𝑅)𝑍)) | ||
𝑝((t+‘𝑅) ∪ I )𝑐 means 𝑐 is a member of the 𝑅 -sequence begining with 𝑝 and 𝑝 is a member of the 𝑅 -sequence ending with 𝑐. dffrege99 41783 through frege114 41798 develop this. This will be shown to be related to the transitive-reflexive closure of relation 𝑅. But more work needs to be done on transitive closure of relations before this is ready for Metamath. | ||
Theorem | dffrege99 41783 | If 𝑍 is identical with 𝑋 or follows 𝑋 in the 𝑅 -sequence, then we say : "𝑍 belongs to the 𝑅-sequence beginning with 𝑋 " or "𝑋 belongs to the 𝑅-sequence ending with 𝑍". Definition 99 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.) |
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) ↔ 𝑋((t+‘𝑅) ∪ I )𝑍) | ||
Theorem | frege100 41784 | One direction of dffrege99 41783. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋)) | ||
Theorem | frege101 41785 | Lemma for frege102 41786. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ ((𝑍 = 𝑋 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → ((𝑋(t+‘𝑅)𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)))) | ||
Theorem | frege102 41786 | If 𝑍 belongs to the 𝑅-sequence beginning with 𝑋, then every result of an application of the procedure 𝑅 to 𝑍 follows 𝑋 in the 𝑅-sequence. Proposition 102 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝐴 & ⊢ 𝑍 ∈ 𝐵 & ⊢ 𝑉 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) | ||
Theorem | frege103 41787 | Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((𝑍 = 𝑋 → 𝑋 = 𝑍) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍))) | ||
Theorem | frege104 41788 |
Proposition 104 of [Frege1879] p. 73.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the minor clause and result swapped. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍)) | ||
Theorem | frege105 41789 | Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) → 𝑋((t+‘𝑅) ∪ I )𝑍) | ||
Theorem | frege106 41790 | Whatever follows 𝑋 in the 𝑅-sequence belongs to the 𝑅 -sequence beginning with 𝑋. Proposition 106 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ (𝑋(t+‘𝑅)𝑍 → 𝑋((t+‘𝑅) ∪ I )𝑍) | ||
Theorem | frege107 41791 | Proposition 107 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑉 ∈ 𝐴 ⇒ ⊢ ((𝑍((t+‘𝑅) ∪ I )𝑌 → (𝑌𝑅𝑉 → 𝑍(t+‘𝑅)𝑉)) → (𝑍((t+‘𝑅) ∪ I )𝑌 → (𝑌𝑅𝑉 → 𝑍((t+‘𝑅) ∪ I )𝑉))) | ||
Theorem | frege108 41792 | If 𝑌 belongs to the 𝑅-sequence beginning with 𝑍, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence beginning with 𝑍. Proposition 108 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑉 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (𝑍((t+‘𝑅) ∪ I )𝑌 → (𝑌𝑅𝑉 → 𝑍((t+‘𝑅) ∪ I )𝑉)) | ||
Theorem | frege109 41793 | The property of belonging to the 𝑅-sequence beginning with 𝑋 is hereditary in the 𝑅-sequence. Proposition 109 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ 𝑅 hereditary (((t+‘𝑅) ∪ I ) “ {𝑋}) | ||
Theorem | frege110 41794* | Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑀 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀)) | ||
Theorem | frege111 41795 | If 𝑌 belongs to the 𝑅-sequence beginning with 𝑍, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence beginning with 𝑍 or precedes 𝑍 in the 𝑅-sequence. Proposition 111 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Revised by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑉 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (𝑍((t+‘𝑅) ∪ I )𝑌 → (𝑌𝑅𝑉 → (¬ 𝑉(t+‘𝑅)𝑍 → 𝑍((t+‘𝑅) ∪ I )𝑉))) | ||
Theorem | frege112 41796 | Identity implies belonging to the 𝑅-sequence beginning with self. Proposition 112 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ (𝑍 = 𝑋 → 𝑋((t+‘𝑅) ∪ I )𝑍) | ||
Theorem | frege113 41797 | Proposition 113 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((𝑍((t+‘𝑅) ∪ I )𝑋 → (¬ 𝑍(t+‘𝑅)𝑋 → 𝑍 = 𝑋)) → (𝑍((t+‘𝑅) ∪ I )𝑋 → (¬ 𝑍(t+‘𝑅)𝑋 → 𝑋((t+‘𝑅) ∪ I )𝑍))) | ||
Theorem | frege114 41798 | If 𝑋 belongs to the 𝑅-sequence beginning with 𝑍, then 𝑍 belongs to the 𝑅-sequence beginning with 𝑋 or 𝑋 follows 𝑍 in the 𝑅-sequence. Proposition 114 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ (𝑍((t+‘𝑅) ∪ I )𝑋 → (¬ 𝑍(t+‘𝑅)𝑋 → 𝑋((t+‘𝑅) ∪ I )𝑍)) | ||
Fun ◡◡𝑅 means the relationship content of procedure 𝑅 is single-valued. The double converse allows us to simply apply this syntax in place of Frege's even though the original never explicitly limited discussion of propositional statements which vary on two variables to relations. dffrege115 41799 through frege133 41817 develop this and how functions relate to transitive and transitive-reflexive closures. | ||
Theorem | dffrege115 41799* | If from the circumstance that 𝑐 is a result of an application of the procedure 𝑅 to 𝑏, whatever 𝑏 may be, it can be inferred that every result of an application of the procedure 𝑅 to 𝑏 is the same as 𝑐, then we say : "The procedure 𝑅 is single-valued". Definition 115 of [Frege1879] p. 77. (Contributed by RP, 7-Jul-2020.) |
⊢ (∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) | ||
Theorem | frege116 41800* | One direction of dffrege115 41799. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 ⇒ ⊢ (Fun ◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |