P. 442 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44101-44200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frege54cor1a 44101	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	frege55aid 44102	Lemma for frege57aid 44109. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	frege55lem1a 44103	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑)))
Theorem	frege55lem2a 44104	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	frege55a 44105	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	frege55cor1a 44106	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	frege56aid 44107	Lemma for frege57aid 44109. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓)))
Theorem	frege56a 44108	Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))))
Theorem	frege57aid 44109	This is the all important formula which allows to apply Frege-style definitions and explore their consequences. A closed form of biimpri 228. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
Theorem	frege57a 44110	Analogue of frege57aid 44109. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)))
Theorem	axfrege58a 44111	Identical to anifp 1071. Justification for ax-frege58a 44112. (Contributed by RP, 28-Mar-2020.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Axiom	ax-frege58a 44112	If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Theorem	frege58acor 44113	Lemma for frege59a 44114. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	frege59a 44114	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 44050 incorrectly referenced where frege30 44069 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏))))
Theorem	frege60a 44115	Swap antecedents of ax-frege58a 44112. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁))))
Theorem	frege61a 44116	Lemma for frege65a 44120. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	frege62a 44117	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44118	Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏))))
Theorem	frege64a 44119	Lemma for frege65a 44120. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁))))
Theorem	frege65a 44120	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44121	Swap antecedents of frege65a 44120. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁))))
Theorem	frege67a 44122	Lemma for frege68a 44123. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒))))
Theorem	frege68a 44123	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-(𝜑, 𝜓, 𝜒)))
21.36.6.6  _Begriffsschrift_ Chapter II with equivalence of sets
Theorem	axfrege52c 44124	Justification for ax-frege52c 44125. (Contributed by RP, 24-Dec-2019.)
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))
Axiom	ax-frege52c 44125	One side of dfsbcq 3742. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))
Theorem	frege52b 44126	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 44127	Lemma for frege102 (via frege92 44192). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑))
Theorem	axfrege54c 44128	Reflexive equality of classes. Identical to eqid 2736. Justification for ax-frege54c 44129. (Contributed by RP, 24-Dec-2019.)
⊢ 𝐴 = 𝐴
Axiom	ax-frege54c 44129	Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2736. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ 𝐴 = 𝐴
Theorem	frege54b 44130	Reflexive equality of sets. The content of 𝑥 is identical with the content of 𝑥. Part of Axiom 54 of [Frege1879] p. 50. Slightly specialized version of eqid 2736. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	frege54cor1b 44131	Reflexive equality. (Contributed by RP, 24-Dec-2019.)
⊢ [𝑥 / 𝑦]𝑦 = 𝑥
Theorem	frege55lem1b 44132*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧))
Theorem	frege55lem2b 44133	Lemma for frege55b 44134. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
Theorem	frege55b 44134	Lemma for frege57b 44136. Proposition 55 of [Frege1879] p. 50. Note that eqtr2 2757 incorporates eqcom 2743 which is stronger than this proposition which is identical to equcomi 2018. Is it possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	frege56b 44135	Lemma for frege57b 44136. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) → (𝑦 = 𝑥 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)))
Theorem	frege57b 44136	Analogue of frege57aid 44109. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
Theorem	axfrege58b 44137	If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2073. Justification for ax-frege58b 44138. (Contributed by RP, 28-Mar-2020.)
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
Axiom	ax-frege58b 44138	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 44139	If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2190. See ax-frege58b 44138 and frege58c 44158 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 44140	Lemma for frege59b 44141. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	frege59b 44141	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 44050 incorrectly referenced where frege30 44069 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓)))
Theorem	frege60b 44142	Swap antecedents of ax-frege58b 44138. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒)))
Theorem	frege61b 44143	Lemma for frege65b 44147. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓))
Theorem	frege62b 44144	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44145	Lemma for frege91 44191. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝑦 / 𝑥]𝜒)))
Theorem	frege64b 44146	Lemma for frege65b 44147. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜓) → (∀𝑦(𝜓 → 𝜒) → ([𝑥 / 𝑦]𝜑 → [𝑧 / 𝑦]𝜒)))
Theorem	frege65b 44147	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44148	Swap antecedents of frege65b 44147. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝑦 / 𝑥]𝜒 → [𝑦 / 𝑥]𝜓)))
Theorem	frege67b 44149	Lemma for frege68b 44150. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝑦 / 𝑥]𝜑)))
Theorem	frege68b 44150	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.36.6.7  _Begriffsschrift_ Chapter II with equivalence of classes Begriffsschrift Chapter II with equivalence of classes (where they are sets).
Theorem	frege53c 44151	Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝐴 / 𝑥]𝜑 → (𝐴 = 𝐵 → [𝐵 / 𝑥]𝜑))
Theorem	frege54cor1c 44152*	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.)
⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ [𝐴 / 𝑥]𝑥 = 𝐴
Theorem	frege55lem1c 44153*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → [𝐴 / 𝑥]𝑥 = 𝐵) → (𝜑 → 𝐴 = 𝐵))
Theorem	frege55lem2c 44154*	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥)
Theorem	frege55c 44155	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐴 = 𝑥)
Theorem	frege56c 44156*	Lemma for frege57c 44157. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ ((𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) → (𝐵 = 𝐴 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)))
Theorem	frege57c 44157*	Swap order of implication in ax-frege52c 44125. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ (𝐴 = 𝐵 → ([𝐵 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜑))
Theorem	frege58c 44158	Principle related to sp 2190. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑)
Theorem	frege59c 44159	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 44050 incorrectly referenced where frege30 44069 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → (¬ [𝐴 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓)))
Theorem	frege60c 44160	Swap antecedents of frege58c 44158. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜓 → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒)))
Theorem	frege61c 44161	Lemma for frege65c 44165. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	frege62c 44162	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44163	Analogue of frege63b 44145. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒)))
Theorem	frege64c 44164	Lemma for frege65c 44165. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒)))
Theorem	frege65c 44165	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 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 44166	Swap antecedents of frege65c 44165. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓)))
Theorem	frege67c 44167	Lemma for frege68c 44168. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑)))
Theorem	frege68c 44168	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.36.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 44197 and frege109 44209. dffrege69 44169 through frege75 44175 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 44169*	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 44170*	Lemma for frege72 44172. 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 44171*	Lemma for frege72 44172. 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 44172	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 44173	Lemma for frege87 44187. 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 44174	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 44175*	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.36.6.9  _Begriffsschrift_ Chapter III Following in a sequence 𝑝(t+‘𝑅)𝑐 means 𝑐 follows 𝑝 in the 𝑅-sequence. dffrege76 44176 through frege98 44198 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 44176*	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 44177*	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 44178*	Commuted form of frege77 44177. 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 44179*	Distributed form of frege78 44178. 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 44180*	Add additional condition to both clauses of frege79 44179. 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 44181	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 44182	Closed-form deduction based on frege81 44181. 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 44183	Apply commuted form of frege81 44181 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 44184	Commuted form of frege81 44181. 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 44185*	Commuted form of frege77 44177. 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 44186*	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 44187*	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 44188*	Commuted form of frege87 44187. 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 44189*	One direction of dffrege76 44176. 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 44190*	Add antecedent to frege89 44189. 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 44191	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 44192	Inference from frege91 44191. 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 44193*	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 44194*	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 44195	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 44196	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 44197	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 44198	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.36.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 44199 through frege114 44214 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 44199	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 44200	One direction of dffrege99 44199. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
⊢ 𝑍 ∈ 𝑈    ⇒   ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋))