![]() |
Metamath
Proof Explorer Theorem List (p. 407 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axfrege58b 40601 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Justification for ax-frege58b 40602. (Contributed by RP, 28-Mar-2020.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Axiom | ax-frege58b 40602 | 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 40603 | If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2180. See ax-frege58b 40602 and frege58c 40622 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 40604 | Lemma for frege59b 40605. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | frege59b 40605 |
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 40514 incorrectly referenced where frege30 40533 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60b 40606 | Swap antecedents of ax-frege58b 40602. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege61b 40607 | Lemma for frege65b 40611. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓)) | ||
Theorem | frege62b 40608 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2725 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 40609 | Lemma for frege91 40655. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝑦 / 𝑥]𝜒))) | ||
Theorem | frege64b 40610 | Lemma for frege65b 40611. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒))) | ||
Theorem | frege65b 40611 |
A kind of Aristotelian inference. This judgement replaces the mode of
inference barbara 2725 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 40612 | Swap antecedents of frege65b 40611. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | frege67b 40613 | Lemma for frege68b 40614. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | frege68b 40614 | 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 40615 | Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege54cor1c 40616* | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ [𝐴 / 𝑥]𝑥 = 𝐴 | ||
Theorem | frege55lem1c 40617* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵)) | ||
Theorem | frege55lem2c 40618* | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55c 40619 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥) | ||
Theorem | frege56c 40620* | Lemma for frege57c 40621. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))) | ||
Theorem | frege57c 40621* | Swap order of implication in ax-frege52c 40589. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | frege58c 40622 | Principle related to sp 2180. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑) | ||
Theorem | frege59c 40623 |
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 40514 incorrectly referenced where frege30 40533 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | frege60c 40624 | Swap antecedents of frege58c 40622. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege61c 40625 | Lemma for frege65c 40629. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | frege62c 40626 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2725 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 40627 | Analogue of frege63b 40609. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege64c 40628 | Lemma for frege65c 40629. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒))) | ||
Theorem | frege65c 40629 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2725 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 40630 | Swap antecedents of frege65c 40629. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | frege67c 40631 | Lemma for frege68c 40632. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑))) | ||
Theorem | frege68c 40632 | 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 40661 and frege109 40673. dffrege69 40633 through frege75 40639 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 40633* | 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 40634* | Lemma for frege72 40636. 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 40635* | Lemma for frege72 40636. 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 40636 | 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 40637 | Lemma for frege87 40651. 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 40638 | 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 40639* | 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 40640 through frege98 40662 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 40640* |
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 40641* | 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 40642* | Commuted form of of frege77 40641. 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 40643* | Distributed form of frege78 40642. 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 40644* | Add additional condition to both clauses of frege79 40643. 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 40645 | 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 40646 | Closed-form deduction based on frege81 40645. 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 40647 | Apply commuted form of frege81 40645 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 40648 | Commuted form of frege81 40645. 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 40649* | Commuted form of frege77 40641. 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 40650* | 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 40651* | 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 40652* | Commuted form of frege87 40651. 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 40653* | One direction of dffrege76 40640. 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 40654* | Add antecedent to frege89 40653. 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 40655 | 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 40656 | Inference from frege91 40655. 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 40657* | 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 40658* | 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 40659 | 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 40660 | 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 40661 |
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 40662 | 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 40663 through frege114 40678 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 40663 | 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 40664 | One direction of dffrege99 40663. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋)) | ||
Theorem | frege101 40665 | Lemma for frege102 40666. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ ((𝑍 = 𝑋 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → ((𝑋(t+‘𝑅)𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)))) | ||
Theorem | frege102 40666 | 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 40667 | Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((𝑍 = 𝑋 → 𝑋 = 𝑍) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍))) | ||
Theorem | frege104 40668 |
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 40669 | Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) → 𝑋((t+‘𝑅) ∪ I )𝑍) | ||
Theorem | frege106 40670 | 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 40671 | 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 40672 | 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 40673 | 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 40674* | Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑀 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀)) | ||
Theorem | frege111 40675 | 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 40676 | 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 40677 | 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 40678 | 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 40679 through frege133 40697 develop this and how functions relate to transitive and transitive-reflexive closures. | ||
Theorem | dffrege115 40679* | 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 40680* | One direction of dffrege115 40679. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 ⇒ ⊢ (Fun ◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) | ||
Theorem | frege117 40681* | Lemma for frege118 40682. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 ⇒ ⊢ ((∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)))) | ||
Theorem | frege118 40682* | Simplified application of one direction of dffrege115 40679. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) | ||
Theorem | frege119 40683* | Lemma for frege120 40684. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ ((∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋) → (𝑌𝑅𝐴 → 𝐴 = 𝑋)) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋)))) | ||
Theorem | frege120 40684 | Simplified application of one direction of dffrege115 40679. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝐴 ∈ 𝑊 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋))) | ||
Theorem | frege121 40685 | Lemma for frege122 40686. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝐴 ∈ 𝑊 ⇒ ⊢ ((𝐴 = 𝑋 → 𝑋((t+‘𝑅) ∪ I )𝐴) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝑋((t+‘𝑅) ∪ I )𝐴)))) | ||
Theorem | frege122 40686 | If 𝑋 is a result of an application of the single-valued procedure 𝑅 to 𝑌, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence beginning with 𝑋. Proposition 122 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝐴 ∈ 𝑊 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝑋((t+‘𝑅) ∪ I )𝐴))) | ||
Theorem | frege123 40687* | Lemma for frege124 40688. Proposition 123 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ ((∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀)) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀)))) | ||
Theorem | frege124 40688 | If 𝑋 is a result of an application of the single-valued procedure 𝑅 to 𝑌 and if 𝑀 follows 𝑌 in the 𝑅-sequence, then 𝑀 belongs to the 𝑅-sequence beginning with 𝑋. Proposition 124 of [Frege1879] p. 80. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀))) | ||
Theorem | frege125 40689 | Lemma for frege126 40690. Proposition 125 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ ((𝑋((t+‘𝑅) ∪ I )𝑀 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋)) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌(t+‘𝑅)𝑀 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋))))) | ||
Theorem | frege126 40690 | If 𝑀 follows 𝑌 in the 𝑅-sequence and if the procedure 𝑅 is single-valued, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence beginning with 𝑀 or precedes 𝑀 in the 𝑅-sequence. Proposition 126 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌(t+‘𝑅)𝑀 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋)))) | ||
Theorem | frege127 40691 | Communte antecedents of frege126 40690. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌(t+‘𝑅)𝑀 → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋)))) | ||
Theorem | frege128 40692 | Lemma for frege129 40693. Proposition 128 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ ((𝑀((t+‘𝑅) ∪ I )𝑌 → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋))) → (Fun ◡◡𝑅 → ((¬ 𝑌(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑌) → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋))))) | ||
Theorem | frege129 40693 | If the procedure 𝑅 is single-valued and 𝑌 belongs to the 𝑅 -sequence begining with 𝑀 or precedes 𝑀 in the 𝑅-sequence, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence begining with 𝑀 or precedes 𝑀 in the 𝑅-sequence. Proposition 129 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → ((¬ 𝑌(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑌) → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋)))) | ||
Theorem | frege130 40694* | Lemma for frege131 40695. Proposition 130 of [Frege1879] p. 84. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑀 ∈ 𝑈 & ⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ ((∀𝑏((¬ 𝑏(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑏) → ∀𝑎(𝑏𝑅𝑎 → (¬ 𝑎(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑎))) → 𝑅 hereditary ((◡(t+‘𝑅) “ {𝑀}) ∪ (((t+‘𝑅) ∪ I ) “ {𝑀}))) → (Fun ◡◡𝑅 → 𝑅 hereditary ((◡(t+‘𝑅) “ {𝑀}) ∪ (((t+‘𝑅) ∪ I ) “ {𝑀})))) | ||
Theorem | frege131 40695 | If the procedure 𝑅 is single-valued, then the property of belonging to the 𝑅-sequence begining with 𝑀 or preceeding 𝑀 in the 𝑅-sequence is hereditary in the 𝑅-sequence. Proposition 131 of [Frege1879] p. 85. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑀 ∈ 𝑈 & ⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ (Fun ◡◡𝑅 → 𝑅 hereditary ((◡(t+‘𝑅) “ {𝑀}) ∪ (((t+‘𝑅) ∪ I ) “ {𝑀}))) | ||
Theorem | frege132 40696 | Lemma for frege133 40697. Proposition 132 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑀 ∈ 𝑈 & ⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ ((𝑅 hereditary ((◡(t+‘𝑅) “ {𝑀}) ∪ (((t+‘𝑅) ∪ I ) “ {𝑀})) → (𝑋(t+‘𝑅)𝑀 → (𝑋(t+‘𝑅)𝑌 → (¬ 𝑌(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑌)))) → (Fun ◡◡𝑅 → (𝑋(t+‘𝑅)𝑀 → (𝑋(t+‘𝑅)𝑌 → (¬ 𝑌(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑌))))) | ||
Theorem | frege133 40697 | If the procedure 𝑅 is single-valued and if 𝑀 and 𝑌 follow 𝑋 in the 𝑅-sequence, then 𝑌 belongs to the 𝑅-sequence beginning with 𝑀 or precedes 𝑀 in the 𝑅-sequence. Proposition 133 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑋(t+‘𝑅)𝑀 → (𝑋(t+‘𝑅)𝑌 → (¬ 𝑌(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑌)))) | ||
See Seifert and Threlfall: A Textbook Of Topology (1980) which is an English translation of Lehrbuch der Topologie (1934). | ||
Because ((2o ↑m 𝐵) ↑m 𝐴) ≈ (2o ↑m (𝐴 × 𝐵)) ≈ ((2o ↑m 𝐴) ↑m 𝐵) is an instance of the law of exponents: ((𝐶 ↑m 𝐵) ↑m 𝐴) ≈ (𝐶 ↑m (𝐴 × 𝐵)) ≈ ((𝐶 ↑m 𝐴) ↑m 𝐵) we are led to see that (𝒫 𝐵 ↑m 𝐴) ≈ 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐴 ↑m 𝐵) is true for any two sets, 𝐴 and 𝐵, and thus there exist one-to-one onto relations between each of these three sets of relations. | ||
Theorem | enrelmap 40698 | The set of all possible relations between two sets is equinumerous to the set of all mappings from one set to the powerset of the other. See rfovf1od 40707 for a demonstration of a natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐵 ↑m 𝐴)) | ||
Theorem | enrelmapr 40699 | The set of all possible relations between two sets is equinumerous to the set of all mappings from one set to the powerset of the other. (Contributed by RP, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐴 ↑m 𝐵)) | ||
Theorem | enmappw 40700 | The set of all mappings from one set to the powerset of the other is equinumerous to the set of all mappings from the second set to the powerset of the first. (Contributed by RP, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐵 ↑m 𝐴) ≈ (𝒫 𝐴 ↑m 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |