P. 443 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

frege61c 44201

Lemma for frege65c 44205. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐴 / 𝑥]𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))

Theorem

frege62c 44202

A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2664 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 44203

Analogue of frege63b 44185. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → (𝜓 → (∀𝑥(𝜑 → 𝜒) → [𝐴 / 𝑥]𝜒)))

Theorem

frege64c 44204

Lemma for frege65c 44205. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) → (∀𝑥(𝜓 → 𝜒) → ([𝐶 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜒)))

Theorem

frege65c 44205

A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2664 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 44206

Swap antecedents of frege65c 44205. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → ([𝐴 / 𝑥]𝜒 → [𝐴 / 𝑥]𝜓)))

Theorem

frege67c 44207

Lemma for frege68c 44208. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ (((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → ∀𝑥𝜑)) → ((∀𝑥𝜑 ↔ 𝜓) → (𝜓 → [𝐴 / 𝑥]𝜑)))

Theorem

frege68c 44208

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 44237 and frege109 44249.

dffrege69 44209 through frege75 44215 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 44209*

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 44210*

Lemma for frege72 44212. 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 44211*

Lemma for frege72 44212. 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 44212

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 44213

Lemma for frege87 44227. 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 44214

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 44215*

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 44216 through frege98 44238 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 44216*

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 44217*

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 44218*

Commuted form of frege77 44217. 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 44219*

Distributed form of frege78 44218. 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 44220*

Add additional condition to both clauses of frege79 44219. 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 44221

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 44222

Closed-form deduction based on frege81 44221. 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 44223

Apply commuted form of frege81 44221 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 44224

Commuted form of frege81 44221. 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 44225*

Commuted form of frege77 44217. 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 44226*

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 44227*

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 44228*

Commuted form of frege87 44227. 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 44229*

One direction of dffrege76 44216. 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 44230*

Add antecedent to frege89 44229. 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 44231

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 44232

Inference from frege91 44231. 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 44233*

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 44234*

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 44235

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 44236

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 44237

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 44238

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 44239 through frege114 44254 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 44239

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 44240

One direction of dffrege99 44239. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑍 ∈ 𝑈    ⇒   ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋))

Theorem

frege101 44241

Lemma for frege102 44242. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑍 ∈ 𝑈    ⇒   ⊢ ((𝑍 = 𝑋 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → ((𝑋(t+‘𝑅)𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉))))

Theorem

frege102 44242

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 44243

Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑍 ∈ 𝑉    ⇒   ⊢ ((𝑍 = 𝑋 → 𝑋 = 𝑍) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍)))

Theorem

frege104 44244

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 44245

Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑍 ∈ 𝑉    ⇒   ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) → 𝑋((t+‘𝑅) ∪ I )𝑍)

Theorem

frege106 44246

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 44247

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 44248

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 44249

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 44250*

Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝐴    &   ⊢ 𝑌 ∈ 𝐵    &   ⊢ 𝑀 ∈ 𝐶    &   ⊢ 𝑅 ∈ 𝐷    ⇒   ⊢ (∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀))

Theorem

frege111 44251

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 44252

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 44253

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 44254

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.36.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 44255 through frege133 44273 develop this and how functions relate to transitive and transitive-reflexive closures.

Theorem

dffrege115 44255*

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 44256*

One direction of dffrege115 44255. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    ⇒   ⊢ (Fun ^◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)))

Theorem

frege117 44257*

Lemma for frege118 44258. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    ⇒   ⊢ ((∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) → (Fun ^◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))))

Theorem

frege118 44258*

Simplified application of one direction of dffrege115 44255. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ (Fun ^◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)))

Theorem

frege119 44259*

Lemma for frege120 44260. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    ⇒   ⊢ ((∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋) → (𝑌𝑅𝐴 → 𝐴 = 𝑋)) → (Fun ^◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋))))

Theorem

frege120 44260

Simplified application of one direction of dffrege115 44255. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝐴 ∈ 𝑊    ⇒   ⊢ (Fun ^◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋)))

Theorem

frege121 44261

Lemma for frege122 44262. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝐴 ∈ 𝑊    ⇒   ⊢ ((𝐴 = 𝑋 → 𝑋((t+‘𝑅) ∪ I )𝐴) → (Fun ^◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝑋((t+‘𝑅) ∪ I )𝐴))))

Theorem

frege122 44262

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 44263*

Lemma for frege124 44264. 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 44264

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 44265

Lemma for frege126 44266. 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 44266

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 44267

Communte antecedents of frege126 44266. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)

⊢ 𝑋 ∈ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑀 ∈ 𝑊    &   ⊢ 𝑅 ∈ 𝑆    ⇒   ⊢ (Fun ^◡◡𝑅 → (𝑌(t+‘𝑅)𝑀 → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋))))

Theorem

frege128 44268

Lemma for frege129 44269. 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 44269

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 44270*

Lemma for frege131 44271. 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 44271

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 44272

Lemma for frege133 44273. 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 44273

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.36.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.36.7.1  Equinumerosity of sets of relations and maps

Because ((2_o ↑_m 𝐵) ↑_m 𝐴) ≈ (2_o ↑_m (𝐴 × 𝐵)) ≈ ((2_o ↑_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 44274

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 44283 for a demonstration of a natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐵 ↑_m 𝐴))

Theorem

enrelmapr 44275

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 44276

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 44277

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 44278*

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 44279*

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 44280*

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 44281*

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-1-onto→(𝒫 𝐵 ↑_m 𝐴) ∧ ^◡𝐹 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})))

Theorem

rfovcnvd 44282*

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 44283*

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-1-onto→(𝒫 𝐵 ↑_m 𝐴))

Theorem

rfovcnvfvd 44284*

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 44285*

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 𝐴) ↦ (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝑓‘𝑥)})))

Theorem

fsovrfovd 44286*

The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ (𝑢 ∈ 𝑎 ↦ {𝑣 ∈ 𝑏 ∣ 𝑢𝑟𝑣})))    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (𝑎 × 𝑏) ↦ ^◡𝑠))    ⇒   ⊢ (𝜑 → (𝐴𝑂𝐵) = ((𝐵𝑅𝐴) ∘ ((𝐴𝐶𝐵) ∘ ^◡(𝐴𝑅𝐵))))

Theorem

fsovfvd 44287*

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 𝐵, when applied to function 𝐹. (Contributed by RP, 25-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝐴))    ⇒   ⊢ (𝜑 → (𝐺‘𝐹) = (𝑦 ∈ 𝐵 ↦ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐹‘𝑥)}))

Theorem

fsovfvfvd 44288*

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 𝐵, when applied to function 𝐹 and element 𝑌. (Contributed by RP, 25-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝐴))    &   ⊢ 𝐻 = (𝐺‘𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻‘𝑌) = {𝑥 ∈ 𝐴 ∣ 𝑌 ∈ (𝐹‘𝑥)})

Theorem

fsovfd 44289*

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 𝐵, gives a function between two sets of functions. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → 𝐺:(𝒫 𝐵 ↑_m 𝐴)⟶(𝒫 𝐴 ↑_m 𝐵))

Theorem

fsovcnvlem 44290*

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, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ 𝐻 = (𝐵𝑂𝐴)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐺) = ( I ↾ (𝒫 𝐵 ↑_m 𝐴)))

Theorem

fsovcnvd 44291*

The value of the converse (𝐴𝑂𝐵) is (𝐵𝑂𝐴), where 𝑂 is 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, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ 𝐻 = (𝐵𝑂𝐴)    ⇒   ⊢ (𝜑 → ^◡𝐺 = 𝐻)

Theorem

fsovcnvfvd 44292*

The value of the converse of (𝐴𝑂𝐵), where 𝑂 is 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, evaluated at function 𝐹. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐴 ↑_m 𝐵))    ⇒   ⊢ (𝜑 → (^◡𝐺‘𝐹) = (𝑦 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ 𝑦 ∈ (𝐹‘𝑥)}))

Theorem

fsovf1od 44293*

The value of (𝐴𝑂𝐵) is a bijection, where 𝑂 is 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. (Contributed by RP, 27-Apr-2021.)

⊢ 𝑂 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝑎) ↦ (𝑦 ∈ 𝑏 ↦ {𝑥 ∈ 𝑎 ∣ 𝑦 ∈ (𝑓‘𝑥)})))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = (𝐴𝑂𝐵)    ⇒   ⊢ (𝜑 → 𝐺:(𝒫 𝐵 ↑_m 𝐴)–1-1-onto→(𝒫 𝐴 ↑_m 𝐵))

Theorem

dssmapfvd 44294*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))

Theorem

dssmapfv2d 44295*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵 when applied to function 𝐹. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))    &   ⊢ 𝐺 = (𝐷‘𝐹)    ⇒   ⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝐹‘(𝐵 ∖ 𝑠)))))

Theorem

dssmapfv3d 44296*

Value of the duality operator for self-mappings of subsets of a base set, 𝐵 when applied to function 𝐹 and subset 𝑆. (Contributed by RP, 19-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))    &   ⊢ 𝐺 = (𝐷‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ 𝑇 = (𝐺‘𝑆)    ⇒   ⊢ (𝜑 → 𝑇 = (𝐵 ∖ (𝐹‘(𝐵 ∖ 𝑆))))

Theorem

dssmapnvod 44297*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set is its own inverse, an involution. (Contributed by RP, 20-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ^◡𝐷 = 𝐷)

Theorem

dssmapf1od 44298*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set is one-to-one and onto. (Contributed by RP, 21-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐷:(𝒫 𝐵 ↑_m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑_m 𝒫 𝐵))

Theorem

dssmap2d 44299*

For any base set 𝐵 the duality operator for self-mappings of subsets of that base set when composed with itself is the restricted identity operator. (Contributed by RP, 21-Apr-2021.)

⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐷 ∘ 𝐷) = ( I ↾ (𝒫 𝐵 ↑_m 𝒫 𝐵)))

21.36.7.2  Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods

For any base set, 𝐵, an arbitrary mapping of subsets to subsets can be called a pseudoclosure (pseudointerior) function, 𝐾, with its dual of a pseudointerior (pseudoclosure), 𝐼, related by the involution in dssmapfvd 44294. As 𝐾 gains properties of the closure (interior) function of a topology on 𝐵, so does its dual gain corresponding properties of the interior (closure) function of that topology.

As (𝒫 𝐵 ↑_m 𝒫 𝐵) ≈ (𝒫 𝒫 𝐵 ↑_m 𝐵) there is also a natural isomorphism which maps from 𝐼 to 𝑁 (and likewise for 𝐾 and 𝑀, introduced below) which identically gains the properties of the neighborhood function of a topology (modified and restricted to operate on single points). A function dual to 𝑁, which Stadler and Stadler refer to as a convergent function, is represented by 𝑀 in this section.

Based on this and the early treatment of topology in Seifert and Threlfall, it seems reasonable to define a pseudotopology as defined in terms of its base set and one of these functions with theorems treating the equivalence of the other definitions and adding topological structure if enough properties hold true.

	Neighborhoods		Interior		Closure		Convergents	Theorems
Functions	𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)		𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)		𝐾 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)		𝑀 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵)
Correspondences (assuming (𝑋 ∈ 𝐵 ∧ 𝑆 ∈ 𝒫 𝐵))	𝑆 ∈ (𝑁‘𝑋)	↔	𝑋 ∈ (𝐼‘𝑆)	↔	¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆))	↔	¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋)	ntrclselnel1 44334, ntrneiel 44358, neicvgel1 44396
	¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)	↔	¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆))	↔	𝑋 ∈ (𝐾‘𝑆)	↔	𝑆 ∈ (𝑀‘𝑋)
Neighborhoods	(𝑁‘𝑋)	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)}	ntrneifv3 44359, clsneifv3 44387, neicvgfv 44398
Interior	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)}	=	(𝐼‘𝑆)	=	(𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆)))	=	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑥)}	ntrneifv4 44362, ntrclsfv 44336, clsneifv4 44388
Closure	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)}	=	(𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑆)))	=	(𝐾‘𝑆)	=	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑀‘𝑥)}	clsneifv4 44388, ntrclsfv 44336, ntrneifv4 44362
Convergents	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑁‘𝑋)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐾‘𝑠)}	=	(𝑀‘𝑋)	neicvgfv 44398, clsneifv3 44387, ntrneifv3 44359

We have the following table of equivalences to axioms largely established by Kuratowski. In the formulas in this table, to reduce the width of the columns, if any of the variables 𝑥, 𝑠, or 𝑡 are used, then they are implicitly universally quantified and 𝑥 (respectively 𝑠 and 𝑡) ranges over 𝐵 (respectively 𝒫 𝐵 and 𝒫 𝐵).

Assuming a prefix of: ∀𝑥 ∈ 𝐵∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵	Neighborhoods	Interior	Closure	Convergents	Equivalence Theorems
K0' Neighborhoods are nonempty.	(𝑁‘𝑥) ≠ ∅	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ 𝒫 𝐵	ntrclsneine0 44342, ntrneineine0 44364, ntrneineine1 44365
KA' No neighborhood is equal to the full powerset.	(𝑁‘𝑥) ≠ 𝒫 𝐵	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ ∅	ntrclsneine0 44342, ntrneineine0 44364, ntrneineine1 44365
K0 Preservation of the Nullary Union of Closures	𝐵 ∈ (𝑁‘𝑥)	(𝐼‘𝐵) = 𝐵	(𝐾‘∅) = ∅	¬ ∅ ∈ (𝑀‘𝑥)	ntrclscls00 44343, ntrneicls00 44366, ntrneicls11 44367
KA Preservation of the Nullary Union of Interiors	¬ ∅ ∈ (𝑁‘𝑥)	(𝐼‘∅) = ∅	(𝐾‘𝐵) = 𝐵	𝐵 ∈ (𝑀‘𝑥)	ntrclscls00 44343, ntrneicls00 44366, ntrneicls11 44367
K1 Isotonic Montonic	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))	(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) — or — ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∪ 𝑡)) — or — (𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) — or — ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) ⊆ (𝐾‘(𝑠 ∪ 𝑡)) — or — (𝐾‘(𝑠 ∩ 𝑡)) ⊆ ((𝐾‘𝑠) ∩ (𝐾‘𝑡))	((𝑠 ∈ (𝑀‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑀‘𝑥))	isotone1 44325, isotone2 44326, ntrclsiso 44344, ntrneiiso 44368
K2 Closure is Expansive	(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)	(𝐼‘𝑠) ⊆ 𝑠	𝑠 ⊆ (𝐾‘𝑠)	(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑀‘𝑥))	ntrclsk2 44345, ntrneik2 44369, ntrneix2 44370
KB Non-disjoint Neighborhoods	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)	((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)	((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)	((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclskb 44346, ntrneikb 44371, ntrneixb 44372
K3 Closure is Sub-linear	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))	((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk3 44347, ntrneik3 44373, ntrneix3 44374
K13 Closure is finitely linear	((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))	(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) ↔ (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk13 44348, ntrneik13 44375, ntrneix13 44376
K4 Closure is idempotent	(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))	(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠)	(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)	(𝑠 ∈ (𝑀‘𝑥) ↔ ∃𝑢 ∈ (𝑀‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑀‘𝑦)))	ntrclsk4 44349, ntrneik4 44378

Using these properties as axiomic constraints on the functions, certain collections of them give rise to named spaces.

Space	Foundational Axioms	Derived Axioms	Theorems
Csázár Generalized Neighborhood Space	K2	KA', KA, KB	ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313
Min Strong Generalized Neighborhood Space	K2, K3	KA', KA, KB	ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313
Gniłka Extended Topology	K0', K1	K0	neik0pk1imk0 44324
Brissaud Space	K0, K2	K0', KA', KA, KB	neik0imk0p 44313, ntrk2imkb 44314, ntrkbimka 44315
Neighborhood Space	K0', K1, K2	K0, KA', KA, KB	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313
Davey and Priestley Intersection Structure	K1, K4
Moore Closure Space	K1, K2, K4	KA', KA, KB	ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313
Convex Closure Space	K0', K1, K2, K4	K0, KA', KA, KB	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313
Smyth Neighborhood Space	K0', K13	K0, K1, K3	neik0pk1imk0 44324, ntrk1k3eqk13 44327
Čech Closure Space Pretopological Space	K0', K2, K13	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313, ntrk1k3eqk13 44327
Topological Space	K0', K2, K13, K4	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313, ntrk1k3eqk13 44327
Alexandroff Space	K0', K2, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313, ntrk1k3eqk13 44327, TBD
Alexandroff Topological Space	K0', K2, K4, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44324, ntrk2imkb 44314, ntrkbimka 44315, neik0imk0p 44313, ntrk1k3eqk13 44327, TBD

Theorem

or3or 44300

Decompose disjunction into three cases. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓)))