![]() |
Metamath
Proof Explorer Theorem List (p. 428 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-frege54a 42701 | Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 260. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑) | ||
Theorem | frege54cor0a 42702 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege54cor1a 42703 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | frege55aid 42704 | Lemma for frege57aid 42711. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege55lem1a 42705 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑))) | ||
Theorem | frege55lem2a 42706 | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55a 42707 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55cor1a 42708 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege56aid 42709 | Lemma for frege57aid 42711. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓))) | ||
Theorem | frege56a 42710 | Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)))) | ||
Theorem | frege57aid 42711 | This is the all imporant formula which allows to apply Frege-style definitions and explore their consequences. A closed form of biimpri 227. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | frege57a 42712 | Analogue of frege57aid 42711. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) | ||
Theorem | axfrege58a 42713 | Identical to anifp 1070. Justification for ax-frege58a 42714. (Contributed by RP, 28-Mar-2020.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Axiom | ax-frege58a 42714 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2071. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | frege58acor 42715 | Lemma for frege59a 42716. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | frege59a 42716 |
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 42652 incorrectly referenced where frege30 42671 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)))) | ||
Theorem | frege60a 42717 | Swap antecedents of ax-frege58a 42714. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege61a 42718 | Lemma for frege65a 42722. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | frege62a 42719 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2658 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 42720 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏)))) | ||
Theorem | frege64a 42721 | Lemma for frege65a 42722. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁)))) | ||
Theorem | frege65a 42722 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2658 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 42723 | Swap antecedents of frege65a 42722. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege67a 42724 | Lemma for frege68a 42725. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒)))) | ||
Theorem | frege68a 42725 | 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 42726 | Justification for ax-frege52c 42727. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Axiom | ax-frege52c 42727 | One side of dfsbcq 3779. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege52b 42728 | 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 42729 | Lemma for frege102 (via frege92 42794). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑)) | ||
Theorem | axfrege54c 42730 | Reflexive equality of classes. Identical to eqid 2732. Justification for ax-frege54c 42731. (Contributed by RP, 24-Dec-2019.) |
⊢ 𝐴 = 𝐴 | ||
Axiom | ax-frege54c 42731 | Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2732. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐴 | ||
Theorem | frege54b 42732 | 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 2732. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | frege54cor1b 42733 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) |
⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | ||
Theorem | frege55lem1b 42734* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧)) | ||
Theorem | frege55lem2b 42735 | Lemma for frege55b 42736. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55b 42736 |
Lemma for frege57b 42738. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2756 incorporates eqcom 2739 which is stronger than this proposition which is identical to equcomi 2020. 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 42737 | Lemma for frege57b 42738. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) → (𝑦 = 𝑥 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))) | ||
Theorem | frege57b 42738 | Analogue of frege57aid 42711. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | ||
Theorem | axfrege58b 42739 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2071. Justification for ax-frege58b 42740. (Contributed by RP, 28-Mar-2020.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Axiom | ax-frege58b 42740 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2071. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | frege58bid 42741 | If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2176. See ax-frege58b 42740 and frege58c 42760 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 42742 | Lemma for frege59b 42743. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | frege59b 42743 |
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 42652 incorrectly referenced where frege30 42671 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60b 42744 | Swap antecedents of ax-frege58b 42740. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege61b 42745 | Lemma for frege65b 42749. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓)) | ||
Theorem | frege62b 42746 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2658 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 42747 | Lemma for frege91 42793. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege64b 42748 | Lemma for frege65b 42749. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒))) | ||
Theorem | frege65b 42749 |
A kind of Aristotelian inference. This judgement replaces the mode of
inference barbara 2658 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 42750 | Swap antecedents of frege65b 42749. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | frege67b 42751 | Lemma for frege68b 42752. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | frege68b 42752 | 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 42753 | Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege54cor1c 42754* | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ [𝐴 / 𝑥]𝑥 = 𝐴 | ||
Theorem | frege55lem1c 42755* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵)) | ||
Theorem | frege55lem2c 42756* | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55c 42757 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥) | ||
Theorem | frege56c 42758* | Lemma for frege57c 42759. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))) | ||
Theorem | frege57c 42759* | Swap order of implication in ax-frege52c 42727. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | frege58c 42760 | Principle related to sp 2176. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑) | ||
Theorem | frege59c 42761 |
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 42652 incorrectly referenced where frege30 42671 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60c 42762 | Swap antecedents of frege58c 42760. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege61c 42763 | Lemma for frege65c 42767. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | frege62c 42764 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2658 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 42765 | Analogue of frege63b 42747. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege64c 42766 | Lemma for frege65c 42767. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege65c 42767 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2658 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 42768 | Swap antecedents of frege65c 42767. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | frege67c 42769 | Lemma for frege68c 42770. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑))) | ||
Theorem | frege68c 42770 | 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 42799 and frege109 42811. dffrege69 42771 through frege75 42777 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 42771* | 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 42772* | Lemma for frege72 42774. 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 42773* | Lemma for frege72 42774. 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 42774 | 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 42775 | Lemma for frege87 42789. 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 42776 | 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 42777* | 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 42778 through frege98 42800 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 42778* |
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 42779* | 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 42780* | Commuted form of frege77 42779. 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 42781* | Distributed form of frege78 42780. 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 42782* | Add additional condition to both clauses of frege79 42781. 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 42783 | 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 42784 | Closed-form deduction based on frege81 42783. 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 42785 | Apply commuted form of frege81 42783 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 42786 | Commuted form of frege81 42783. 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 42787* | Commuted form of frege77 42779. 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 42788* | 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 42789* | 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 42790* | Commuted form of frege87 42789. 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 42791* | One direction of dffrege76 42778. 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 42792* | Add antecedent to frege89 42791. 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 42793 | 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 42794 | Inference from frege91 42793. 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 42795* | 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 42796* | 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 42797 | 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 42798 | 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 42799 |
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 42800 | 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+‘𝑅)𝑍)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |