Home | Metamath
Proof Explorer Theorem List (p. 78 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | op1stg 7701 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) | ||
Theorem | op2ndg 7702 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) | ||
Theorem | ot1stg 7703 | Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 7703, ot2ndg 7704, ot3rdg 7705.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) | ||
Theorem | ot2ndg 7704 | Extract the second member of an ordered triple. (See ot1stg 7703 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) | ||
Theorem | ot3rdg 7705 | Extract the third member of an ordered triple. (See ot1stg 7703 comment.) (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐶 ∈ 𝑉 → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) | ||
Theorem | 1stval2 7706 | Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.) |
⊢ (𝐴 ∈ (V × V) → (1st ‘𝐴) = ∩ ∩ 𝐴) | ||
Theorem | 2ndval2 7707 | Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.) |
⊢ (𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∩ ∩ ∩ ◡{𝐴}) | ||
Theorem | oteqimp 7708 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (𝑇 = 〈𝐴, 𝐵, 𝐶〉 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
Theorem | fo1st 7709 | The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ 1st :V–onto→V | ||
Theorem | fo2nd 7710 | The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ 2nd :V–onto→V | ||
Theorem | br1steqg 7711 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉1st 𝐶 ↔ 𝐶 = 𝐴)) | ||
Theorem | br2ndeqg 7712 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉2nd 𝐶 ↔ 𝐶 = 𝐵)) | ||
Theorem | f1stres 7713 | Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 | ||
Theorem | f2ndres 7714 | Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵 | ||
Theorem | fo1stres 7715 | Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐵 ≠ ∅ → (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴) | ||
Theorem | fo2ndres 7716 | Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ≠ ∅ → (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐵) | ||
Theorem | 1st2val 7717* | Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴) | ||
Theorem | 2nd2val 7718* | Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴) | ||
Theorem | 1stcof 7719 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵) | ||
Theorem | 2ndcof 7720 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶) | ||
Theorem | xp1st 7721 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) | ||
Theorem | xp2nd 7722 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) | ||
Theorem | elxp6 7723 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7627. (Contributed by NM, 9-Oct-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | elxp7 7724 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7627. (Contributed by NM, 19-Aug-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | eqopi 7725 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = 〈𝐵, 𝐶〉) | ||
Theorem | xp2 7726* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)} | ||
Theorem | unielxp 7727 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶)) | ||
Theorem | 1st2nd2 7728 | Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
Theorem | 1st2ndb 7729 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
Theorem | xpopth 7730 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | eqop 7731 | Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 = 〈𝐵, 𝐶〉 ↔ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶))) | ||
Theorem | eqop2 7732 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶))) | ||
Theorem | op1steq 7733* | Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝐴 ∈ (𝑉 × 𝑊) → ((1st ‘𝐴) = 𝐵 ↔ ∃𝑥 𝐴 = 〈𝐵, 𝑥〉)) | ||
Theorem | opreuopreu 7734* | There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝜓 ↔ 𝜑)) ⇒ ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓)) | ||
Theorem | el2xptp 7735* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (𝐴 ∈ ((𝐵 × 𝐶) × 𝐷) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝐴 = 〈𝑥, 𝑦, 𝑧〉) | ||
Theorem | el2xptp0 7736 | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st ‘(1st ‘𝐴)) = 𝑋 ∧ (2nd ‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) ↔ 𝐴 = 〈𝑋, 𝑌, 𝑍〉)) | ||
Theorem | 2nd1st 7737 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ◡{𝐴} = 〈(2nd ‘𝐴), (1st ‘𝐴)〉) | ||
Theorem | 1st2nd 7738 | Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.) |
⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
Theorem | 1stdm 7739 | The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (1st ‘𝐴) ∈ dom 𝑅) | ||
Theorem | 2ndrn 7740 | The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (2nd ‘𝐴) ∈ ran 𝑅) | ||
Theorem | 1st2ndbr 7741 | Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.) |
⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴)) | ||
Theorem | releldm2 7742* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
⊢ (Rel 𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) | ||
Theorem | reldm 7743* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
⊢ (Rel 𝐴 → dom 𝐴 = ran (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))) | ||
Theorem | releldmdifi 7744* | One way of expressing membership in the difference of domains of two nested relations. (Contributed by AV, 26-Oct-2023.) |
⊢ ((Rel 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) | ||
Theorem | funfv1st2nd 7745 | The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝐹) → (𝐹‘(1st ‘𝑋)) = (2nd ‘𝑋)) | ||
Theorem | funelss 7746 | If the first component of an element of a function is in the domain of a subset of the function, the element is a member of this subset. (Contributed by AV, 27-Oct-2023.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐴) → ((1st ‘𝑋) ∈ dom 𝐵 → 𝑋 ∈ 𝐵)) | ||
Theorem | funeldmdif 7747* | Two ways of expressing membership in the difference of domains of two nested functions. (Contributed by AV, 27-Oct-2023.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) | ||
Theorem | sbcopeq1a 7748 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3783 that avoids the existential quantifiers of copsexg 5382). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ([(1st ‘𝐴) / 𝑥][(2nd ‘𝐴) / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | csbopeq1a 7749 | Equality theorem for substitution of a class 𝐴 for an ordered pair 〈𝑥, 𝑦〉 in 𝐵 (analogue of csbeq1a 3897). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ⦋(1st ‘𝐴) / 𝑥⦌⦋(2nd ‘𝐴) / 𝑦⦌𝐵 = 𝐵) | ||
Theorem | dfopab2 7750* | A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∈ (V × V) ∣ [(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} | ||
Theorem | dfoprab3s 7751* | A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (V × V) ∧ [(1st ‘𝑤) / 𝑥][(2nd ‘𝑤) / 𝑦]𝜑)} | ||
Theorem | dfoprab3 7752* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | dfoprab4 7753* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} | ||
Theorem | dfoprab4f 7754* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} | ||
Theorem | opabex2 7755* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ∈ V) | ||
Theorem | opabn1stprc 7756* | An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020.) |
⊢ (∃𝑦𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜑} ∉ V) | ||
Theorem | opiota 7757* | The property of a uniquely specified ordered pair. The proof uses properties of the ℩ description binder. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ 𝐼 = (℩𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) & ⊢ 𝑋 = (1st ‘𝐼) & ⊢ 𝑌 = (2nd ‘𝐼) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐷 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃!𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝜒) ↔ (𝐶 = 𝑋 ∧ 𝐷 = 𝑌))) | ||
Theorem | cnvoprab 7758* | The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof shortened by Thierry Arnoux, 20-Feb-2022.) |
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜑)) & ⊢ (𝜓 → 𝑎 ∈ (V × V)) ⇒ ⊢ ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑧, 𝑎〉 ∣ 𝜓} | ||
Theorem | dfxp3 7759* | Define the Cartesian product of three classes. Compare df-xp 5561. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 × 𝐵) × 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)} | ||
Theorem | elopabi 7760* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝜒) | ||
Theorem | eloprabi 7761* | A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = (1st ‘(1st ‘𝐴)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = (2nd ‘(1st ‘𝐴)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = (2nd ‘𝐴) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝐴 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} → 𝜃) | ||
Theorem | mpomptsx 7762* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
Theorem | mpompts 7763* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
Theorem | dmmpossx 7764* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) | ||
Theorem | fmpox 7765* | Functionality, domain and codomain of a class given by the maps-to notation, where 𝐵(𝑥) is not constant but depends on 𝑥. (Contributed by NM, 29-Dec-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) | ||
Theorem | fmpo 7766* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) | ||
Theorem | fnmpo 7767* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵)) | ||
Theorem | fnmpoi 7768* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ 𝐹 Fn (𝐴 × 𝐵) | ||
Theorem | dmmpo 7769* | Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ dom 𝐹 = (𝐴 × 𝐵) | ||
Theorem | ovmpoelrn 7770* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀) | ||
Theorem | dmmpoga 7771* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7769. (Contributed by Alexander van der Vekens, 10-Feb-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵)) | ||
Theorem | dmmpog 7772* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7769. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵)) | ||
Theorem | mpoexxg 7773* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | mpoexg 7774* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | mpoexga 7775* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) | ||
Theorem | mpoexw 7776* | Weak version of mpoex 7777 that holds without ax-rep 5190. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V | ||
Theorem | mpoex 7777* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V | ||
Theorem | mptmpoopabbrd 7778* | The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) & ⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ 𝜓} ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓) & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) & ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏)) & ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)})) ⇒ ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | ||
Theorem | mptmpoopabovd 7779* | The operation value of a function value of a collection of ordered pairs of related elements (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) & ⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ 𝜓} ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓) & ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝑓(𝑎(𝐶‘𝑔)𝑏)ℎ ∧ 𝑓(𝐷‘𝑔)ℎ)})) ⇒ ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝑓(𝑋(𝐶‘𝐺)𝑌)ℎ ∧ 𝑓(𝐷‘𝐺)ℎ)}) | ||
Theorem | el2mpocsbcl 7780* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐶 ∧ 𝑇 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐷)))) | ||
Theorem | el2mpocl 7781* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. Using implicit substitution. (Contributed by AV, 21-May-2021.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸)) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝐶 = 𝐹 ∧ 𝐷 = 𝐺)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺)))) | ||
Theorem | fnmpoovd 7782* | A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) (Revised by AV, 3-Jul-2022.) |
⊢ (𝜑 → 𝑀 Fn (𝐴 × 𝐵)) & ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐵 (𝑖𝑀𝑗) = 𝐷)) | ||
Theorem | offval22 7783* | The function operation expressed as a mapping, variation of offval2 7426. (Contributed by SO, 15-Jul-2018.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷))) | ||
Theorem | brovpreldm 7784 | If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020.) |
⊢ (𝐷(𝐵𝐴𝐶)𝐸 → 〈𝐵, 𝐶〉 ∈ dom 𝐴) | ||
Theorem | bropopvvv 7785* | If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.) |
⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ 𝜑})) & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓)) & ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ 𝜃}) ⇒ ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) | ||
Theorem | bropfvvvvlem 7786* | Lemma for bropfvvvv 7787. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) & ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) ⇒ ⊢ ((〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))) | ||
Theorem | bropfvvvv 7787* | If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) & ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) & ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆) & ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇) & ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) | ||
Theorem | ovmptss 7788* | If all the values of the mapping are subsets of a class 𝑋, then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → (𝐸𝐹𝐺) ⊆ 𝑋) | ||
Theorem | relmpoopab 7789* | Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈𝑧, 𝑤〉 ∣ 𝜑}) ⇒ ⊢ Rel (𝐶𝐹𝐷) | ||
Theorem | fmpoco 7790* | Composition of two functions. Variation of fmptco 6891 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) & ⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | ||
Theorem | oprabco 7791* | Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐷) & ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐻‘𝐶)) ⇒ ⊢ (𝐻 Fn 𝐷 → 𝐺 = (𝐻 ∘ 𝐹)) | ||
Theorem | oprab2co 7792* | Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑅) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈𝐶, 𝐷〉) & ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑀𝐷)) ⇒ ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹)) | ||
Theorem | df1st2 7793* | An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} = (1st ↾ (V × V)) | ||
Theorem | df2nd2 7794* | An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} = (2nd ↾ (V × V)) | ||
Theorem | 1stconst 7795 | The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴) | ||
Theorem | 2ndconst 7796 | The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ∈ 𝑉 → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–1-1-onto→𝐵) | ||
Theorem | dfmpo 7797* | Alternate definition for the maps-to notation df-mpo 7161 (although it requires that 𝐶 be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 𝐶〉} | ||
Theorem | mposn 7798* | An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.) |
⊢ 𝐹 = (𝑥 ∈ {𝐴}, 𝑦 ∈ {𝐵} ↦ 𝐶) & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑦 = 𝐵 → 𝐷 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈) → 𝐹 = {〈〈𝐴, 𝐵〉, 𝐸〉}) | ||
Theorem | curry1 7799* | Composition with ◡(2nd ↾ ({𝐶} × V)) turns any binary operation 𝐹 with a constant first operand into a function 𝐺 of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥))) | ||
Theorem | curry1val 7800 | The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (𝐺‘𝐷) = (𝐶𝐹𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |