| Metamath
Proof Explorer Theorem List (p. 63 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | imainrect 6201 | 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 6202 | Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
| ⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) | ||
| Theorem | xpima1 6203 | Direct image by a Cartesian product (case of empty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
| ⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) | ||
| Theorem | xpima2 6204 | Direct image by a Cartesian product (case of nonempty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
| ⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) | ||
| Theorem | xpimasn 6205 | 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 6206 | 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 6207 | 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 6208* | 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 6209 | Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
| ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) | ||
| Theorem | dfrel4v 6210* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6967 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) |
| ⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
| Theorem | dfrel4 6211* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6967 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑦𝑅 ⇒ ⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
| Theorem | cnvcnv 6212 | 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 6213 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
| ⊢ ◡◡𝐴 = (𝐴 ↾ V) | ||
| Theorem | cnvcnvss 6214 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
| ⊢ ◡◡𝐴 ⊆ 𝐴 | ||
| Theorem | cnvrescnv 6215 | Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023.) |
| ⊢ ◡(◡𝑅 ↾ 𝐵) = (𝑅 ∩ (V × 𝐵)) | ||
| Theorem | cnveqb 6216 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
| ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) | ||
| Theorem | cnveq0 6217 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
| ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) | ||
| Theorem | dfrel3 6218 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
| ⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
| Theorem | elid 6219* | Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 6218 after elrid 6064. (Contributed by BJ, 28-Aug-2022.) |
| ⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = 〈𝑥, 𝑥〉) | ||
| Theorem | dmresv 6220 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
| ⊢ dom (𝐴 ↾ V) = dom 𝐴 | ||
| Theorem | rnresv 6221 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
| ⊢ ran (𝐴 ↾ V) = ran 𝐴 | ||
| Theorem | dfrn4 6222 | Range defined in terms of image. (Contributed by NM, 14-May-2008.) |
| ⊢ ran 𝐴 = (𝐴 “ V) | ||
| Theorem | csbrn 6223 | Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) |
| ⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 | ||
| Theorem | rescnvcnv 6224 | 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 6225 | The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.) |
| ⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) | ||
| Theorem | imacnvcnv 6226 | The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
| ⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) | ||
| Theorem | dmsnn0 6227 | 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 6228 | 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 6229 | The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.) |
| ⊢ dom {∅} = ∅ | ||
| Theorem | cnvsn0 6230 | The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.) |
| ⊢ ◡{∅} = ∅ | ||
| Theorem | dmsn0el 6231 | 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 6232 | 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 6233 | 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 6234 | 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 6235 | The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) | ||
| Theorem | dmsnop 6236 | 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 6237 | The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.) |
| ⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} | ||
| Theorem | dmtpop 6238 | The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.) |
| ⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} | ||
| Theorem | cnvcnvsn 6239 | Double converse of a singleton of an ordered pair. (Unlike cnvsn 6246, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
| ⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} | ||
| Theorem | dmsnsnsn 6240 | 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 6241 | 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 6242 | The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) | ||
| Theorem | cnvsng 6243 | Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) | ||
| Theorem | rnsnop 6244 | 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 6245 | Extract the first member of an ordered pair. (See op2nda 6248 to extract the second member, op1stb 5476 for an alternate version, and op1st 8022 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 | ||
| Theorem | cnvsn 6246 | 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 6247 | Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5476 to extract the first member, op2nda 6248 for an alternate version, and op2nd 8023 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 | ||
| Theorem | op2nda 6248 | Extract the second member of an ordered pair. (See op1sta 6245 to extract the first member, op2ndb 6247 for an alternate version, and op2nd 8023 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ ran {〈𝐴, 𝐵〉} = 𝐵 | ||
| Theorem | opswap 6249 | Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.) |
| ⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 | ||
| Theorem | cnvresima 6250 | An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
| ⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) | ||
| Theorem | resdm2 6251 | A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.) |
| ⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 | ||
| Theorem | resdmres 6252 | Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
| ⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
| Theorem | resresdm 6253 | A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.) |
| ⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹)) | ||
| Theorem | imadmres 6254 | The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
| ⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) | ||
| Theorem | resdmss 6255 | Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024.) |
| ⊢ dom (𝐴 ↾ 𝐵) ⊆ 𝐵 | ||
| Theorem | resdifdi 6256 | Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.) |
| ⊢ (𝐴 ↾ (𝐵 ∖ 𝐶)) = ((𝐴 ↾ 𝐵) ∖ (𝐴 ↾ 𝐶)) | ||
| Theorem | resdifdir 6257 | Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.) |
| ⊢ ((𝐴 ∖ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∖ (𝐵 ↾ 𝐶)) | ||
| Theorem | mptpreima 6258* | The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} | ||
| Theorem | mptiniseg 6259* | Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) | ||
| Theorem | dmmpt 6260 | 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 6261* | The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | dmmptg 6262* | 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 | rnmpt0f 6263* | The range of a function in maps-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 = ∅ ↔ 𝐴 = ∅)) | ||
| Theorem | rnmptn0 6264* | The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 ≠ ∅) | ||
| Theorem | dfco2 6265* | Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.) |
| ⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) | ||
| Theorem | dfco2a 6266* | Generalization of dfco2 6265, 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 6267 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) | ||
| Theorem | coundir 6268 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) | ||
| Theorem | cores 6269 | Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) | ||
| Theorem | resco 6270 | Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
| ⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) | ||
| Theorem | imaco 6271 | Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) (Proof shortened by Wolf Lammen, 16-May-2025.) |
| ⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) | ||
| Theorem | rnco 6272 | 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 6273 | The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.) |
| ⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵) | ||
| Theorem | dmco 6274 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
| ⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) | ||
| Theorem | coeq0 6275 | 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 6267 and coundir 6268 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
| ⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅) | ||
| Theorem | coiun 6276* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
| ⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
| Theorem | cocnvcnv1 6277 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
| ⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) | ||
| Theorem | cocnvcnv2 6278 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
| ⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) | ||
| Theorem | cores2 6279 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
| ⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) | ||
| Theorem | co02 6280 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
| ⊢ (𝐴 ∘ ∅) = ∅ | ||
| Theorem | co01 6281 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
| ⊢ (∅ ∘ 𝐴) = ∅ | ||
| Theorem | coi1 6282 | 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 6283 | 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 6284 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
| ⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
| Theorem | coass 6285 | 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 6286 | General form of relcnvtr 6287. (Contributed by Peter Mazsa, 17-Oct-2023.) |
| ⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇)) | ||
| Theorem | relcnvtr 6287 | 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 6288 | 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.) (Proof shortened by SN, 23-Dec-2024.) |
| ⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
| Theorem | relssdmrnOLD 6289 | Obsolete version of relssdmrn 6288 as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
| Theorem | resssxp 6290 | 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 6291 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) | ||
| Theorem | cossxp 6292 | Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | ||
| Theorem | relrelss 6293 | 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 6294 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
| ⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) | ||
| Theorem | relfld 6295 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
| ⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
| Theorem | relresfld 6296 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
| ⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
| Theorem | relcoi2 6297 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
| ⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
| Theorem | relcoi1 6298 | 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 6299 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
| ⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴) | ||
| Theorem | relcnvfld 6300 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
| ⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |