| Metamath
Proof Explorer Theorem List (p. 81 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-30927) |
(30928-32450) |
(32451-49315) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ab2rexex2 8001* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7990. (Contributed by NM, 20-Sep-2011.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V | ||
| Theorem | xpexgALT 8002 | Alternate proof of xpexg 7766 requiring Replacement (ax-rep 5277) but not Power Set (ax-pow 5363). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
| Theorem | offval3 8003* | General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
| Theorem | offres 8004 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷))) | ||
| Theorem | ofmres 8005* | Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 8006, allowing it to be used as a function or structure argument. By ofmresval 7710, the restricted operation map values are the same as the original values, allowing theorems for ∘f 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.) |
| ⊢ ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘f 𝑅𝑔)) | ||
| Theorem | ofmresex 8006 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) | ||
| Theorem | mptcnfimad 8007* | The converse of a mapping of subsets to their image of a bijection. (Contributed by AV, 23-Apr-2025.) |
| ⊢ 𝑀 = (𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉) & ⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 𝑊) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) ⇒ ⊢ (𝜑 → ◡𝑀 = (𝑦 ∈ ran 𝑀 ↦ (◡𝐹 “ 𝑦))) | ||
| Syntax | c1st 8008 | Extend the definition of a class to include the first member an ordered pair function. |
| class 1st | ||
| Syntax | c2nd 8009 | Extend the definition of a class to include the second member an ordered pair function. |
| class 2nd | ||
| Definition | df-1st 8010 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 8018 proves that it does this. For example, (1st ‘〈3, 4〉) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6243 and op1stb 5474). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
| ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | ||
| Definition | df-2nd 8011 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 8019 proves that it does this. For example, (2nd ‘〈3, 4〉) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6246 and op2ndb 6245). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
| ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | ||
| Theorem | 1stval 8012 | The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
| ⊢ (1st ‘𝐴) = ∪ dom {𝐴} | ||
| Theorem | 2ndval 8013 | The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
| ⊢ (2nd ‘𝐴) = ∪ ran {𝐴} | ||
| Theorem | 1stnpr 8014 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅) | ||
| Theorem | 2ndnpr 8015 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅) | ||
| Theorem | 1st0 8016 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
| ⊢ (1st ‘∅) = ∅ | ||
| Theorem | 2nd0 8017 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
| ⊢ (2nd ‘∅) = ∅ | ||
| Theorem | op1st 8018 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 | ||
| Theorem | op2nd 8019 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 | ||
| Theorem | op1std 8020 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) | ||
| Theorem | op2ndd 8021 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) | ||
| Theorem | op1stg 8022 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) | ||
| Theorem | op2ndg 8023 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) | ||
| Theorem | ot1stg 8024 | 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 8024, ot2ndg 8025, ot3rdg 8026.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) | ||
| Theorem | ot2ndg 8025 | Extract the second member of an ordered triple. (See ot1stg 8024 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) | ||
| Theorem | ot3rdg 8026 | Extract the third member of an ordered triple. (See ot1stg 8024 comment.) (Contributed by NM, 3-Apr-2015.) |
| ⊢ (𝐶 ∈ 𝑉 → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) | ||
| Theorem | 1stval2 8027 | 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 8028 | 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 8029 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
| ⊢ (𝑇 = 〈𝐴, 𝐵, 𝐶〉 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
| Theorem | fo1st 8030 | 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 8031 | 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 8032 | 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 8033 | 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 8034 | 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 8035 | 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 8036 | 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 8037 | 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 8038* | 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 8039* | 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 8040 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
| ⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵) | ||
| Theorem | 2ndcof 8041 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
| ⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶) | ||
| Theorem | xp1st 8042 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) | ||
| Theorem | xp2nd 8043 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) | ||
| Theorem | elxp6 8044 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7940. (Contributed by NM, 9-Oct-2004.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
| Theorem | elxp7 8045 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7940. (Contributed by NM, 19-Aug-2006.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
| Theorem | eqopi 8046 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
| ⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = 〈𝐵, 𝐶〉) | ||
| Theorem | xp2 8047* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
| ⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)} | ||
| Theorem | unielxp 8048 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶)) | ||
| Theorem | 1st2nd2 8049 | 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 8050 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
| ⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
| Theorem | xpopth 8051 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
| ⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) | ||
| Theorem | eqop 8052 | 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 8053 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
| ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶))) | ||
| Theorem | op1steq 8054* | 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 8055* | 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 8056* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
| ⊢ (𝐴 ∈ ((𝐵 × 𝐶) × 𝐷) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝐴 = 〈𝑥, 𝑦, 𝑧〉) | ||
| Theorem | el2xptp0 8057 | 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 | el2xpss 8058* | Version of elrel 5806 for triple Cartesian products. (Contributed by Scott Fenton, 1-Feb-2025.) |
| ⊢ ((𝐴 ∈ 𝑅 ∧ 𝑅 ⊆ ((𝐵 × 𝐶) × 𝐷)) → ∃𝑥∃𝑦∃𝑧 𝐴 = 〈𝑥, 𝑦, 𝑧〉) | ||
| Theorem | 2nd1st 8059 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ◡{𝐴} = 〈(2nd ‘𝐴), (1st ‘𝐴)〉) | ||
| Theorem | 1st2nd 8060 | 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 8061 | 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 8062 | 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 8063 | 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 8064* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
| ⊢ (Rel 𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) | ||
| Theorem | reldm 8065* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
| ⊢ (Rel 𝐴 → dom 𝐴 = ran (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))) | ||
| Theorem | releldmdifi 8066* | 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 8067 | 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 8068 | 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 8069* | 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 8070 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3798 that avoids the existential quantifiers of copsexg 5494). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 = 〈𝑥, 𝑦〉 → ([(1st ‘𝐴) / 𝑥][(2nd ‘𝐴) / 𝑦]𝜑 ↔ 𝜑)) | ||
| Theorem | csbopeq1a 8071 | Equality theorem for substitution of a class 𝐴 for an ordered pair 〈𝑥, 𝑦〉 in 𝐵 (analogue of csbeq1a 3912). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 = 〈𝑥, 𝑦〉 → ⦋(1st ‘𝐴) / 𝑥⦌⦋(2nd ‘𝐴) / 𝑦⦌𝐵 = 𝐵) | ||
| Theorem | sbcoteq1a 8072 | Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024.) |
| ⊢ (𝐴 = 〈𝑥, 𝑦, 𝑧〉 → ([(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ 𝜑)) | ||
| Theorem | dfopab2 8073* | 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 8074* | 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 8075* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
| ⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
| Theorem | dfoprab4 8076* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} | ||
| Theorem | dfoprab4f 8077* | 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 8078* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ∈ V) | ||
| Theorem | opabn1stprc 8079* | 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 8080* | 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 8081* | 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 8082* | Define the Cartesian product of three classes. Compare df-xp 5689. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
| ⊢ ((𝐴 × 𝐵) × 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)} | ||
| Theorem | elopabi 8083* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
| ⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝜒) | ||
| Theorem | eloprabi 8084* | 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 8085* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
| Theorem | mpompts 8086* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
| ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
| Theorem | dmmpossx 8087* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) | ||
| Theorem | fmpox 8088* | 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 8089* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) | ||
| Theorem | fnmpo 8090* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵)) | ||
| Theorem | fnmpoi 8091* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ 𝐹 Fn (𝐴 × 𝐵) | ||
| Theorem | dmmpo 8092* | Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ dom 𝐹 = (𝐴 × 𝐵) | ||
| Theorem | ovmpoelrn 8093* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
| ⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀) | ||
| Theorem | dmmpoga 8094* | Domain of an operation given by the maps-to notation, closed form of dmmpo 8092. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵)) | ||
| Theorem | dmmpog 8095* | Domain of an operation given by the maps-to notation, closed form of dmmpo 8092. 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 8096* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
| Theorem | mpoexg 8097* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
| Theorem | mpoexga 8098* | 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 8099* | Weak version of mpoex 8100 that holds without ax-rep 5277. 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 8100* | 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 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |