![]() |
Metamath
Proof Explorer Theorem List (p. 61 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xpcan2 6001 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | ssrnres 6002 | Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product): the LHS expresses inclusion in the range of the restricted relation, while the RHS expresses equality with the range of the restricted and corestricted relation. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) | ||
Theorem | rninxp 6003* | Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) | ||
Theorem | dminxp 6004* | Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006.) |
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) | ||
Theorem | imainrect 6005 | Image by a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) | ||
Theorem | xpima 6006 | Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) | ||
Theorem | xpima1 6007 | Direct image by a Cartesian product (case of empty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) | ||
Theorem | xpima2 6008 | Direct image by a Cartesian product (case of nonempty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) | ||
Theorem | xpimasn 6009 | Direct image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | sossfld 6010 | The base set of a strict order is contained in the field of the relation, except possibly for one element (note that ∅ Or {𝐵}). (Contributed by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ⊆ (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | sofld 6011 | The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → 𝐴 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | cnvcnv3 6012* | The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ ◡◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} | ||
Theorem | dfrel2 6013 | Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) | ||
Theorem | dfrel4v 6014* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6699 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | dfrel4 6015* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6699 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑦𝑅 ⇒ ⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | cnvcnv 6016 | The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) (Proof shortened by BJ, 26-Nov-2021.) |
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V)) | ||
Theorem | cnvcnv2 6017 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
⊢ ◡◡𝐴 = (𝐴 ↾ V) | ||
Theorem | cnvcnvss 6018 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
⊢ ◡◡𝐴 ⊆ 𝐴 | ||
Theorem | cnvrescnv 6019 | Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023.) |
⊢ ◡(◡𝑅 ↾ 𝐵) = (𝑅 ∩ (V × 𝐵)) | ||
Theorem | cnveqb 6020 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) | ||
Theorem | cnveq0 6021 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) | ||
Theorem | dfrel3 6022 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
Theorem | elid 6023* | Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 6022 after elrid 5880. (Contributed by BJ, 28-Aug-2022.) |
⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = 〈𝑥, 𝑥〉) | ||
Theorem | dmresv 6024 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ dom (𝐴 ↾ V) = dom 𝐴 | ||
Theorem | rnresv 6025 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ ran (𝐴 ↾ V) = ran 𝐴 | ||
Theorem | dfrn4 6026 | Range defined in terms of image. (Contributed by NM, 14-May-2008.) |
⊢ ran 𝐴 = (𝐴 “ V) | ||
Theorem | csbrn 6027 | Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | rescnvcnv 6028 | The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
Theorem | cnvcnvres 6029 | The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.) |
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) | ||
Theorem | imacnvcnv 6030 | The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) | ||
Theorem | dmsnn0 6031 | The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ (V × V) ↔ dom {𝐴} ≠ ∅) | ||
Theorem | rnsnn0 6032 | The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ∈ (V × V) ↔ ran {𝐴} ≠ ∅) | ||
Theorem | dmsn0 6033 | The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.) |
⊢ dom {∅} = ∅ | ||
Theorem | cnvsn0 6034 | The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ◡{∅} = ∅ | ||
Theorem | dmsn0el 6035 | The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.) |
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅) | ||
Theorem | relsn2 6036 | A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013.) Make hypothesis an antecedent. (Revised by BJ, 12-Feb-2022.) |
⊢ (𝐴 ∈ 𝑉 → (Rel {𝐴} ↔ dom {𝐴} ≠ ∅)) | ||
Theorem | dmsnopg 6037 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐵 ∈ 𝑉 → dom {〈𝐴, 𝐵〉} = {𝐴}) | ||
Theorem | dmsnopss 6038 | The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on 𝐵). (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ dom {〈𝐴, 𝐵〉} ⊆ {𝐴} | ||
Theorem | dmpropg 6039 | The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) | ||
Theorem | dmsnop 6040 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉} = {𝐴} | ||
Theorem | dmprop 6041 | The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} | ||
Theorem | dmtpop 6042 | The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} | ||
Theorem | cnvcnvsn 6043 | Double converse of a singleton of an ordered pair. (Unlike cnvsn 6050, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} | ||
Theorem | dmsnsnsn 6044 | The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ dom {{{𝐴}}} = {𝐴} | ||
Theorem | rnsnopg 6045 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → ran {〈𝐴, 𝐵〉} = {𝐵}) | ||
Theorem | rnpropg 6046 | The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) | ||
Theorem | cnvsng 6047 | Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) | ||
Theorem | rnsnop 6048 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ran {〈𝐴, 𝐵〉} = {𝐵} | ||
Theorem | op1sta 6049 | Extract the first member of an ordered pair. (See op2nda 6052 to extract the second member, op1stb 5328 for an alternate version, and op1st 7679 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 | ||
Theorem | cnvsn 6050 | Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof shortened by BJ, 12-Feb-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉} | ||
Theorem | op2ndb 6051 | Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5328 to extract the first member, op2nda 6052 for an alternate version, and op2nd 7680 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | op2nda 6052 | Extract the second member of an ordered pair. (See op1sta 6049 to extract the first member, op2ndb 6051 for an alternate version, and op2nd 7680 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ ran {〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | opswap 6053 | Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 | ||
Theorem | cnvresima 6054 | An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) | ||
Theorem | resdm2 6055 | A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 | ||
Theorem | resdmres 6056 | Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | resresdm 6057 | A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.) |
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹)) | ||
Theorem | imadmres 6058 | The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) | ||
Theorem | mptpreima 6059* | The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} | ||
Theorem | mptiniseg 6060* | Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) | ||
Theorem | dmmpt 6061 | The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} | ||
Theorem | dmmptss 6062* | The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | dmmptg 6063* | The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) | ||
Theorem | relco 6064 | A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
⊢ Rel (𝐴 ∘ 𝐵) | ||
Theorem | dfco2 6065* | Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.) |
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) | ||
Theorem | dfco2a 6066* | Generalization of dfco2 6065, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) | ||
Theorem | coundi 6067 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) | ||
Theorem | coundir 6068 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) | ||
Theorem | cores 6069 | Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) | ||
Theorem | resco 6070 | Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) | ||
Theorem | imaco 6071 | Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) |
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) | ||
Theorem | rnco 6072 | The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵) | ||
Theorem | rnco2 6073 | The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.) |
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵) | ||
Theorem | dmco 6074 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) | ||
Theorem | coeq0 6075 | A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi 6067 and coundir 6068 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅) | ||
Theorem | coiun 6076* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv1 6077 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv2 6078 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cores2 6079 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) | ||
Theorem | co02 6080 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ∘ ∅) = ∅ | ||
Theorem | co01 6081 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∘ 𝐴) = ∅ | ||
Theorem | coi1 6082 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴) | ||
Theorem | coi2 6083 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴) | ||
Theorem | coires1 6084 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | coass 6085 | Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.) |
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) | ||
Theorem | relcnvtrg 6086 | General form of relcnvtr 6087. (Contributed by Peter Mazsa, 17-Oct-2023.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇)) | ||
Theorem | relcnvtr 6087 | A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Peter Mazsa, 17-Oct-2023.) |
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅)) | ||
Theorem | relssdmrn 6088 | A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) |
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
Theorem | resssxp 6089 | 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 RP, 24-Dec-2019.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐵 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐵)) | ||
Theorem | cnvssrndm 6090 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) | ||
Theorem | cossxp 6091 | Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | ||
Theorem | relrelss 6092 | Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.) |
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) × V)) | ||
Theorem | unielrel 6093 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) | ||
Theorem | relfld 6094 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | relresfld 6095 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
Theorem | relcoi2 6096 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
Theorem | relcoi1 6097 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) | ||
Theorem | unidmrn 6098 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴) | ||
Theorem | relcnvfld 6099 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅) | ||
Theorem | dfdm2 6100 | Alternate definition of domain df-dm 5529 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |