![]() |
Metamath
Proof Explorer Theorem List (p. 62 of 472) | < 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-29688) |
![]() (29689-31211) |
![]() (31212-47146) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imaundir 6101 | The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.) |
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) | ||
Theorem | cnvimassrndm 6102 | The preimage of a superset of the range of a class is the domain of the class. Generalization of cnvimarndm 6032 for subsets. (Contributed by AV, 18-Sep-2024.) |
⊢ (ran 𝐹 ⊆ 𝐴 → (◡𝐹 “ 𝐴) = dom 𝐹) | ||
Theorem | dminss 6103 | An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising". (Contributed by NM, 11-Aug-2004.) |
⊢ (dom 𝑅 ∩ 𝐴) ⊆ (◡𝑅 “ (𝑅 “ 𝐴)) | ||
Theorem | imainss 6104 | An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) | ||
Theorem | inimass 6105 | The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) | ||
Theorem | inimasn 6106 | The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) | ||
Theorem | cnvxp 6107 | The converse of a Cartesian product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴) | ||
Theorem | xp0 6108 | The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) |
⊢ (𝐴 × ∅) = ∅ | ||
Theorem | xpnz 6109 | The Cartesian product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by NM, 30-Jun-2006.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) | ||
Theorem | xpeq0 6110 | At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) | ||
Theorem | xpdisj1 6111 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) | ||
Theorem | xpdisj2 6112 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) | ||
Theorem | xpsndisj 6113 | Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.) |
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) | ||
Theorem | difxp 6114 | Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐶 × 𝐷) ∖ (𝐴 × 𝐵)) = (((𝐶 ∖ 𝐴) × 𝐷) ∪ (𝐶 × (𝐷 ∖ 𝐵))) | ||
Theorem | difxp1 6115 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐴 ∖ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∖ (𝐵 × 𝐶)) | ||
Theorem | difxp2 6116 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) = ((𝐴 × 𝐵) ∖ (𝐴 × 𝐶)) | ||
Theorem | djudisj 6117* | Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) | ||
Theorem | xpdifid 6118* | The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I ) | ||
Theorem | resdisj 6119 | A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅) | ||
Theorem | rnxp 6120 | The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) |
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) | ||
Theorem | dmxpss 6121 | The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.) |
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 | ||
Theorem | rnxpss 6122 | The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 | ||
Theorem | rnxpid 6123 | The range of a Cartesian square. (Contributed by FL, 17-May-2010.) |
⊢ ran (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ssxpb 6124 | A Cartesian product subclass relationship is equivalent to the conjunction of the analogous relationships for the factors. (Contributed by NM, 17-Dec-2008.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) | ||
Theorem | xp11 6125 | The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | xpcan 6126 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | xpcan2 6127 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | ssrnres 6128 | 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 6129* | 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 6130* | 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 6131 | 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 6132 | Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) | ||
Theorem | xpima1 6133 | Direct image by a Cartesian product (case of empty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) | ||
Theorem | xpima2 6134 | Direct image by a Cartesian product (case of nonempty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) | ||
Theorem | xpimasn 6135 | 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 6136 | 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 6137 | 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 6138* | 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 6139 | Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) | ||
Theorem | dfrel4v 6140* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6898 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | dfrel4 6141* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6898 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑦𝑅 ⇒ ⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | cnvcnv 6142 | 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 6143 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
⊢ ◡◡𝐴 = (𝐴 ↾ V) | ||
Theorem | cnvcnvss 6144 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
⊢ ◡◡𝐴 ⊆ 𝐴 | ||
Theorem | cnvrescnv 6145 | Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023.) |
⊢ ◡(◡𝑅 ↾ 𝐵) = (𝑅 ∩ (V × 𝐵)) | ||
Theorem | cnveqb 6146 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) | ||
Theorem | cnveq0 6147 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) | ||
Theorem | dfrel3 6148 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
Theorem | elid 6149* | Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 6148 after elrid 5997. (Contributed by BJ, 28-Aug-2022.) |
⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = 〈𝑥, 𝑥〉) | ||
Theorem | dmresv 6150 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ dom (𝐴 ↾ V) = dom 𝐴 | ||
Theorem | rnresv 6151 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ ran (𝐴 ↾ V) = ran 𝐴 | ||
Theorem | dfrn4 6152 | Range defined in terms of image. (Contributed by NM, 14-May-2008.) |
⊢ ran 𝐴 = (𝐴 “ V) | ||
Theorem | csbrn 6153 | Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | rescnvcnv 6154 | 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 6155 | The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.) |
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) | ||
Theorem | imacnvcnv 6156 | The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) | ||
Theorem | dmsnn0 6157 | 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 6158 | 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 6159 | The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.) |
⊢ dom {∅} = ∅ | ||
Theorem | cnvsn0 6160 | The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ◡{∅} = ∅ | ||
Theorem | dmsn0el 6161 | 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 6162 | 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 6163 | 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 6164 | 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 6165 | The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) | ||
Theorem | dmsnop 6166 | 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 6167 | The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} | ||
Theorem | dmtpop 6168 | The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} | ||
Theorem | cnvcnvsn 6169 | Double converse of a singleton of an ordered pair. (Unlike cnvsn 6176, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} | ||
Theorem | dmsnsnsn 6170 | 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 6171 | 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 6172 | The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) | ||
Theorem | cnvsng 6173 | Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) | ||
Theorem | rnsnop 6174 | 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 6175 | Extract the first member of an ordered pair. (See op2nda 6178 to extract the second member, op1stb 5426 for an alternate version, and op1st 7921 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 | ||
Theorem | cnvsn 6176 | 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 6177 | Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5426 to extract the first member, op2nda 6178 for an alternate version, and op2nd 7922 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | op2nda 6178 | Extract the second member of an ordered pair. (See op1sta 6175 to extract the first member, op2ndb 6177 for an alternate version, and op2nd 7922 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ ran {〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | opswap 6179 | Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 | ||
Theorem | cnvresima 6180 | An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) | ||
Theorem | resdm2 6181 | A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 | ||
Theorem | resdmres 6182 | Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | resresdm 6183 | A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.) |
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹)) | ||
Theorem | imadmres 6184 | The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) | ||
Theorem | resdmss 6185 | Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024.) |
⊢ dom (𝐴 ↾ 𝐵) ⊆ 𝐵 | ||
Theorem | resdifdi 6186 | Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.) |
⊢ (𝐴 ↾ (𝐵 ∖ 𝐶)) = ((𝐴 ↾ 𝐵) ∖ (𝐴 ↾ 𝐶)) | ||
Theorem | resdifdir 6187 | Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.) |
⊢ ((𝐴 ∖ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∖ (𝐵 ↾ 𝐶)) | ||
Theorem | mptpreima 6188* | The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} | ||
Theorem | mptiniseg 6189* | Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) | ||
Theorem | dmmpt 6190 | 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 6191* | The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | dmmptg 6192* | 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 6193* | 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 6194* | 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 6195* | Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.) |
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) | ||
Theorem | dfco2a 6196* | Generalization of dfco2 6195, 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 6197 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) | ||
Theorem | coundir 6198 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) | ||
Theorem | cores 6199 | Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) | ||
Theorem | resco 6200 | Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |