Home | Metamath
Proof Explorer Theorem List (p. 364 of 406) | < 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-26571) |
Hilbert Space Explorer
(26572-28094) |
Users' Mathboxes
(28095-40593) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | relexpmulnn 36301 | 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 36302 | 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 36303* | 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 36304* | 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 36305 | 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 36306 | Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.) |
Theorem | relexp0idm 36307 | Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.) |
Theorem | relexp0a 36308 | Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.) |
Theorem | relexpxpmin 36309 | 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 36310 | 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 13117 or when the sum of the powers isn't 1 as shown by relexpaddg 13116. (Contributed by RP, 3-Jun-2020.) |
Theorem | iunrelexpuztr 36311* | The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 13123. (Contributed by RP, 4-Jun-2020.) |
Theorem | dftrcl3 36312* | Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.) |
Theorem | brfvtrcld 36313* | 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 36314 | A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.) |
Theorem | trclfvcom 36315 | The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.) |
Theorem | cnvtrclfv 36316 | The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.) |
Theorem | cotrcltrcl 36317 | The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.) |
Theorem | trclimalb2 36318 | Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.) |
Theorem | brtrclfv2 36319* | Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.) |
Theorem | trclfvdecomr 36320 | 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 36321 | 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 36322 | 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 36323 | 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 36324 | 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 36325* | Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 13125. (Contributed by RP, 5-Jun-2020.) |
Theorem | brfvrtrcld 36326* | 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 13120. (Contributed by RP, 22-Jul-2020.) |
Theorem | fvrtrcllb0d 36327 | 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 36328 | 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 36329 | A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.) |
Theorem | dfrtrcl4 36330 | 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 36331 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.) |
Theorem | cortrcltrcl 36332 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | corclrtrcl 36333 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cotrclrcl 36334 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.) |
Theorem | cortrclrcl 36335 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cotrclrtrcl 36336 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
Theorem | cortrclrtrcl 36337 | 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 36338 | 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 36536. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege81d 36339 | 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 36540. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege83d 36340 | 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 36542. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege96d 36341 | 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 36555. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege87d 36342 | 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 36546. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege91d 36343 | If follows in then follows in the transitive closure of . Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 36550. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege97d 36344 | 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 36556. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege98d 36345 | 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 36557. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege102d 36346 | 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 36561. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege106d 36347 | If follows in , then either and are the same or follows in . Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 36565. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege108d 36348 | 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 36567. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege109d 36349 | 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 36568. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege114d 36350 | 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 36573. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege111d 36351 | 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 36570. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege122d 36352 | 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 36581. (Contributed by RP, 15-Jul-2020.) |
Theorem | frege124d 36353 | 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 36583. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege126d 36354 | 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 36585. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege129d 36355 | 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 36588. (Contributed by RP, 16-Jul-2020.) |
Theorem | frege131d 36356 | 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 36590. (Contributed by RP, 17-Jul-2020.) |
Theorem | frege133d 36357 | 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 36592. (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 3266 for discussion of an example of a class that is not a set. Numbered propositions from [Frege1879]. ax-frege1 36386, ax-frege2 36387, ax-frege8 36405, ax-frege28 36426, ax-frege31 36430, ax-frege41 36441, frege52 (see ax-frege52a 36453, frege52b 36485, and ax-frege52c 36484 for translations), frege54 (see ax-frege54a 36458, frege54b 36489 and ax-frege54c 36488 for translations) and frege58 (see ax-frege58a 36471, ax-frege58b 36497 and frege58c 36517 for translations) are considered "core" or axioms. However, at least ax-frege8 36405 can be derived from ax-frege1 36386 and ax-frege2 36387, see axfrege8 36403. 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 36453, frege52b 36485, and ax-frege52c 36484. In dffrege69 36528, 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 36368 for a definition in terms of image and subset. In dffrege76 36535, 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 36558, 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 36574, 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 36338 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 372, df-an 373, dfxor4 36358, dfxor5 36359. 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 1937 (or simpl 459 and simpr 463 and anifp 1433 in the propositional case) and statments similar to cbvalivw 1850, ax-gen 1669, alrimiv 1773, and alrimdv 1775. 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 1698, eqv 3748; Some are not B, , exnal 1699, pssv 3804, nev 36362; There are no C, , alnex 1665, eq0 3747; There exist D, , df-ex 1664, 0pss 3802, n0 3741. Notation for relations between expressions also can be written in various ways. All E are P, , dfss6 36363, df-ss 3418, dfss2 3421; No F are P, , alinexa 1713, disj1 3807; Some G are not P, , exanali 1721, nssinpss 3675, nss 3490; Some H are P, , bj-exnalimn 31221, 0pssin 36365, ndisj 36364. | ||
Theorem | dfxor4 36358 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
Theorem | dfxor5 36359 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
Theorem | df3or2 36360 | Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.) |
Theorem | df3an2 36361 | Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.) |
Theorem | nev 36362* | Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.) |
Theorem | dfss6 36363* | Another definition of subclasshood. (Contributed by RP, 16-Apr-2020.) |
Theorem | ndisj 36364* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
Theorem | 0pssin 36365* | 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 wasn't 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 36366 | 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 36367 | The property of relation being hereditary in class . |
hereditary | ||
Definition | df-he 36368 | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | dfhe2 36369 | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | dfhe3 36370* | The property of relation being hereditary in class . (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | heeq12 36371 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | heeq1 36372 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | heeq2 36373 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | sbcheg 36374 | Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020.) |
hereditary hereditary | ||
Theorem | hess 36375 | Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
hereditary hereditary | ||
Theorem | xphe 36376 | Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
hereditary | ||
Theorem | xpheOLD 36377 | Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) Obsolete version of xphe 36376 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
hereditary | ||
Theorem | 0he 36378 | The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | 0heALT 36379 | 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 36380 | Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020.) |
hereditary | ||
Theorem | unhe1 36381 | 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 36382 | Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020.) |
hereditary | ||
Theorem | idhe 36383 | The identity relation is hereditary in any class. (Contributed by RP, 28-Mar-2020.) |
hereditary | ||
Theorem | psshepw 36384 | 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 36385 | 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 36386 | 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 36387 | 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 36388 | Simplification of triple conjunction. Compare with simp2 1009. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-simp2 36389 | Simplification of triple conjunction. Identical to simp2 1009. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-frege3g 36390 |
Add antecedent to ax-frege2 36387. More general statement than frege3 36391.
Like ax-frege2 36387, 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 36387 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege3 36391 | Add antecedent to ax-frege2 36387. Special case of rp-frege3g 36390. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-misc1-frege 36392 | Double-use of ax-frege2 36387. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | rp-frege24 36393 | Introducing an embedded antecedent. Alternate proof for frege24 36411. Closed form for a1d 26. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-frege4g 36394 | Deduction related to distribution. (Contributed by RP, 24-Dec-2019.) |
Theorem | frege4 36395 | Special case of closed form of a2d 29. Special case of rp-frege4g 36394. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
Theorem | frege5 36396 | A closed form of syl 17. Identical to imim2 55. 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 36397 | Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-4frege 36398 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-6frege 36399 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
Theorem | rp-8frege 36400 | Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |