P. 452 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45101-45200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frege64b 45101	Lemma for frege65b 45102. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒)))
Theorem	frege65b 45102	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2690 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 45103	Swap antecedents of frege65b 45102. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓)))
Theorem	frege67b 45104	Lemma for frege68b 45105. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑)))
Theorem	frege68b 45105	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.)
⊢ ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑))
21.40.6.7  _Begriffsschrift_ Chapter II with equivalence of classes Begriffsschrift Chapter II with equivalence of classes (where they are sets).
Theorem	frege53c 45106	Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑))
Theorem	frege54cor1c 45107*	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.)
⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ [𝐴 / 𝑥]𝑥 = 𝐴
Theorem	frege55lem1c 45108*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵))
Theorem	frege55lem2c 45109*	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥)
Theorem	frege55c 45110	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥)
Theorem	frege56c 45111*	Lemma for frege57c 45112. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)))
Theorem	frege57c 45112*	Swap order of implication in ax-frege52c 45080. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑))
Theorem	frege58c 45113	Principle related to sp 2223. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)
Theorem	frege59c 45114	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 45005 incorrectly referenced where frege30 45024 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓)))
Theorem	frege60c 45115	Swap antecedents of frege58c 45113. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒)))
Theorem	frege61c 45116	Lemma for frege65c 45120. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	frege62c 45117	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2690 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 45118	Analogue of frege63b 45100. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒)))
Theorem	frege64c 45119	Lemma for frege65c 45120. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒)))
Theorem	frege65c 45120	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2690 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 45121	Swap antecedents of frege65c 45120. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓)))
Theorem	frege67c 45122	Lemma for frege68c 45123. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑)))
Theorem	frege68c 45123	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.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑))
21.40.6.8  _Begriffsschrift_ Chapter III Properties hereditary in a sequence (𝑅 “ 𝐴) ⊆ 𝐴 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 45152 and frege109 45164. dffrege69 45124 through frege75 45130 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 45124*	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 45125*	Lemma for frege72 45127. 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 45126*	Lemma for frege72 45127. 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 45127	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 45128	Lemma for frege87 45142. 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 45129	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 45130*	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 𝐴)
21.40.6.9  _Begriffsschrift_ Chapter III Following in a sequence 𝑝(t+‘𝑅)𝑐 means 𝑐 follows 𝑝 in the 𝑅-sequence. dffrege76 45131 through frege98 45153 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 45131*	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 45132*	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 45133*	Commuted form of frege77 45132. 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 45134*	Distributed form of frege78 45133. 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 45135*	Add additional condition to both clauses of frege79 45134. 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 45136	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 45137	Closed-form deduction based on frege81 45136. 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 45138	Apply commuted form of frege81 45136 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 45139	Commuted form of frege81 45136. 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 45140*	Commuted form of frege77 45132. 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 45141*	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 45142*	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 45143*	Commuted form of frege87 45142. 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 45144*	One direction of dffrege76 45131. 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 45145*	Add antecedent to frege89 45144. 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 45146	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 45147	Inference from frege91 45146. 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 45148*	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 45149*	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 45150	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 45151	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 45152	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 45153	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+‘𝑅)𝑍))
21.40.6.10  _Begriffsschrift_ Chapter III Member of sequence 𝑝((t+‘𝑅) ∪ I )𝑐 means 𝑐 is a member of the 𝑅 -sequence beginning with 𝑝 and 𝑝 is a member of the 𝑅 -sequence ending with 𝑐. dffrege99 45154 through frege114 45169 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 45154	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 45155	One direction of dffrege99 45154. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑍 ∈ 𝑈    ⇒   ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋))
Theorem	frege101 45156	Lemma for frege102 45157. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑍 ∈ 𝑈    ⇒   ⊢ ((𝑍 = 𝑋 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → ((𝑋(t+‘𝑅)𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉))))
Theorem	frege102 45157	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 45158	Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑍 ∈ 𝑉    ⇒   ⊢ ((𝑍 = 𝑋 → 𝑋 = 𝑍) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍)))
Theorem	frege104 45159	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 45160	Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑍 ∈ 𝑉    ⇒   ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) → 𝑋((t+‘𝑅) ∪ I )𝑍)
Theorem	frege106 45161	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 45162	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 45163	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 45164	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 45165*	Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝐴    &   ⊢ 𝑌 ∈ 𝐵    &   ⊢ 𝑀 ∈ 𝐶    &   ⊢ 𝑅 ∈ 𝐷    ⇒   ⊢ (∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀))
Theorem	frege111 45166	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 45167	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 45168	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 45169	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 )𝑍))
21.40.6.11  _Begriffsschrift_ Chapter III Single-valued procedures Fun ◡◡𝑅 means the relationship content of procedure 𝑅 is single-valued. The double converse allows 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 45170 through frege133 45188 develop this and how functions relate to transitive and transitive-reflexive closures.
Theorem	dffrege115 45170*	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 45171*	One direction of dffrege115 45170. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    ⇒   ⊢ (Fun ◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)))
Theorem	frege117 45172*	Lemma for frege118 45173. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    ⇒   ⊢ ((∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))))
Theorem	frege118 45173*	Simplified application of one direction of dffrege115 45170. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)))
Theorem	frege119 45174*	Lemma for frege120 45175. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ ((∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋) → (𝑌𝑅𝐴 → 𝐴 = 𝑋)) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋))))
Theorem	frege120 45175	Simplified application of one direction of dffrege115 45170. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝐴 ∈ 𝑊    ⇒   ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋)))
Theorem	frege121 45176	Lemma for frege122 45177. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝐴 ∈ 𝑊    ⇒   ⊢ ((𝐴 = 𝑋 → 𝑋((t+‘𝑅) ∪ I )𝐴) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝑋((t+‘𝑅) ∪ I )𝐴))))
Theorem	frege122 45177	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 45178*	Lemma for frege124 45179. 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 45179	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 45180	Lemma for frege126 45181. 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 45181	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 45182	Communte antecedents of frege126 45181. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑀 ∈ 𝑊    &   ⊢ 𝑅 ∈ 𝑆    ⇒   ⊢ (Fun ◡◡𝑅 → (𝑌(t+‘𝑅)𝑀 → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋))))
Theorem	frege128 45183	Lemma for frege129 45184. 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 45184	If the procedure 𝑅 is single-valued and 𝑌 belongs to the 𝑅 -sequence beginning with 𝑀 or precedes 𝑀 in the 𝑅-sequence, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence beginning 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 45185*	Lemma for frege131 45186. 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 45186	If the procedure 𝑅 is single-valued, then the property of belonging to the 𝑅-sequence beginning 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 45187	Lemma for frege133 45188. 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 45188	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 )𝑌))))
21.40.7  Exploring Topology via Seifert and Threlfall See Seifert and Threlfall: A Textbook Of Topology (1980) which is an English translation of Lehrbuch der Topologie (1934).
21.40.7.1  Equinumerosity of sets of relations and maps 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 45189	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 45198 for a demonstration of a natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐵 ↑m 𝐴))
Theorem	enrelmapr 45190	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 45191	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 𝐵))
Theorem	enmappwid 45192	The set of all mappings from the powerset to the powerset is equinumerous to the set of all mappings from the set to the powerset of the powerset. (Contributed by RP, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑m 𝒫 𝐴) ≈ (𝒫 𝒫 𝐴 ↑m 𝐴))
Theorem	rfovd 45193*	Value of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 25-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))
Theorem	rfovfvd 45194*	Value of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, and relation 𝑅. (Contributed by RP, 25-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝒫 (𝐴 × 𝐵))    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝑅) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑅𝑦}))
Theorem	rfovfvfvd 45195*	Value of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, relation 𝑅, and left element 𝑋. (Contributed by RP, 25-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝒫 (𝐴 × 𝐵))    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ 𝐺 = (𝐹‘𝑅)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) = {𝑦 ∈ 𝐵 ∣ 𝑋𝑅𝑦})
Theorem	rfovcnvf1od 45196*	Properties of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 27-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝒫 (𝐴 × 𝐵)⟶1-1onto(𝒫 𝐵 ↑m 𝐴) ∧ ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))
Theorem	rfovcnvd 45197*	Value of the converse of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵. (Contributed by RP, 27-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → ◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}))
Theorem	rfovf1od 45198*	The value of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, is a bijection. (Contributed by RP, 27-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝒫 (𝐴 × 𝐵)⟶1-1onto(𝒫 𝐵 ↑m 𝐴))
Theorem	rfovcnvfvd 45199*	Value of the converse of the operator, (𝐴𝑂𝐵), which maps between relations and functions for relations between base sets, 𝐴 and 𝐵, evaluated at function 𝐺. (Contributed by RP, 27-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑥 ∈ 𝑎 ↦ {𝑦 ∈ 𝑏 ∣ 𝑥𝑟𝑦})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝒫 𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → (◡𝐹‘𝐺) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐺‘𝑥))})
Theorem	fsovd 45200*	Value of the operator, (𝐴𝑂𝐵), which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, 𝐴 and 𝐵. (Contributed by RP, 25-Apr-2021.)
⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴𝑂𝐵) = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))