Home | Metamath
Proof Explorer Theorem List (p. 404 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege86 40301* | 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 40302* | 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 40303* | Commuted form of frege87 40302. 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 40304* | One direction of dffrege76 40291. 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 40305* | Add antecedent to frege89 40304. 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 40306 | 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 40307 | Inference from frege91 40306. 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 40308* | 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 40309* | 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 40310 | 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 40311 | 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 40312 |
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 40313 | 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+‘𝑅)𝑍)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
𝑝((t+‘𝑅) ∪ I )𝑐 means 𝑐 is a member of the 𝑅 -sequence begining with 𝑝 and 𝑝 is a member of the 𝑅 -sequence ending with 𝑐. dffrege99 40314 through frege114 40329 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 40314 | 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 40315 | One direction of dffrege99 40314. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege101 40316 | Lemma for frege102 40317. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑍 ∈ 𝑈 ⇒ ⊢ ((𝑍 = 𝑋 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → ((𝑋(t+‘𝑅)𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (𝑍𝑅𝑉 → 𝑋(t+‘𝑅)𝑉)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege102 40317 | 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 40318 | Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((𝑍 = 𝑋 → 𝑋 = 𝑍) → (𝑋((t+‘𝑅) ∪ I )𝑍 → (¬ 𝑋(t+‘𝑅)𝑍 → 𝑋 = 𝑍))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege104 40319 |
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 40320 | Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑍 ∈ 𝑉 ⇒ ⊢ ((¬ 𝑋(t+‘𝑅)𝑍 → 𝑍 = 𝑋) → 𝑋((t+‘𝑅) ∪ I )𝑍) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege106 40321 | 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 40322 | 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 40323 | 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 40324 | 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 40325* | Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝐴 & ⊢ 𝑌 ∈ 𝐵 & ⊢ 𝑀 ∈ 𝐶 & ⊢ 𝑅 ∈ 𝐷 ⇒ ⊢ (∀𝑎(𝑌𝑅𝑎 → 𝑋((t+‘𝑅) ∪ I )𝑎) → (𝑌(t+‘𝑅)𝑀 → 𝑋((t+‘𝑅) ∪ I )𝑀)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege111 40326 | 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 40327 | 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 40328 | 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 40329 | 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 )𝑍)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Fun ◡◡𝑅 means the relationship content of procedure 𝑅 is single-valued. The double converse allows us 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 40330 through frege133 40348 develop this and how functions relate to transitive and transitive-reflexive closures. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dffrege115 40330* | 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 40331* | One direction of dffrege115 40330. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 ⇒ ⊢ (Fun ◡◡𝑅 → ∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege117 40332* | Lemma for frege118 40333. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 ⇒ ⊢ ((∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege118 40333* | Simplified application of one direction of dffrege115 40330. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege119 40334* | Lemma for frege120 40335. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ ((∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋) → (𝑌𝑅𝐴 → 𝐴 = 𝑋)) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege120 40335 | Simplified application of one direction of dffrege115 40330. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝐴 ∈ 𝑊 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝐴 = 𝑋))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege121 40336 | Lemma for frege122 40337. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝐴 ∈ 𝑊 ⇒ ⊢ ((𝐴 = 𝑋 → 𝑋((t+‘𝑅) ∪ I )𝐴) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → (𝑌𝑅𝐴 → 𝑋((t+‘𝑅) ∪ I )𝐴)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege122 40337 | 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 40338* | Lemma for frege124 40339. 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 40339 | 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 40340 | Lemma for frege126 40341. 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 40341 | 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 40342 | Communte antecedents of frege126 40341. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 ∈ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑀 ∈ 𝑊 & ⊢ 𝑅 ∈ 𝑆 ⇒ ⊢ (Fun ◡◡𝑅 → (𝑌(t+‘𝑅)𝑀 → (𝑌𝑅𝑋 → (¬ 𝑋(t+‘𝑅)𝑀 → 𝑀((t+‘𝑅) ∪ I )𝑋)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | frege128 40343 | Lemma for frege129 40344. 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 40344 | If the procedure 𝑅 is single-valued and 𝑌 belongs to the 𝑅 -sequence begining with 𝑀 or precedes 𝑀 in the 𝑅-sequence, then every result of an application of the procedure 𝑅 to 𝑌 belongs to the 𝑅-sequence begining 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 40345* | Lemma for frege131 40346. 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 40346 | If the procedure 𝑅 is single-valued, then the property of belonging to the 𝑅-sequence begining 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 40347 | Lemma for frege133 40348. 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 40348 | 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 )𝑌)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
See Seifert and Threlfall: A Textbook Of Topology (1980) which is an English translation of Lehrbuch der Topologie (1934). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Because ((2o ↑m 𝐵) ↑m 𝐴) ≈ (2o ↑m (𝐴 × 𝐵)) ≈ ((2o ↑m 𝐴) ↑m 𝐵) is an instance of the law of exponents: ((𝐶 ↑m 𝐵) ↑m 𝐴) ≈ (𝐶 ↑m (𝐴 × 𝐵)) ≈ ((𝐶 ↑m 𝐴) ↑m 𝐵) we are led to see that (𝒫 𝐵 ↑m 𝐴) ≈ 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐴 ↑m 𝐵) is true for any two sets, 𝐴 and 𝐵, and thus there exist one-to-one onto relations between each of these three sets of relations. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | enrelmap 40349 | 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 40358 for a demonstration of a natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 × 𝐵) ≈ (𝒫 𝐵 ↑m 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | enrelmapr 40350 | 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 40351 | 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 40352 | 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 40353* | 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 40354* | 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 40355* | 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 40356* | 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 40357* | 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 40358* | 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 40359* | 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 40360* | 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 40361* | 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 40362* | 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 40363* | 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 40364* | 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 40365* | 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 40366* | 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 40367* | 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 40368* | 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 40369* | 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 40370* | 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 40371* | 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 40372* | 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 40373* | 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 40374* | 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 𝒫 𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
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 40369. 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.
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 𝒫 𝐵).
Using these properties as axiomic constraints on the functions, certain collections of them give rise to named spaces.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sscon34b 40375 | Relative complementation reverses inclusion of subclasses. Relativized version of complss 4126. (Contributed by RP, 3-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | rcompleq 40376 | Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4127. (Contributed by RP, 10-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | or3or 40377 | Decompose disjunction into three cases. (Contributed by RP, 5-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | andi3or 40378 | Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒 ∨ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uneqsn 40379 | 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 | df3o2 40380 | Ordinal 3 is the triplet containing ordinals 0, 1 and 2. (Contributed by RP, 8-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 3o = {∅, 1o, 2o} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | df3o3 40381 | Ordinal 3 , fully expanded. (Contributed by RP, 8-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 3o = {∅, {∅}, {∅, {∅}}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfvimex 40382 | 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 40383* | 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)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brovmptimex1 40384* | 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) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brovmptimex2 40385* | 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) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brcoffn 40386 | Conditions allowing the decomposition of a binary relation. (Contributed by RP, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐶 Fn 𝑌) & ⊢ (𝜑 → 𝐷:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴(𝐶 ∘ 𝐷)𝐵) ⇒ ⊢ (𝜑 → (𝐴𝐷(𝐷‘𝐴) ∧ (𝐷‘𝐴)𝐶𝐵)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brcofffn 40387 | Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐶 Fn 𝑍) & ⊢ (𝜑 → 𝐷:𝑌⟶𝑍) & ⊢ (𝜑 → 𝐸:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵) ⇒ ⊢ (𝜑 → (𝐴𝐸(𝐸‘𝐴) ∧ (𝐸‘𝐴)𝐷(𝐷‘(𝐸‘𝐴)) ∧ (𝐷‘(𝐸‘𝐴))𝐶𝐵)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brco2f1o 40388 | Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐶:𝑌–1-1-onto→𝑍) & ⊢ (𝜑 → 𝐷:𝑋–1-1-onto→𝑌) & ⊢ (𝜑 → 𝐴(𝐶 ∘ 𝐷)𝐵) ⇒ ⊢ (𝜑 → ((◡𝐶‘𝐵)𝐶𝐵 ∧ 𝐴𝐷(◡𝐶‘𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brco3f1o 40389 | Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐶:𝑌–1-1-onto→𝑍) & ⊢ (𝜑 → 𝐷:𝑋–1-1-onto→𝑌) & ⊢ (𝜑 → 𝐸:𝑊–1-1-onto→𝑋) & ⊢ (𝜑 → 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵) ⇒ ⊢ (𝜑 → ((◡𝐶‘𝐵)𝐶𝐵 ∧ (◡𝐷‘(◡𝐶‘𝐵))𝐷(◡𝐶‘𝐵) ∧ 𝐴𝐸(◡𝐷‘(◡𝐶‘𝐵)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ntrclsbex 40390 | If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then the base set exists. (Contributed by RP, 21-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) ⇒ ⊢ (𝜑 → 𝐵 ∈ V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ntrclsrcomplex 40391 | The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 25-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐷 = (𝑂‘𝐵) & ⊢ (𝜑 → 𝐼𝐷𝐾) ⇒ ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | neik0imk0p 40392 | Kuratowski's K0 axiom implies K0'. Neighborhood version. Also a proof the dual KA axiom implies KA' when considering the convergents. (Contributed by RP, 28-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥) → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ntrk2imkb 40393* | If an interior function is contracting, the interiors of disjoint sets are disjoint. Kuratowski's K2 axiom implies KB. Interior version. (Contributed by RP, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ntrkbimka 40394* | If the interiors of disjoint sets are disjoint, then the interior of the empty set is the empty set. (Contributed by RP, 14-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) → (𝐼‘∅) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ntrk0kbimka 40395* | If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka 40394. (Contributed by RP, 12-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → (𝐼‘∅) = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | clsk3nimkb 40396* | If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) is given. (Contributed by RP, 16-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | clsk1indlem0 40397 | The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) has the K0 property of preserving the nullary union. (Contributed by RP, 6-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ⇒ ⊢ (𝐾‘∅) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | clsk1indlem2 40398* | The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) has the K2 property of expanding. (Contributed by RP, 6-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ⇒ ⊢ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝐾‘𝑠) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | clsk1indlem3 40399* | The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) has the K3 property of being sub-linear. (Contributed by RP, 6-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ⇒ ⊢ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫 3o(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | clsk1indlem4 40400* | The ansatz closure function (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) has the K4 property of idempotence. (Contributed by RP, 6-Jul-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟)) ⇒ ⊢ ∀𝑠 ∈ 𝒫 3o(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |