P. 438 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43701-43800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iunrelexpmin2 43701*	The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0) → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠))
Theorem	relexp01min 43702	With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))
Theorem	relexp1idm 43703	Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.)
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1)↑𝑟1) = (𝑅↑𝑟1))
Theorem	relexp0idm 43704	Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.)
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟0)↑𝑟0) = (𝑅↑𝑟0))
Theorem	relexp0a 43705	Absorption law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0))
Theorem	relexpxpmin 43706	The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼))
Theorem	relexpaddss 43707	The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where 𝑅 is a relation as shown by relexpaddd 15089 or when the sum of the powers isn't 1 as shown by relexpaddg 15088. (Contributed by RP, 3-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ⊆ (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	iunrelexpuztr 43708*	The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 15095. (Contributed by RP, 4-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = (ℤ≥‘𝑀) ∧ 𝑀 ∈ ℕ0) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅))
21.36.5.4  Transitive closure of a relation
Theorem	dftrcl3 43709*	Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.)
⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛))
Theorem	brfvtrcld 43710*	If two elements are connected by the transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some counting number 𝑛. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvtrcllb1d 43711	A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcom 43712	The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (𝑅 ∘ (t+‘𝑅)))
Theorem	cnvtrclfv 43713	The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ◡(t+‘𝑅) = (t+‘◡𝑅))
Theorem	cotrcltrcl 43714	The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.)
⊢ (t+ ∘ t+) = t+
Theorem	trclimalb2 43715	Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 “ (𝐴 ∪ 𝐵)) ⊆ 𝐵) → ((t+‘𝑅) “ 𝐴) ⊆ 𝐵)
Theorem	brtrclfv2 43716*	Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋(t+‘𝑅)𝑌 ↔ 𝑌 ∈ ∩ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓}))
Theorem	trclfvdecomr 43717	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))
Theorem	trclfvdecoml 43718	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ (𝑅 ∘ (t+‘𝑅))))
Theorem	dmtrclfvRP 43719	The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅)
Theorem	rntrclfvRP 43720	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
Theorem	rntrclfv 43721	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
Theorem	dfrtrcl3 43722*	Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 15097. (Contributed by RP, 5-Jun-2020.)
⊢ t* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))
Theorem	brfvrtrcld 43723*	If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some natural number 𝑛. Similar of dfrtrclrec2 15093. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝐴(t*‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvrtrcllb0d 43724	A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*‘𝑅))
Theorem	fvrtrcllb0da 43725	A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*‘𝑅))
Theorem	fvrtrcllb1d 43726	A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (t*‘𝑅))
Theorem	dfrtrcl4 43727	Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.)
⊢ t* = (𝑟 ∈ V ↦ ((𝑟↑𝑟0) ∪ (t+‘𝑟)))
Theorem	corcltrcl 43728	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.)
⊢ (r* ∘ t+) = t*
Theorem	cortrcltrcl 43729	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ t+) = t*
Theorem	corclrtrcl 43730	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (r* ∘ t*) = t*
Theorem	cotrclrcl 43731	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.)
⊢ (t+ ∘ r*) = t*
Theorem	cortrclrcl 43732	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ r*) = t*
Theorem	cotrclrtrcl 43733	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
⊢ (t+ ∘ t*) = t*
Theorem	cortrclrtrcl 43734	The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020.)
⊢ (t* ∘ t*) = t*
21.36.5.5  Adapted from Frege Theorems inspired by Begriffsschrift without restricting form and content to closely parallel those in [Frege1879].
Theorem	frege77d 43735	If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 77 of [Frege1879] p. 62. Compare with frege77 43929. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    &   ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege81d 43736	If the image of 𝑈 is a subset 𝑈, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 81 of [Frege1879] p. 63. Compare with frege81 43933. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege83d 43737	If the image of the union of 𝑈 and 𝑉 is a subset of the union of 𝑈 and 𝑉, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of the union of 𝑈 and 𝑉. Similar to Proposition 83 of [Frege1879] p. 65. Compare with frege83 43935. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)    &   ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑉)) ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑉))
Theorem	frege96d 43738	If 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 96 of [Frege1879] p. 71. Compare with frege96 43948. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege87d 43739	If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 87 of [Frege1879] p. 66. Compare with frege87 43939. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    &   ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈)    &   ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	frege91d 43740	If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 43943. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege97d 43741	If 𝐴 contains all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴. Similar to Proposition 97 of [Frege1879] p. 71. Compare with frege97 43949. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 = ((t+‘𝑅) “ 𝑈))    ⇒   ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
Theorem	frege98d 43742	If 𝐶 follows 𝐴 and 𝐵 follows 𝐶 in the transitive closure of 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 98 of [Frege1879] p. 71. Compare with frege98 43950. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶)    &   ⊢ (𝜑 → 𝐶(t+‘𝑅)𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege102d 43743	If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 102 of [Frege1879] p. 72. Compare with frege102 43954. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶))    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵)
Theorem	frege106d 43744	If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅. Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 43958. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege108d 43745	If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 108 of [Frege1879] p. 74. Compare with frege108 43960. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶))    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege109d 43746	If 𝐴 contains all elements of 𝑈 and all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴. Similar to Proposition 109 of [Frege1879] p. 74. Compare with frege109 43961. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((t+‘𝑅) “ 𝑈)))    ⇒   ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴)
Theorem	frege114d 43747	If either 𝑅 relates 𝐴 and 𝐵 or 𝐴 and 𝐵 are the same, then either 𝐴 and 𝐵 are the same, 𝑅 relates 𝐴 and 𝐵, 𝑅 relates 𝐵 and 𝐴. Similar to Proposition 114 of [Frege1879] p. 76. Compare with frege114 43966. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴))
Theorem	frege111d 43748	If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐴 follows 𝐵 or 𝐵 and 𝐴 in the transitive closure of 𝑅. Similar to Proposition 111 of [Frege1879] p. 75. Compare with frege111 43963. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶))    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝑅)𝐴))
Theorem	frege122d 43749	If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 is the successor of 𝑋, then 𝐴 and 𝐵 are the same (or 𝐵 follows 𝐴 in the transitive closure of 𝐹). Similar to Proposition 122 of [Frege1879] p. 79. Compare with frege122 43974. (Contributed by RP, 15-Jul-2020.)
⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))    &   ⊢ (𝜑 → 𝐵 = (𝐹‘𝑋))    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege124d 43750	If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝐹. Similar to Proposition 124 of [Frege1879] p. 80. Compare with frege124 43976. (Contributed by RP, 16-Jul-2020.)
⊢ (𝜑 → 𝐹 ∈ V)    &   ⊢ (𝜑 → 𝑋 ∈ dom 𝐹)    &   ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))    &   ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵))
Theorem	frege126d 43751	If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹. Similar to Proposition 126 of [Frege1879] p. 81. Compare with frege126 43978. (Contributed by RP, 16-Jul-2020.)
⊢ (𝜑 → 𝐹 ∈ V)    &   ⊢ (𝜑 → 𝑋 ∈ dom 𝐹)    &   ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋))    &   ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴))
Theorem	frege129d 43752	If 𝐹 is a function and (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹, the successor of 𝐴 is either 𝐵 or it follows 𝐵 or it comes before 𝐵 in the transitive closure of 𝐹. Similar to Proposition 129 of [Frege1879] p. 83. Comparw with frege129 43981. (Contributed by RP, 16-Jul-2020.)
⊢ (𝜑 → 𝐹 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝐹)    &   ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴))    &   ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴))    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵))
Theorem	frege131d 43753	If 𝐹 is a function and 𝐴 contains all elements of 𝑈 and all elements before or after those elements of 𝑈 in the transitive closure of 𝐹, then the image under 𝐹 of 𝐴 is a subclass of 𝐴. Similar to Proposition 131 of [Frege1879] p. 85. Compare with frege131 43983. (Contributed by RP, 17-Jul-2020.)
⊢ (𝜑 → 𝐹 ∈ V)    &   ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈))))    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴)
Theorem	frege133d 43754	If 𝐹 is a function and 𝐴 and 𝐵 both follow 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹 (or both if it loops). Similar to Proposition 133 of [Frege1879] p. 86. Compare with frege133 43985. (Contributed by RP, 18-Jul-2020.)
⊢ (𝜑 → 𝐹 ∈ V)    &   ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐴)    &   ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴))
21.36.6  Propositions from _Begriffsschrift_ In 1879, Frege introduced notation for documenting formal reasoning about propositions (and classes) which covered elements of propositional logic, predicate calculus and reasoning about relations. However, due to the pitfalls of naive set theory, adapting this work for inclusion in set.mm required dividing statements about propositions from those about classes and identifying when a restriction to sets is required. For an overview comparing the details of Frege's two-dimensional notation and that used in set.mm, see mmfrege.html. See ru 3788 for discussion of an example of a class that is not a set. Numbered propositions from [Frege1879]. ax-frege1 43779, ax-frege2 43780, ax-frege8 43798, ax-frege28 43819, ax-frege31 43823, ax-frege41 43834, frege52 (see ax-frege52a 43846, frege52b 43878, and ax-frege52c 43877 for translations), frege54 (see ax-frege54a 43851, frege54b 43882 and ax-frege54c 43881 for translations) and frege58 (see ax-frege58a 43864, ax-frege58b 43890 and frege58c 43910 for translations) are considered "core" or axioms. However, at least ax-frege8 43798 can be derived from ax-frege1 43779 and ax-frege2 43780, see axfrege8 43796. Frege introduced implication, negation and the universal quantifier as primitives and did not in the numbered propositions use other logical connectives other than equivalence introduced in ax-frege52a 43846, frege52b 43878, and ax-frege52c 43877. In dffrege69 43921, Frege introduced 𝑅 hereditary 𝐴 to say that relation 𝑅, when restricted to operate on elements of class 𝐴, will only have elements of class 𝐴 in its domain; see df-he 43762 for a definition in terms of image and subset. In dffrege76 43928, Frege introduced notation for the concept of two sets related by the transitive closure of a relation, for which we write 𝑋(t+‘𝑅)𝑌, which requires 𝑅 to also be a set. In dffrege99 43951, Frege introduced notation for the concept of two sets either identical or related by the transitive closure of a relation, for which we write 𝑋((t+‘𝑅) ∪ I )𝑌, which is a superclass of sets related by the reflexive-transitive relation 𝑋(t*‘𝑅)𝑌. Finally, in dffrege115 43967, Frege introduced notation for the concept of a relation having the property elements in its domain pair up with only one element each in its range, for which we write Fun ◡◡𝑅 (to ignore any non-relational content of the class 𝑅). Frege did this without the expressing concept of a relation (or its transitive closure) as a class, and needed to invent conventions for discussing indeterminate propositions with two slots free and how to recognize which of the slots was domain and which was range. See mmfrege.html 43967 for details. English translations for specific propositions lifted in part from a translation by Stefan Bauer-Mengelberg as reprinted in From Frege to Goedel: A Source Book in Mathematical Logic, 1879-1931. An attempt to align these propositions in the larger set.mm database has also been made. See frege77d 43735 for an example.
21.36.6.1  _Begriffsschrift_ Chapter I Section 2 introduces the turnstile ⊢ which turns an idea which may be true 𝜑 into an assertion that it does hold true ⊢ 𝜑. Section 5 introduces implication, (𝜑 → 𝜓). Section 6 introduces the single rule of interference relied upon, modus ponens ax-mp 5. Section 7 introduces negation and with in synonyms for or (¬ 𝜑 → 𝜓) , and ¬ (𝜑 → ¬ 𝜓), and two for exclusive-or corresponding to df-or 848, df-an 396, dfxor4 43755, dfxor5 43756. Section 8 introduces the problematic notation for identity of conceptual content which must be separated into cases for biconditional (𝜑 ↔ 𝜓) or class equality 𝐴 = 𝐵 in this adaptation. Section 10 introduces "truth functions" for one or two variables in equally troubling notation, as the arguments may be understood to be logical predicates or collections. Here f(𝜑) is interpreted to mean if-(𝜑, 𝜓, 𝜒) where the content of the "function" is specified by the latter two arguments or logical equivalent, while g(𝐴) is read as 𝐴 ∈ 𝐺 and h(𝐴, 𝐵) as 𝐴𝐻𝐵. This necessarily introduces a need for set theory as both 𝐴 ∈ 𝐺 and 𝐴𝐻𝐵 cannot hold unless 𝐴 is a set. (Also 𝐵.) Section 11 introduces notation for generality, but there is no standard notation for generality when the variable is a proposition because it was realized after Frege that the universe of all possible propositions includes paradoxical constructions leading to the failure of naive set theory. So adopting f(𝜑) as if-(𝜑, 𝜓, 𝜒) would result in the translation of ∀𝜑 f (𝜑) as (𝜓 ∧ 𝜒). For collections, we must generalize over set variables or run into the same problems; this leads to ∀𝐴 g(𝐴) being translated as ∀𝑎𝑎 ∈ 𝐺 and so forth. Under this interpreation the text of section 11 gives us sp 2180 (or simpl 482 and simpr 484 and anifp 1071 in the propositional case) and statements similar to cbvalivw 2003, ax-gen 1791, alrimiv 1924, and alrimdv 1926. These last four introduce a generality and have no useful definition in terms of propositional variables. Section 12 introduces some combinations of primitive symbols and their human language counterparts. Using class notation, these can also be expressed without dummy variables. All are A, ∀𝑥𝑥 ∈ 𝐴, ¬ ∃𝑥¬ 𝑥 ∈ 𝐴 alex 1822, 𝐴 = V eqv 3487; Some are not B, ¬ ∀𝑥𝑥 ∈ 𝐵, ∃𝑥¬ 𝑥 ∈ 𝐵 exnal 1823, 𝐵 ⊊ V pssv 4454, 𝐵 ≠ V nev 43759; There are no C, ∀𝑥¬ 𝑥 ∈ 𝐶, ¬ ∃𝑥𝑥 ∈ 𝐶 alnex 1777, 𝐶 = ∅ eq0 4355; There exist D, ¬ ∀𝑥¬ 𝑥 ∈ 𝐷, ∃𝑥𝑥 ∈ 𝐷 df-ex 1776, ∅ ⊊ 𝐷 0pss 4452, 𝐷 ≠ ∅ n0 4358. Notation for relations between expressions also can be written in various ways. All E are P, ∀𝑥(𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑃), ¬ ∃𝑥(𝑥 ∈ 𝐸 ∧ ¬ 𝑥 ∈ 𝑃) dfss6 3984, 𝐸 = (𝐸 ∩ 𝑃) dfss2 3980, 𝐸 ⊆ 𝑃 df-ss 3979; No F are P, ∀𝑥(𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑃), ¬ ∃𝑥(𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝑃) alinexa 1839, (𝐹 ∩ 𝑃) = ∅ disj1 4457; Some G are not P, ¬ ∀𝑥(𝑥 ∈ 𝐺 → 𝑥 ∈ 𝑃), ∃𝑥(𝑥 ∈ 𝐺 ∧ ¬ 𝑥 ∈ 𝑃) exanali 1856, (𝐺 ∩ 𝑃) ⊊ 𝐺 nssinpss 4272, ¬ 𝐺 ⊆ 𝑃 nss 4059; Some H are P, ¬ ∀𝑥(𝑥 ∈ 𝐻 → ¬ 𝑥 ∈ 𝑃), ∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑥 ∈ 𝑃) exnalimn 1840, ∅ ⊊ (𝐻 ∩ 𝑃) 0pssin 43760, (𝐻 ∩ 𝑃) ≠ ∅ ndisj 4375.
Theorem	dfxor4 43755	Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ ((¬ 𝜑 → 𝜓) → ¬ (𝜑 → ¬ 𝜓)))
Theorem	dfxor5 43756	Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓)))
Theorem	df3or2 43757	Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 → (¬ 𝜓 → 𝜒)))
Theorem	df3an2 43758	Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (𝜑 → (𝜓 → ¬ 𝜒)))
Theorem	nev 43759*	Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.)
⊢ (𝐴 ≠ V ↔ ¬ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	0pssin 43760*	Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.)
⊢ (∅ ⊊ (𝐴 ∩ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
21.36.6.2  _Begriffsschrift_ Notation hints The statement 𝑅 hereditary 𝐴 means relation 𝑅 is hereditary (in the sense of Frege) in the class 𝐴 or (𝑅 “ 𝐴) ⊆ 𝐴. The former is only a slight reduction in the number of symbols, but this reduces the number of floating hypotheses needed to be checked. As Frege was not using the language of classes or sets, this naturally 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.
Syntax	whe 43761	The property of relation 𝑅 being hereditary in class 𝐴.
wff 𝑅 hereditary 𝐴
Definition	df-he 43762	The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.)
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 “ 𝐴) ⊆ 𝐴)
Theorem	dfhe2 43763	The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.)
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐴))
Theorem	dfhe3 43764*	The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.)
⊢ (𝑅 hereditary 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑥𝑅𝑦 → 𝑦 ∈ 𝐴)))
Theorem	heeq12 43765	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐵))
Theorem	heeq1 43766	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
⊢ (𝑅 = 𝑆 → (𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐴))
Theorem	heeq2 43767	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
⊢ (𝐴 = 𝐵 → (𝑅 hereditary 𝐴 ↔ 𝑅 hereditary 𝐵))
Theorem	sbcheg 43768	Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 hereditary 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 hereditary ⦋𝐴 / 𝑥⦌𝐶))
Theorem	hess 43769	Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
⊢ (𝑆 ⊆ 𝑅 → (𝑅 hereditary 𝐴 → 𝑆 hereditary 𝐴))
Theorem	xphe 43770	Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (𝐴 × 𝐵) hereditary 𝐵
Theorem	0he 43771	The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.)
⊢ ∅ hereditary 𝐴
Theorem	0heALT 43772	The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∅ hereditary 𝐴
Theorem	he0 43773	Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020.)
⊢ 𝐴 hereditary ∅
Theorem	unhe1 43774	The union of two relations hereditary in a class is also hereditary in a class. (Contributed by RP, 28-Mar-2020.)
⊢ ((𝑅 hereditary 𝐴 ∧ 𝑆 hereditary 𝐴) → (𝑅 ∪ 𝑆) hereditary 𝐴)
Theorem	snhesn 43775	Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020.)
⊢ {⟨𝐴, 𝐴⟩} hereditary {𝐵}
Theorem	idhe 43776	The identity relation is hereditary in any class. (Contributed by RP, 28-Mar-2020.)
⊢ I hereditary 𝐴
Theorem	psshepw 43777	The relation between sets and their proper subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.)
⊢ ◡ [⊊] hereditary 𝒫 𝐴
Theorem	sshepw 43778	The relation between sets and their subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.)
⊢ (◡ [⊊] ∪ I ) hereditary 𝒫 𝐴
21.36.6.3  _Begriffsschrift_ Chapter II Implication
Axiom	ax-frege1 43779	The case in which 𝜑 is denied, 𝜓 is affirmed, and 𝜑 is affirmed is excluded. This is evident since 𝜑 cannot at the same time be denied and affirmed. Axiom 1 of [Frege1879] p. 26. Identical to ax-1 6. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Axiom	ax-frege2 43780	If a proposition 𝜒 is a necessary consequence of two propositions 𝜓 and 𝜑 and one of those, 𝜓, is in turn a necessary consequence of the other, 𝜑, then the proposition 𝜒 is a necessary consequence of the latter one, 𝜑, alone. Axiom 2 of [Frege1879] p. 26. Identical to ax-2 7. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	rp-simp2-frege 43781	Simplification of triple conjunction. Compare with simp2 1136. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓)))
Theorem	rp-simp2 43782	Simplification of triple conjunction. Identical to simp2 1136. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
Theorem	rp-frege3g 43783	Add antecedent to ax-frege2 43780. More general statement than frege3 43784. Like ax-frege2 43780, it is essentially a closed form of mpd 15, however it has an extra antecedent. It would be more natural to prove from a1i 11 and ax-frege2 43780 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃))))
Theorem	frege3 43784	Add antecedent to ax-frege2 43780. Special case of rp-frege3g 43783. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜑 → 𝜓)) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))))
Theorem	rp-misc1-frege 43785	Double-use of ax-frege2 43780. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜓)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
Theorem	rp-frege24 43786	Introducing an embedded antecedent. Alternate proof for frege24 43804. Closed form for a1d 25. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓)))
Theorem	rp-frege4g 43787	Deduction related to distribution. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))))
Theorem	frege4 43788	Special case of closed form of a2d 29. Special case of rp-frege4g 43787. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))))
Theorem	frege5 43789	A closed form of syl 17. Identical to imim2 58. Theorem *2.05 of [WhiteheadRussell] p. 100. Proposition 5 of [Frege1879] p. 32. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	rp-7frege 43790	Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜃 → ((𝜑 → 𝜓) → (𝜑 → 𝜒))))
Theorem	rp-4frege 43791	Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → ((𝜓 → 𝜑) → 𝜒)) → (𝜑 → 𝜒))
Theorem	rp-6frege 43792	Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ((𝜓 → ((𝜒 → 𝜓) → 𝜃)) → (𝜓 → 𝜃)))
Theorem	rp-8frege 43793	Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → (𝜓 → ((𝜒 → 𝜓) → 𝜃))) → (𝜑 → (𝜓 → 𝜃)))
Theorem	rp-frege25 43794	Closed form for a1dd 50. Alternate route to Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒))))
Theorem	frege6 43795	A closed form of imim2d 57 which is a deduction adding nested antecedents. Proposition 6 of [Frege1879] p. 33. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒))))
Theorem	axfrege8 43796	Swap antecedents. Identical to pm2.04 90. This demonstrates that Axiom 8 of [Frege1879] p. 35 is redundant. Proof follows closely proof of pm2.04 90 in https://us.metamath.org/mmsolitaire/pmproofs.txt 90, but in the style of Frege's 1879 work. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	frege7 43797	A closed form of syl6 35. The first antecedent is used to replace the consequent of the second antecedent. Proposition 7 of [Frege1879] p. 34. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜃 → 𝜑)) → (𝜒 → (𝜃 → 𝜓))))
Axiom	ax-frege8 43798	Swap antecedents. If two conditions have a proposition as a consequence, their order is immaterial. Third axiom of Frege's 1879 work but identical to pm2.04 90 which can be proved from only ax-mp 5, ax-frege1 43779, and ax-frege2 43780. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	frege26 43799	Identical to idd 24. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜓))
Theorem	frege27 43800	We cannot (at the same time) affirm 𝜑 and deny 𝜑. Identical to id 22. Proposition 27 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝜑)