Home | Metamath
Proof Explorer Theorem List (p. 381 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 | relexpmulnn 38001 | With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
Theorem | relexpmulg 38002 | With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
Theorem | trclrelexplem 38003* | The union of relational powers to positive multiples of is a subset to the transitive closure raised to the power of . (Contributed by RP, 15-Jun-2020.) |
Theorem | iunrelexpmin2 38004* | The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.) |
Theorem | relexp01min 38005 | With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.) |
Theorem | relexp1idm 38006 | Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.) |
Theorem | relexp0idm 38007 | Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.) |
Theorem | relexp0a 38008 | Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.) |
Theorem | relexpxpmin 38009 | The composition of powers of a cross-product of non-disjoint sets is the cross product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.) |
Theorem | relexpaddss 38010 | The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where is a relation as shown by relexpaddd 13794 or when the sum of the powers isn't 1 as shown by relexpaddg 13793. (Contributed by RP, 3-Jun-2020.) |
Theorem | iunrelexpuztr 38011* | The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 13800. (Contributed by RP, 4-Jun-2020.) |
Theorem | dftrcl3 38012* | Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.) |
Theorem | brfvtrcld 38013* | If two elements are connected by the transitive closure of a relation, then they are connected via instances the relation, for some counting number . (Contributed by RP, 22-Jul-2020.) |
Theorem | fvtrcllb1d 38014 | A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.) |
Theorem | trclfvcom 38015 | The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.) |
Theorem | cnvtrclfv 38016 | The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.) |
Theorem | cotrcltrcl 38017 | The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.) |
Theorem | trclimalb2 38018 | Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.) |
Theorem | brtrclfv2 38019* | Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.) |
Theorem | trclfvdecomr 38020 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
Theorem | trclfvdecoml 38021 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
Theorem | dmtrclfvRP 38022 | The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
Theorem | rntrclfvRP 38023 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.) |
Theorem | rntrclfv 38024 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
Theorem | dfrtrcl3 38025* | Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 13802. (Contributed by RP, 5-Jun-2020.) |
Theorem | brfvrtrcld 38026* | If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via instances the relation, for some natural number . Similar of dfrtrclrec2 13797. (Contributed by RP, 22-Jul-2020.) |
Theorem | fvrtrcllb0d 38027 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.) |
Theorem | fvrtrcllb0da 38028 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.) |
Theorem | fvrtrcllb1d 38029 | A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.) |
Theorem | dfrtrcl4 38030 | Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.) |
Theorem | corcltrcl 38031 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.) |
Theorem | cortrcltrcl 38032 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | corclrtrcl 38033 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cotrclrcl 38034 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.) |
Theorem | cortrclrcl 38035 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cotrclrtrcl 38036 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cortrclrtrcl 38037 | The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
Theorems inspired by Begriffsschrift without restricting form and content to closely parallel those in [Frege1879]. | ||
Theorem | frege77d 38038 | If the images of both and are subsets of and follows in the transitive closure of , then is an element of . Similar to Proposition 77 of [Frege1879] p. 62. Compare with frege77 38234. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege81d 38039 | If the image of is a subset , is an element of and follows in the transitive closure of , then is an element of . Similar to Proposition 81 of [Frege1879] p. 63. Compare with frege81 38238. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege83d 38040 | If the image of the union of and is a subset of the union of and , is an element of and follows in the transitive closure of , then is an element of the union of and . Similar to Proposition 83 of [Frege1879] p. 65. Compare with frege83 38240. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege96d 38041 | If follows in the transitive closure of and follows in , then follows in the transitive closure of . Similar to Proposition 96 of [Frege1879] p. 71. Compare with frege96 38253. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege87d 38042 | If the images of both and are subsets of and follows in the transitive closure of and follows in , then is an element of . Similar to Proposition 87 of [Frege1879] p. 66. Compare with frege87 38244. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege91d 38043 | If follows in then follows in the transitive closure of . Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 38248. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege97d 38044 | If contains all elements after those in in the transitive closure of , then the image under of is a subclass of . Similar to Proposition 97 of [Frege1879] p. 71. Compare with frege97 38254. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege98d 38045 | If follows and follows in the transitive closure of , then follows in the transitive closure of . Similar to Proposition 98 of [Frege1879] p. 71. Compare with frege98 38255. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege102d 38046 | If either and are the same or follows in the transitive closure of and is the successor to , then follows in the transitive closure of . Similar to Proposition 102 of [Frege1879] p. 72. Compare with frege102 38259. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege106d 38047 | If follows in , then either and are the same or follows in . Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 38263. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege108d 38048 | If either and are the same or follows in the transitive closure of and is the successor to , then either and are the same or follows in the transitive closure of . Similar to Proposition 108 of [Frege1879] p. 74. Compare with frege108 38265. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege109d 38049 | If contains all elements of and all elements after those in in the transitive closure of , then the image under of is a subclass of . Similar to Proposition 109 of [Frege1879] p. 74. Compare with frege109 38266. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege114d 38050 | If either relates and or and are the same, then either and are the same, relates and , relates and . Similar to Proposition 114 of [Frege1879] p. 76. Compare with frege114 38271. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege111d 38051 | If either and are the same or follows in the transitive closure of and is the successor to , then either and are the same or follows or and in the transitive closure of . Similar to Proposition 111 of [Frege1879] p. 75. Compare with frege111 38268. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege122d 38052 | If is a function, is the successor of , and is the successor of , then and are the same (or follows in the transitive closure of ). Similar to Proposition 122 of [Frege1879] p. 79. Compare with frege122 38279. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege124d 38053 | If is a function, is the successor of , and follows in the transitive closure of , then and are the same or follows in the transitive closure of . Similar to Proposition 124 of [Frege1879] p. 80. Compare with frege124 38281. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege126d 38054 | If is a function, is the successor of , and follows in the transitive closure of , then (for distinct and ) either follows or follows in the transitive closure of . Similar to Proposition 126 of [Frege1879] p. 81. Compare with frege126 38283. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege129d 38055 | If is a function and (for distinct and ) either follows or follows in the transitive closure of , the successor of is either or it follows or it comes before in the transitive closure of . Similar to Proposition 129 of [Frege1879] p. 83. Comparw with frege129 38286. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege131d 38056 | If is a function and contains all elements of and all elements before or after those elements of in the transitive closure of , then the image under of is a subclass of . Similar to Proposition 131 of [Frege1879] p. 85. Compare with frege131 38288. (Contributed by RP, 17-Jul-2020.) |
Theorem | frege133d 38057 | If is a function and and both follow in the transitive closure of , then (for distinct and ) either follows or follows in the transitive closure of (or both if it loops). Similar to Proposition 133 of [Frege1879] p. 86. Compare with frege133 38290. (Contributed by RP, 18-Jul-2020.) |
In 1879, Frege introduced notation for documenting formal reasoning about propositions (and classes) which covered elements of propositional logic, predicate calculus and reasoning about relations. However, due to the pitfalls of naive set theory, adapting this work for inclusion in set.mm required dividing statements about propositions from those about classes and identifying when a restriction to sets is required. For an overview comparing the details of Frege's two-dimensional notation and that used in set.mm, see mmfrege.html. See ru 3434 for discussion of an example of a class that is not a set. Numbered propositions from [Frege1879]. ax-frege1 38084, ax-frege2 38085, ax-frege8 38103, ax-frege28 38124, ax-frege31 38128, ax-frege41 38139, frege52 (see ax-frege52a 38151, frege52b 38183, and ax-frege52c 38182 for translations), frege54 (see ax-frege54a 38156, frege54b 38187 and ax-frege54c 38186 for translations) and frege58 (see ax-frege58a 38169, ax-frege58b 38195 and frege58c 38215 for translations) are considered "core" or axioms. However, at least ax-frege8 38103 can be derived from ax-frege1 38084 and ax-frege2 38085, see axfrege8 38101. Frege introduced implication, negation and the universal qualifier as primitives and did not in the numbered propositions use other logical connectives other than equivalence introduced in ax-frege52a 38151, frege52b 38183, and ax-frege52c 38182. In dffrege69 38226, Frege introduced hereditary to say that relation , when restricted to operate on elements of class , will only have elements of class in its domain; see df-he 38067 for a definition in terms of image and subset. In dffrege76 38233, Frege introduced notation for the concept of two sets related by the transitive closure of a relation, for which we write , which requires to also be a set. In dffrege99 38256, Frege introduced notation for the concept of two sets either identical or related by the transitive closure of a relation, for which we write , which is a superclass of sets related by the reflexive-transitive relation . Finally, in dffrege115 38272, Frege introduced notation for the concept of a relation having the property elements in its domain pair up with only one element each in its range, for which we write (to ignore any non-relational content of the class ). Frege did this without the expressing concept of a relation (or its transitive closure) as a class, and needed to invent conventions for discussing indeterminate propositions with two slots free and how to recognize which of the slots was domain and which was range. See mmfrege.html for details. English translations for specific propositions lifted in part from a translation by Stefan Bauer-Mengelberg as reprinted in From Frege to Goedel: A Source Book in Mathematical Logic, 1879-1931. An attempt to align these propositions in the larger set.mm database has also been made. See frege77d 38038 for an example. | ||
Section 2 introduces the turnstile which turns an idea which may be true into an assertion that it does hold true . Section 5 introduces implication, . Section 6 introduces the single rule of interference relied upon, modus ponens ax-mp 5. Section 7 introduces negation and with in synonyms for or , and , and two for exclusive-or corresponding to df-or 385, df-an 386, dfxor4 38058, dfxor5 38059. Section 8 introduces the problematic notation for identity of conceptual content which must be separated into cases for biimplication or class equality in this adaptation. Section 10 introduces "truth functions" for one or two variables in equally troubling notation, as the arguments may be understood to be logical predicates or collections. Here f() is interpreted to mean if- where the content of the "function" is specified by the latter two argments or logical equivalent, while g() is read as and h( ) as . This necessarily introduces a need for set theory as both and cannot hold unless is a set. (Also .) Section 11 introduces notation for generality, but there is no standard notation for generality when the variable is a proposition because it was realized after Frege that the universe of all possible propositions includes paradoxical constructions leading to the failure of naive set theory. So adopting f() as if- would result in the translation of f () as . For collections, we must generalize over set variables or run into the same problems; this leads to g() being translated as and so forth. Under this interpreation the text of section 11 gives us sp 2053 (or simpl 473 and simpr 477 and anifp 1020 in the propositional case) and statments similar to cbvalivw 1934, ax-gen 1722, alrimiv 1855, and alrimdv 1857. These last four introduce a generality and have no useful definition in terms of propositional variables. Section 12 introduces some combinations of primitive symbols and their human language counterparts. Using class notation, these can also be expressed without dummy variables. All are A, , alex 1753, eqv 3205; Some are not B, , exnal 1754, pssv 4016, nev 38062; There are no C, , alnex 1706, eq0 3929; There exist D, , df-ex 1705, 0pss 4013, n0 3931. Notation for relations between expressions also can be written in various ways. All E are P, , dfss6 3593, df-ss 3588, dfss2 3591; No F are P, , alinexa 1770, disj1 4019; Some G are not P, , exanali 1786, nssinpss 3856, nss 3663; Some H are P, , bj-exnalimn 32610, 0pssin 38064, ndisj 38063. | ||
Theorem | dfxor4 38058 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
Theorem | dfxor5 38059 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
Theorem | df3or2 38060 | Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.) |
Theorem | df3an2 38061 | Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.) |
Theorem | nev 38062* | Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.) |
Theorem | ndisj 38063* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
Theorem | 0pssin 38064* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
The statement hereditary means relation is hereditary (in the sense of Frege) in the class or . The former is only a slight reduction in the number of symbols, but this reduces the number of floating hypotheses needed to be checked. As Frege was not using the language of classes or sets, this naturally differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on. | ||
Theorem | rp-imass 38065 | If the -image of a class is a subclass of , then the restriction of to is a subset of the Cartesian product of and . (Contributed by Richard Penner, 24-Dec-2019.) |
Syntax | whe 38066 | The property of relation being hereditary in class . |
hereditary | ||
Definition | df-he 38067 | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | dfhe2 38068 | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | dfhe3 38069* | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | heeq12 38070 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | heeq1 38071 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | heeq2 38072 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | sbcheg 38073 | Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020.) |
hereditary hereditary | ||
Theorem | hess 38074 | Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | xphe 38075 | Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
hereditary | ||
Theorem | 0he 38076 | The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | 0heALT 38077 | The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | he0 38078 | Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | unhe1 38079 | The union of two relations hereditary in a class is also hereditary in a class. (Contributed by RP, 28-Mar-2020.) |
hereditary hereditary hereditary | ||
Theorem | snhesn 38080 | Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020.) |
hereditary | ||
Theorem | idhe 38081 | The identity relation is hereditary in any class. (Contributed by RP, 28-Mar-2020.) |
hereditary | ||
Theorem | psshepw 38082 | The relation between sets and their proper subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.) |
[] hereditary | ||
Theorem | sshepw 38083 | The relation between sets and their subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.) |
[] hereditary | ||
Axiom | ax-frege1 38084 | The case in which is denied, is affirmed, and is affirmed is excluded. This is evident since cannot at the same time be denied and affirmed. Axiom 1 of [Frege1879] p. 26. Identical to ax-1 6. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
Axiom | ax-frege2 38085 | If a proposition is a necessary consequence of two propositions and and one of those, , is in turn a necessary consequence of the other, , then the proposition is a necessary consequence of the latter one, , alone. Axiom 2 of [Frege1879] p. 26. Identical to ax-2 7. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
Theorem | rp-simp2-frege 38086 | Simplification of triple conjunction. Compare with simp2 1062. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-simp2 38087 | Simplification of triple conjunction. Identical to simp2 1062. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-frege3g 38088 |
Add antecedent to ax-frege2 38085. More general statement than frege3 38089.
Like ax-frege2 38085, it is essentially a closed form of mpd 15,
however it
has an extra antecedent.
It would be more natural to prove from a1i 11 and ax-frege2 38085 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege3 38089 | Add antecedent to ax-frege2 38085. Special case of rp-frege3g 38088. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-misc1-frege 38090 | Double-use of ax-frege2 38085. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-frege24 38091 | Introducing an embedded antecedent. Alternate proof for frege24 38109. Closed form for a1d 25. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-frege4g 38092 | Deduction related to distribution. (Contributed by RP, 24-Dec-2019.) |
Theorem | frege4 38093 | Special case of closed form of a2d 29. Special case of rp-frege4g 38092. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege5 38094 | A closed form of syl 17. Identical to imim2 58. Theorem *2.05 of [WhiteheadRussell] p. 100. Proposition 5 of [Frege1879] p. 32. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-7frege 38095 | Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-4frege 38096 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-6frege 38097 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-8frege 38098 | Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-frege25 38099 | Closed form for a1dd 50. Alternate route to Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) |
Theorem | frege6 38100 | A closed form of imim2d 57 which is a deduction adding nested antecedents. Proposition 6 of [Frege1879] p. 33. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |