Home | Metamath
Proof Explorer Theorem List (p. 383 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | frege62b 38201 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2563 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege63b 38202 | Lemma for frege91 38248. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege64b 38203 | Lemma for frege65b 38204. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege65b 38204 |
A kind of Aristotelian inference. This judgement replaces the mode of
inference barbara 2563 when the minor premise has a general context.
Proposition 65 of [Frege1879] p. 53.
In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : . But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege66b 38205 | Swap antecedents of frege65b 38204. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege67b 38206 | Lemma for frege68b 38207. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege68b 38207 | 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.) |
Theorem | frege53c 38208 | Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege54cor1c 38209* | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.) |
Theorem | frege55lem1c 38210* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
Theorem | frege55lem2c 38211* | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege55c 38212 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege56c 38213* | Lemma for frege57c 38214. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege57c 38214* | Swap order of implication in ax-frege52c 38182. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege58c 38215 | Principle related to sp 2053. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege59c 38216 |
A kind of Aristotelian inference. Proposition 59 of [Frege1879] p. 51.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 38107 incorrectly referenced where frege30 38126 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege60c 38217 | Swap antecedents of frege58c 38215. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege61c 38218 | Lemma for frege65c 38222. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege62c 38219 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2563 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege63c 38220 | Analogue of frege63b 38202. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege64c 38221 | Lemma for frege65c 38222. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege65c 38222 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2563 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 38223 | Swap antecedents of frege65c 38222. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege67c 38224 | Lemma for frege68c 38225. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege68c 38225 | 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.) |
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 38254 and frege109 38266. dffrege69 38226 through frege75 38232 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 38226* | 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 38227* | Lemma for frege72 38229. 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 38228* | Lemma for frege72 38229. 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 38229 | 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 38230 | Lemma for frege87 38244. 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 38231 | 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 38232* | 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 | ||
means follows in the -sequence. dffrege76 38233 through frege98 38255 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 38233* |
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 | ||
Theorem | frege77 38234* | 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.) |
hereditary | ||
Theorem | frege78 38235* | Commuted form of of frege77 38234. Proposition 78 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege79 38236* | Distributed form of frege78 38235. Proposition 79 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.) |
hereditary hereditary | ||
Theorem | frege80 38237* | Add additional condition to both clauses of frege79 38236. Proposition 80 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
hereditary hereditary | ||
Theorem | frege81 38238 | 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 | ||
Theorem | frege82 38239 | Closed-form deduction based on frege81 38238. Proposition 82 of [Frege1879] p. 64. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege83 38240 | Apply commuted form of frege81 38238 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 | ||
Theorem | frege84 38241 | Commuted form of frege81 38238. Proposition 84 of [Frege1879] p. 65. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege85 38242* | Commuted form of frege77 38234. Proposition 85 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege86 38243* | 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 hereditary | ||
Theorem | frege87 38244* | 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.) |
hereditary | ||
Theorem | frege88 38245* | Commuted form of frege87 38244. Proposition 88 of [Frege1879] p. 67. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege89 38246* | One direction of dffrege76 38233. Proposition 89 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege90 38247* | Add antecedent to frege89 38246. Proposition 90 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege91 38248 | 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.) |
Theorem | frege92 38249 | Inference from frege91 38248. Proposition 92 of [Frege1879] p. 69. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege93 38250* | 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 | ||
Theorem | frege94 38251* | 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.) |
hereditary | ||
Theorem | frege95 38252 | 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.) |
Theorem | frege96 38253 | 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.) |
Theorem | frege97 38254 |
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 | ||
Theorem | frege98 38255 | 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.) |
means is a member of the -sequence begining with and is a member of the -sequence ending with . dffrege99 38256 through frege114 38271 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 38256 | 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.) |
Theorem | frege100 38257 | One direction of dffrege99 38256. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege101 38258 | Lemma for frege102 38259. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege102 38259 | 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.) |
Theorem | frege103 38260 | Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege104 38261 |
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.) |
Theorem | frege105 38262 | Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege106 38263 | 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.) |
Theorem | frege107 38264 | Proposition 107 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege108 38265 | 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.) |
Theorem | frege109 38266 | 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 | ||
Theorem | frege110 38267* | Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege111 38268 | 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.) |
Theorem | frege112 38269 | 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.) |
Theorem | frege113 38270 | Proposition 113 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege114 38271 | 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.) |
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 statments which vary on two variables to relations. dffrege115 38272 through frege133 38290 develop this and how functions relate to transitive and transitive-reflexive closures. | ||
Theorem | dffrege115 38272* | If from the 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.) |
Theorem | frege116 38273* | One direction of dffrege115 38272. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege117 38274* | Lemma for frege118 38275. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege118 38275* | Simplified application of one direction of dffrege115 38272. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege119 38276* | Lemma for frege120 38277. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege120 38277 | Simplified application of one direction of dffrege115 38272. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege121 38278 | Lemma for frege122 38279. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege122 38279 | 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.) |
Theorem | frege123 38280* | Lemma for frege124 38281. Proposition 123 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege124 38281 | 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.) |
Theorem | frege125 38282 | Lemma for frege126 38283. Proposition 125 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege126 38283 | 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.) |
Theorem | frege127 38284 | Communte antecedents of frege126 38283. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege128 38285 | Lemma for frege129 38286. Proposition 128 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
Theorem | frege129 38286 | 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.) |
Theorem | frege130 38287* | Lemma for frege131 38288. Proposition 130 of [Frege1879] p. 84. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
hereditary hereditary | ||
Theorem | frege131 38288 | 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.) |
hereditary | ||
Theorem | frege132 38289 | Lemma for frege133 38290. Proposition 132 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | frege133 38290 | 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.) |
See Seifert And Threlfall: A Textbook Of Topology (1980) which is an English translation of Lehrbuch der Topologie (1934). | ||
Because is an instance of the law of exponents: we are led to see that 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 38291 | 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 38300 for a demonstration of an natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021.) |
Theorem | enrelmapr 38292 | 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.) |
Theorem | enmappw 38293 | 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.) |
Theorem | enmappwid 38294 | 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.) |
Theorem | rfovd 38295* | Value of the operator, , which maps between relations and functions for relations between base sets, and . (Contributed by RP, 25-Apr-2021.) |
Theorem | rfovfvd 38296* | Value of the operator, , which maps between relations and functions for relations between base sets, and , and relation . (Contributed by RP, 25-Apr-2021.) |
Theorem | rfovfvfvd 38297* | 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.) |
Theorem | rfovcnvf1od 38298* | Properties of the operator, , which maps between relations and functions for relations between base sets, and . (Contributed by RP, 27-Apr-2021.) |
Theorem | rfovcnvd 38299* | 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.) |
Theorem | rfovf1od 38300* | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |