P. 440 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

frege65c 43901

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

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

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

Theorem

frege67c 43903

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

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

Theorem

frege68c 43904

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 43933 and frege109 43945.

dffrege69 43905 through frege75 43911 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 43905*

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

Lemma for frege72 43908. 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 43907*

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

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 43909

Lemma for frege87 43923. 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 43910

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

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 43912 through frege98 43934 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 43912*

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

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

Commuted form of frege77 43913. 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 43915*

Distributed form of frege78 43914. 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 43916*

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

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 43918

Closed-form deduction based on frege81 43917. 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 43919

Apply commuted form of frege81 43917 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 43920

Commuted form of frege81 43917. 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 43921*

Commuted form of frege77 43913. 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 43922*

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

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

Commuted form of frege87 43923. 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 43925*

One direction of dffrege76 43912. 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 43926*

Add antecedent to frege89 43925. 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 43927

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 43928

Inference from frege91 43927. 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 43929*

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

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 43931

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 43932

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 43933

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 43934

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 43935 through frege114 43950 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 43935

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 43936

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

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

Theorem

frege101 43937

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

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

Theorem

frege102 43938

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 43939

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

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

Theorem

frege104 43940

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 43941

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

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

Theorem

frege106 43942

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 43943

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 43944

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 43945

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

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

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

Theorem

frege111 43947

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 43948

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 43949

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 43950

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

Theorem

dffrege115 43951*

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

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

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

Theorem

frege117 43953*

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

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

Theorem

frege118 43954*

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

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

Theorem

frege119 43955*

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

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

Theorem

frege120 43956

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

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

Theorem

frege121 43957

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

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

Theorem

frege122 43958

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

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

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 43961

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

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 43963

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

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

Theorem

frege128 43964

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

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

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

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 43968

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

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 43970

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

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

Theorem

enrelmapr 43971

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 43972

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 43973

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 43990. 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 44030, ntrneiel 44054, neicvgel1 44092
	¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)	↔	¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆))	↔	𝑋 ∈ (𝐾‘𝑆)	↔	𝑆 ∈ (𝑀‘𝑋)
Neighborhoods	(𝑁‘𝑋)	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)}	ntrneifv3 44055, clsneifv3 44083, neicvgfv 44094
Interior	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)}	=	(𝐼‘𝑆)	=	(𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆)))	=	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑥)}	ntrneifv4 44058, ntrclsfv 44032, clsneifv4 44084
Closure	{𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)}	=	(𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑆)))	=	(𝐾‘𝑆)	=	{𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑀‘𝑥)}	clsneifv4 44084, ntrclsfv 44032, ntrneifv4 44058
Convergents	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑁‘𝑋)}	=	{𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑠))}	=	{𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐾‘𝑠)}	=	(𝑀‘𝑋)	neicvgfv 44094, clsneifv3 44083, ntrneifv3 44055

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 44038, ntrneineine0 44060, ntrneineine1 44061
KA' No neighborhood is equal to the full powerset.	(𝑁‘𝑥) ≠ 𝒫 𝐵	∃𝑢 ∈ 𝒫 𝐵¬ 𝑥 ∈ (𝐼‘𝑢)	∃𝑢 ∈ 𝒫 𝐵𝑥 ∈ (𝐾‘𝑢)	(𝑀‘𝑥) ≠ ∅	ntrclsneine0 44038, ntrneineine0 44060, ntrneineine1 44061
K0 Preservation of the Nullary Union of Closures	𝐵 ∈ (𝑁‘𝑥)	(𝐼‘𝐵) = 𝐵	(𝐾‘∅) = ∅	¬ ∅ ∈ (𝑀‘𝑥)	ntrclscls00 44039, ntrneicls00 44062, ntrneicls11 44063
KA Preservation of the Nullary Union of Interiors	¬ ∅ ∈ (𝑁‘𝑥)	(𝐼‘∅) = ∅	(𝐾‘𝐵) = 𝐵	𝐵 ∈ (𝑀‘𝑥)	ntrclscls00 44039, ntrneicls00 44062, ntrneicls11 44063
K1 Isotonic Montonic	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))	(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) — or — ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∪ 𝑡)) — or — (𝐼‘(𝑠 ∩ 𝑡)) ⊆ ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) — or — ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) ⊆ (𝐾‘(𝑠 ∪ 𝑡)) — or — (𝐾‘(𝑠 ∩ 𝑡)) ⊆ ((𝐾‘𝑠) ∩ (𝐾‘𝑡))	((𝑠 ∈ (𝑀‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑀‘𝑥))	isotone1 44021, isotone2 44022, ntrclsiso 44040, ntrneiiso 44064
K2 Closure is Expansive	(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)	(𝐼‘𝑠) ⊆ 𝑠	𝑠 ⊆ (𝐾‘𝑠)	(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑀‘𝑥))	ntrclsk2 44041, ntrneik2 44065, ntrneix2 44066
KB Non-disjoint Neighborhoods	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)	((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)	((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)	((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclskb 44042, ntrneikb 44067, ntrneixb 44068
K3 Closure is Sub-linear	((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))	((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) → (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk3 44043, ntrneik3 44069, ntrneix3 44070
K13 Closure is finitely linear	((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))	(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡))	(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))	((𝑠 ∪ 𝑡) ∈ (𝑀‘𝑥) ↔ (𝑠 ∈ (𝑀‘𝑥) ∨ 𝑡 ∈ (𝑀‘𝑥)))	ntrclsk13 44044, ntrneik13 44071, ntrneix13 44072
K4 Closure is idempotent	(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))	(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠)	(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)	(𝑠 ∈ (𝑀‘𝑥) ↔ ∃𝑢 ∈ (𝑀‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑀‘𝑦)))	ntrclsk4 44045, ntrneik4 44074

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 44010, ntrkbimka 44011, neik0imk0p 44009
Min Strong Generalized Neighborhood Space	K2, K3	KA', KA, KB	ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009
Gniłka Extended Topology	K0', K1	K0	neik0pk1imk0 44020
Brissaud Space	K0, K2	K0', KA', KA, KB	neik0imk0p 44009, ntrk2imkb 44010, ntrkbimka 44011
Neighborhood Space	K0', K1, K2	K0, KA', KA, KB	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009
Davey and Priestley Intersection Structure	K1, K4
Moore Closure Space	K1, K2, K4	KA', KA, KB	ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009
Convex Closure Space	K0', K1, K2, K4	K0, KA', KA, KB	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009
Smyth Neighborhood Space	K0', K13	K0, K1, K3	neik0pk1imk0 44020, ntrk1k3eqk13 44023
Čech Closure Space Pretopological Space	K0', K2, K13	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009, ntrk1k3eqk13 44023
Topological Space	K0', K2, K13, K4	K0, K1, KA', KA, KB, K3	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009, ntrk1k3eqk13 44023
Alexandroff Space	K0', K2, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009, ntrk1k3eqk13 44023, TBD
Alexandroff Topological Space	K0', K2, K4, K5	K0, K1, KA', KA, KB, K3, K13	neik0pk1imk0 44020, ntrk2imkb 44010, ntrkbimka 44011, neik0imk0p 44009, ntrk1k3eqk13 44023, TBD

Theorem

or3or 43996

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

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

Theorem

andi3or 43997

Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒 ∨ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)))

Theorem

uneqsn 43998

If a union of classes is equal to a singleton then at least one class is equal to the singleton while the other may be equal to the empty set. (Contributed by RP, 5-Jul-2021.)

⊢ ((𝐴 ∪ 𝐵) = {𝐶} ↔ ((𝐴 = {𝐶} ∧ 𝐵 = {𝐶}) ∨ (𝐴 = {𝐶} ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ 𝐵 = {𝐶})))

Theorem

brfvimex 43999

If a binary relation holds and the relation is the value of a function, then the argument to that function is a set. (Contributed by RP, 22-May-2021.)

⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐹‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)

Theorem

brovmptimex 44000*

If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021.)

⊢ 𝐹 = (𝑥 ∈ 𝐸, 𝑦 ∈ 𝐺 ↦ 𝐻)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝑅 = (𝐶𝐹𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∈ V ∧ 𝐷 ∈ V))