![]() |
Metamath
Proof Explorer Theorem List (p. 431 of 484) | < 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: | ![]() (1-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ifpbibib 43001 | Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
β’ (if-(π, (π β π), (π β π)) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpxorxorb 43002 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
β’ (if-(π, (π β» π), (π β» π)) β (if-(π, π, π) β» if-(π, π, π))) | ||
Theorem | rp-fakeimass 43003 | A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
β’ ((π β¨ π) β (((π β π) β π) β (π β (π β π)))) | ||
Theorem | rp-fakeanorass 43004 | A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.) |
β’ ((π β π) β (((π β§ π) β¨ π) β (π β§ (π β¨ π)))) | ||
Theorem | rp-fakeoranass 43005 | A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
β’ ((π β π) β (((π β¨ π) β§ π) β (π β¨ (π β§ π)))) | ||
Theorem | rp-fakeinunass 43006 | A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.) |
β’ (πΆ β π΄ β ((π΄ β© π΅) βͺ πΆ) = (π΄ β© (π΅ βͺ πΆ))) | ||
Theorem | rp-fakeuninass 43007 | A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
β’ (π΄ β πΆ β ((π΄ βͺ π΅) β© πΆ) = (π΄ βͺ (π΅ β© πΆ))) | ||
Membership in the class of finite sets can be expressed in many ways. | ||
Theorem | rp-isfinite5 43008* | A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some π β β0. (Contributed by RP, 3-Mar-2020.) |
β’ (π΄ β Fin β βπ β β0 (1...π) β π΄) | ||
Theorem | rp-isfinite6 43009* | A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some π β β. (Contributed by RP, 10-Mar-2020.) |
β’ (π΄ β Fin β (π΄ = β β¨ βπ β β (1...π) β π΄)) | ||
Theorem | intabssd 43010* | When for each element π¦ there is a subset π΄ which may substituted for π₯ such that π¦ satisfying π implies π₯ satisfies π then the intersection of all π₯ that satisfy π is a subclass the intersection of all π¦ that satisfy π. (Contributed by RP, 17-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ = π΄) β (π β π)) & β’ (π β π΄ β π¦) β β’ (π β β© {π₯ β£ π} β β© {π¦ β£ π}) | ||
Theorem | eu0 43011* | There is only one empty set. (Contributed by RP, 1-Oct-2023.) |
β’ (βπ₯ Β¬ π₯ β β β§ β!π₯βπ¦ Β¬ π¦ β π₯) | ||
Theorem | epelon2 43012 | Over the ordinal numbers, one may define the relation π΄ E π΅ iff π΄ β π΅ and one finds that, under this ordering, On is a well-ordered class, see epweon 7772. This is a weak form of epelg 5578 which only requires that we know π΅ to be a set. (Contributed by RP, 27-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ E π΅ β π΄ β π΅)) | ||
Theorem | ontric3g 43013* | For all π₯, π¦ β On, one and only one of the following hold: π₯ β π¦, π¦ = π₯, or π¦ β π₯. This is a transparent strict trichotomy. (Contributed by RP, 27-Sep-2023.) |
β’ βπ₯ β On βπ¦ β On ((π₯ β π¦ β Β¬ (π¦ = π₯ β¨ π¦ β π₯)) β§ (π¦ = π₯ β Β¬ (π₯ β π¦ β¨ π¦ β π₯)) β§ (π¦ β π₯ β Β¬ (π₯ β π¦ β¨ π¦ = π₯))) | ||
Theorem | dfsucon 43014* | π΄ is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023.) |
β’ ((Ord π΄ β§ Β¬ Lim π΄ β§ π΄ β β ) β βπ₯ β On π΄ = suc π₯) | ||
Theorem | snen1g 43015 | A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.) |
β’ ({π΄} β 1o β π΄ β V) | ||
Theorem | snen1el 43016 | A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.) |
β’ ({π΄} β 1o β π΄ β {π΄}) | ||
Theorem | sn1dom 43017 | A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.) |
β’ {π΄} βΌ 1o | ||
Theorem | pr2dom 43018 | An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.) |
β’ {π΄, π΅} βΌ 2o | ||
Theorem | tr3dom 43019 | An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.) |
β’ {π΄, π΅, πΆ} βΌ 3o | ||
Theorem | ensucne0 43020 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.) |
β’ (π΄ β suc π΅ β π΄ β β ) | ||
Theorem | ensucne0OLD 43021 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β suc π΅ β π΄ β β ) | ||
Theorem | dfom6 43022 | Let Ο be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
β’ Ο = βͺ (On β© Fin) | ||
Theorem | infordmin 43023 | Ο is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
β’ βπ₯ β (On β Fin)Ο β π₯ | ||
Theorem | iscard4 43024 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
β’ ((cardβπ΄) = π΄ β π΄ β ran card) | ||
Theorem | minregex 43025* | Given any cardinal number π΄, there exists an argument π₯, which yields the least regular uncountable value of β΅ which is greater to or equal to π΄. This proof uses AC. (Contributed by RP, 23-Nov-2023.) |
β’ (π΄ β (ran card β Ο) β βπ₯ β On π₯ = β© {π¦ β On β£ (β β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) | ||
Theorem | minregex2 43026* | Given any cardinal number π΄, there exists an argument π₯, which yields the least regular uncountable value of β΅ which dominates π΄. This proof uses AC. (Contributed by RP, 24-Nov-2023.) |
β’ (π΄ β (ran card β Ο) β βπ₯ β On π₯ = β© {π¦ β On β£ (β β π¦ β§ π΄ βΌ (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) | ||
Theorem | iscard5 43027* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
β’ ((cardβπ΄) = π΄ β (π΄ β On β§ βπ₯ β π΄ Β¬ π₯ β π΄)) | ||
Theorem | elrncard 43028* | Let us define a cardinal number to be an element π΄ β On such that π΄ is not equipotent with any π₯ β π΄. (Contributed by RP, 1-Oct-2023.) |
β’ (π΄ β ran card β (π΄ β On β§ βπ₯ β π΄ Β¬ π₯ β π΄)) | ||
Theorem | harval3 43029* | (harβπ΄) is the least cardinal that is greater than π΄. (Contributed by RP, 4-Nov-2023.) |
β’ (π΄ β dom card β (harβπ΄) = β© {π₯ β ran card β£ π΄ βΊ π₯}) | ||
Theorem | harval3on 43030* | For any ordinal number π΄ let (harβπ΄) denote the least cardinal that is greater than π΄. (Contributed by RP, 4-Nov-2023.) |
β’ (π΄ β On β (harβπ΄) = β© {π₯ β ran card β£ π΄ βΊ π₯}) | ||
Theorem | omssrncard 43031 | All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023.) |
β’ Ο β ran card | ||
Theorem | 0iscard 43032 | 0 is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
β’ β β ran card | ||
Theorem | 1iscard 43033 | 1 is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
β’ 1o β ran card | ||
Theorem | omiscard 43034 | Ο is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
β’ Ο β ran card | ||
Theorem | sucomisnotcard 43035 | Ο +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023.) |
β’ Β¬ (Ο +o 1o) β ran card | ||
Theorem | nna1iscard 43036 | For any natural number, the add one operation is results in a cardinal number. (Contributed by RP, 1-Oct-2023.) |
β’ (π β Ο β (π +o 1o) β ran card) | ||
Theorem | har2o 43037 | The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023.) |
β’ (harβ2o) = 3o | ||
Theorem | en2pr 43038* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
β’ (π΄ β 2o β βπ₯βπ¦(π΄ = {π₯, π¦} β§ π₯ β π¦)) | ||
Theorem | pr2cv 43039 | If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.) |
β’ ({π΄, π΅} β 2o β (π΄ β V β§ π΅ β V)) | ||
Theorem | pr2el1 43040 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΄ β {π΄, π΅}) | ||
Theorem | pr2cv1 43041 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΄ β V) | ||
Theorem | pr2el2 43042 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΅ β {π΄, π΅}) | ||
Theorem | pr2cv2 43043 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΅ β V) | ||
Theorem | pren2 43044 | An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.) |
β’ ({π΄, π΅} β 2o β (π΄ β V β§ π΅ β V β§ π΄ β π΅)) | ||
Theorem | pr2eldif1 43045 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΄ β ({π΄, π΅} β {π΅})) | ||
Theorem | pr2eldif2 43046 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
β’ ({π΄, π΅} β 2o β π΅ β ({π΄, π΅} β {π΄})) | ||
Theorem | pren2d 43047 | A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) β β’ (π β {π΄, π΅} β 2o) | ||
Theorem | aleph1min 43048 | (β΅β1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.) |
β’ (β΅β1o) = β© {π₯ β On β£ Ο βΊ π₯} | ||
Theorem | alephiso2 43049 | β΅ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
β’ β΅ Isom E , βΊ (On, {π₯ β ran card β£ Ο β π₯}) | ||
Theorem | alephiso3 43050 | β΅ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
β’ β΅ Isom E , βΊ (On, (ran card β Ο)) | ||
Theorem | pwelg 43051* | The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.) |
β’ (βπ₯ β π΅ (βͺ π₯ β π΅ β§ π« π₯ β π΅) β (π΄ β π΅ β π« π΄ β π΅)) | ||
Theorem | pwinfig 43052* | The powerclass of an infinite set is an infinite set, and vice-versa. Here π΅ is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.) |
β’ (βπ₯ β π΅ (βͺ π₯ β π΅ β§ π« π₯ β π΅) β (π΄ β (π΅ β Fin) β π« π΄ β (π΅ β Fin))) | ||
Theorem | pwinfi2 43053 | The powerclass of an infinite set is an infinite set, and vice-versa. Here π is a weak universe. (Contributed by RP, 21-Mar-2020.) |
β’ (π β WUni β (π΄ β (π β Fin) β π« π΄ β (π β Fin))) | ||
Theorem | pwinfi3 43054 | The powerclass of an infinite set is an infinite set, and vice-versa. Here π is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.) |
β’ ((π β Tarski β§ Tr π) β (π΄ β (π β Fin) β π« π΄ β (π β Fin))) | ||
Theorem | pwinfi 43055 | The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.) |
β’ (π΄ β (V β Fin) β π« π΄ β (V β Fin)) | ||
While there is not yet a definition, the finite intersection property of a class is introduced by fiint 9343 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6396, ordelinel 6466), chains of sets ordered by the proper subset relation (sorpssin 7731), various sets in the field of topology (inopn 22814, incld 22960, innei 23042, ... ) and "universal" classes like weak universes (wunin 10731, tskin 10777) and the class of all sets (inex1g 5315). | ||
Theorem | fipjust 43056* | A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020.) |
β’ (βπ’ β π΄ βπ£ β π΄ (π’ β© π£) β π΄ β βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄) | ||
Theorem | cllem0 43057* | The class of all sets with property π(π§) is closed under the binary operation on sets defined in π (π₯, π¦). (Contributed by RP, 3-Jan-2020.) |
β’ π = {π§ β£ π} & β’ π β π & β’ (π§ = π β (π β π)) & β’ (π§ = π₯ β (π β π)) & β’ (π§ = π¦ β (π β π)) & β’ ((π β§ π) β π) β β’ βπ₯ β π βπ¦ β π π β π | ||
Theorem | superficl 43058* | The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π΅ β π§} β β’ βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄ | ||
Theorem | superuncl 43059* | The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π΅ β π§} β β’ βπ₯ β π΄ βπ¦ β π΄ (π₯ βͺ π¦) β π΄ | ||
Theorem | ssficl 43060* | The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π§ β π΅} β β’ βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄ | ||
Theorem | ssuncl 43061* | The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π§ β π΅} β β’ βπ₯ β π΄ βπ¦ β π΄ (π₯ βͺ π¦) β π΄ | ||
Theorem | ssdifcl 43062* | The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π§ β π΅} β β’ βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦) β π΄ | ||
Theorem | sssymdifcl 43063* | The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.) |
β’ π΄ = {π§ β£ π§ β π΅} β β’ βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦) βͺ (π¦ β π₯)) β π΄ | ||
Theorem | fiinfi 43064* | If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.) |
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄) & β’ (π β βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β π΅) & β’ (π β πΆ = (π΄ β© π΅)) β β’ (π β βπ₯ β πΆ βπ¦ β πΆ (π₯ β© π¦) β πΆ) | ||
Theorem | rababg 43065 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
β’ (βπ₯(π β π₯ β π΄) β {π₯ β π΄ β£ π} = {π₯ β£ π}) | ||
Theorem | elinintab 43066* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
β’ (π΄ β (π΅ β© β© {π₯ β£ π}) β (π΄ β π΅ β§ βπ₯(π β π΄ β π₯))) | ||
Theorem | elmapintrab 43067* | Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.) |
β’ πΆ β V & β’ πΆ β π΅ β β’ (π΄ β π β (π΄ β β© {π€ β π« π΅ β£ βπ₯(π€ = πΆ β§ π)} β ((βπ₯π β π΄ β π΅) β§ βπ₯(π β π΄ β πΆ)))) | ||
Theorem | elinintrab 43068* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.) |
β’ (π΄ β π β (π΄ β β© {π€ β π« π΅ β£ βπ₯(π€ = (π΅ β© π₯) β§ π)} β ((βπ₯π β π΄ β π΅) β§ βπ₯(π β π΄ β π₯)))) | ||
Theorem | inintabss 43069* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
β’ (π΄ β© β© {π₯ β£ π}) β β© {π€ β π« π΄ β£ βπ₯(π€ = (π΄ β© π₯) β§ π)} | ||
Theorem | inintabd 43070* | Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.) |
β’ (π β βπ₯π) β β’ (π β (π΄ β© β© {π₯ β£ π}) = β© {π€ β π« π΄ β£ βπ₯(π€ = (π΄ β© π₯) β§ π)}) | ||
Theorem | xpinintabd 43071* | Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.) |
β’ (π β βπ₯π) β β’ (π β ((π΄ Γ π΅) β© β© {π₯ β£ π}) = β© {π€ β π« (π΄ Γ π΅) β£ βπ₯(π€ = ((π΄ Γ π΅) β© π₯) β§ π)}) | ||
Theorem | relintabex 43072 | If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.) |
β’ (Rel β© {π₯ β£ π} β βπ₯π) | ||
Theorem | elcnvcnvintab 43073* | Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
β’ (π΄ β β‘β‘β© {π₯ β£ π} β (π΄ β (V Γ V) β§ βπ₯(π β π΄ β π₯))) | ||
Theorem | relintab 43074* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
β’ (Rel β© {π₯ β£ π} β β© {π₯ β£ π} = β© {π€ β π« (V Γ V) β£ βπ₯(π€ = β‘β‘π₯ β§ π)}) | ||
Theorem | nonrel 43075 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
β’ (π΄ β β‘β‘π΄) = (π΄ β (V Γ V)) | ||
Theorem | elnonrel 43076 | Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.) |
β’ (β¨π, πβ© β (π΄ β β‘β‘π΄) β (β β π΄ β§ Β¬ (π β V β§ π β V))) | ||
Theorem | cnvssb 43077 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
β’ (Rel π΄ β (π΄ β π΅ β β‘π΄ β β‘π΅)) | ||
Theorem | relnonrel 43078 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
β’ (Rel π΄ β (π΄ β β‘β‘π΄) = β ) | ||
Theorem | cnvnonrel 43079 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
β’ β‘(π΄ β β‘β‘π΄) = β | ||
Theorem | brnonrel 43080 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
β’ ((π β π β§ π β π) β Β¬ π(π΄ β β‘β‘π΄)π) | ||
Theorem | dmnonrel 43081 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ dom (π΄ β β‘β‘π΄) = β | ||
Theorem | rnnonrel 43082 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ ran (π΄ β β‘β‘π΄) = β | ||
Theorem | resnonrel 43083 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ ((π΄ β β‘β‘π΄) βΎ π΅) = β | ||
Theorem | imanonrel 43084 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ ((π΄ β β‘β‘π΄) β π΅) = β | ||
Theorem | cononrel1 43085 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ ((π΄ β β‘β‘π΄) β π΅) = β | ||
Theorem | cononrel2 43086 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
β’ (π΄ β (π΅ β β‘β‘π΅)) = β | ||
See also idssxp 6048 by Thierry Arnoux. | ||
Theorem | elmapintab 43087* | Two ways to say a set is an element of mapped intersection of a class. Here πΉ maps elements of πΆ to elements of β© {π₯ β£ π} or π₯. (Contributed by RP, 19-Aug-2020.) |
β’ (π΄ β π΅ β (π΄ β πΆ β§ (πΉβπ΄) β β© {π₯ β£ π})) & β’ (π΄ β πΈ β (π΄ β πΆ β§ (πΉβπ΄) β π₯)) β β’ (π΄ β π΅ β (π΄ β πΆ β§ βπ₯(π β π΄ β πΈ))) | ||
Theorem | fvnonrel 43088 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
β’ ((π΄ β β‘β‘π΄)βπ) = β | ||
Theorem | elinlem 43089 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
β’ (π΄ β (π΅ β© πΆ) β (π΄ β π΅ β§ ( I βπ΄) β πΆ)) | ||
Theorem | elcnvcnvlem 43090 | Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.) |
β’ (π΄ β β‘β‘π΅ β (π΄ β (V Γ V) β§ ( I βπ΄) β π΅)) | ||
Original probably needs new subsection for Relation-related existence theorems. | ||
Theorem | cnvcnvintabd 43091* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
β’ (π β βπ₯π) β β’ (π β β‘β‘β© {π₯ β£ π} = β© {π€ β π« (V Γ V) β£ βπ₯(π€ = β‘β‘π₯ β§ π)}) | ||
Theorem | elcnvlem 43092 | Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.) |
β’ πΉ = (π₯ β (V Γ V) β¦ β¨(2nd βπ₯), (1st βπ₯)β©) β β’ (π΄ β β‘π΅ β (π΄ β (V Γ V) β§ (πΉβπ΄) β π΅)) | ||
Theorem | elcnvintab 43093* | Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.) |
β’ (π΄ β β‘β© {π₯ β£ π} β (π΄ β (V Γ V) β§ βπ₯(π β π΄ β β‘π₯))) | ||
Theorem | cnvintabd 43094* | Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.) |
β’ (π β βπ₯π) β β’ (π β β‘β© {π₯ β£ π} = β© {π€ β π« (V Γ V) β£ βπ₯(π€ = β‘π₯ β§ π)}) | ||
Theorem | undmrnresiss 43095* | Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 43096. (Contributed by RP, 26-Sep-2020.) |
β’ (( I βΎ (dom π΄ βͺ ran π΄)) β π΅ β βπ₯βπ¦(π₯π΄π¦ β (π₯π΅π₯ β§ π¦π΅π¦))) | ||
Theorem | reflexg 43096* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
β’ (( I βΎ (dom π΄ βͺ ran π΄)) β π΄ β βπ₯βπ¦(π₯π΄π¦ β (π₯π΄π₯ β§ π¦π΄π¦))) | ||
Theorem | cnvssco 43097* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
β’ (β‘π΄ β β‘(π΅ β πΆ) β βπ₯βπ¦βπ§(π₯π΄π¦ β (π₯πΆπ§ β§ π§π΅π¦))) | ||
Theorem | refimssco 43098 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
β’ (( I βΎ (dom π΄ βͺ ran π΄)) β π΄ β β‘π΄ β β‘(π΄ β π΄)) | ||
Theorem | cleq2lem 43099 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
β’ (π΄ = π΅ β (π β π)) β β’ (π΄ = π΅ β ((π β π΄ β§ π) β (π β π΅ β§ π))) | ||
Theorem | cbvcllem 43100* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
β’ (π₯ = π¦ β (π β π)) β β’ {π₯ β£ (π β π₯ β§ π)} = {π¦ β£ (π β π¦ β§ π)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |