![]() |
Metamath
Proof Explorer Theorem List (p. 80 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunex 7901* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V | ||
Theorem | abrexex2 7902* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7895. (Contributed by NM, 12-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | abexssex 7903* | Existence of a class abstraction with an existentially quantified expression. Both 𝑥 and 𝑦 can be free in 𝜑. (Contributed by NM, 29-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | abexex 7904* | A condition where a class abstraction continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V | ||
Theorem | f1oweALT 7905* | Alternate proof of f1owe 7298, more direct since not using the isomorphism predicate, but requiring ax-un 7672. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | wemoiso 7906* | Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 10049. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | wemoiso2 7907* | Thus, there is at most one isomorphism between any two well-ordered sets. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (𝑆 We 𝐵 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | oprabexd 7908* | Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by AV, 9-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓) & ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | oprabex 7909* | Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabex3 7910* | Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabrexex2 7911* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | ab2rexex 7912* | Existence of a class abstraction of existentially restricted sets. Variables 𝑥 and 𝑦 are normally free-variable parameters in the class expression substituted for 𝐶, which can be thought of as 𝐶(𝑥, 𝑦). See comments for abrexex 7895. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V | ||
Theorem | ab2rexex2 7913* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7902. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V | ||
Theorem | xpexgALT 7914 | Alternate proof of xpexg 7684 requiring Replacement (ax-rep 5242) but not Power Set (ax-pow 5320). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | offval3 7915* | General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | offres 7916 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷))) | ||
Theorem | ofmres 7917* | Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 7918, allowing it to be used as a function or structure argument. By ofmresval 7633, 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 7918 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) | ||
Syntax | c1st 7919 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7920 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7921 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7929 proves that it does this. For example, (1st ‘〈3, 4〉) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6177 and op1stb 5428). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | ||
Definition | df-2nd 7922 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7930 proves that it does this. For example, (2nd ‘〈3, 4〉) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6180 and op2ndb 6179). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | ||
Theorem | 1stval 7923 | 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 7924 | 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 7925 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅) | ||
Theorem | 2ndnpr 7926 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅) | ||
Theorem | 1st0 7927 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (1st ‘∅) = ∅ | ||
Theorem | 2nd0 7928 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (2nd ‘∅) = ∅ | ||
Theorem | op1st 7929 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 | ||
Theorem | op2nd 7930 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 | ||
Theorem | op1std 7931 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) | ||
Theorem | op2ndd 7932 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) | ||
Theorem | op1stg 7933 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) | ||
Theorem | op2ndg 7934 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) | ||
Theorem | ot1stg 7935 | 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 7935, ot2ndg 7936, ot3rdg 7937.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) | ||
Theorem | ot2ndg 7936 | Extract the second member of an ordered triple. (See ot1stg 7935 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) | ||
Theorem | ot3rdg 7937 | Extract the third member of an ordered triple. (See ot1stg 7935 comment.) (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐶 ∈ 𝑉 → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) | ||
Theorem | 1stval2 7938 | 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 7939 | 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 7940 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (𝑇 = 〈𝐴, 𝐵, 𝐶〉 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
Theorem | fo1st 7941 | 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 7942 | 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 7943 | 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 7944 | 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 7945 | 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 7946 | 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 7947 | 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 7948 | 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 7949* | 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 7950* | 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 7951 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵) | ||
Theorem | 2ndcof 7952 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶) | ||
Theorem | xp1st 7953 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) | ||
Theorem | xp2nd 7954 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) | ||
Theorem | elxp6 7955 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7859. (Contributed by NM, 9-Oct-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | elxp7 7956 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7859. (Contributed by NM, 19-Aug-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | eqopi 7957 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = 〈𝐵, 𝐶〉) | ||
Theorem | xp2 7958* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)} | ||
Theorem | unielxp 7959 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶)) | ||
Theorem | 1st2nd2 7960 | 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 7961 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
Theorem | xpopth 7962 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | eqop 7963 | 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 7964 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶))) | ||
Theorem | op1steq 7965* | 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 7966* | 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 7967* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (𝐴 ∈ ((𝐵 × 𝐶) × 𝐷) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝐴 = 〈𝑥, 𝑦, 𝑧〉) | ||
Theorem | el2xptp0 7968 | 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 7969* | Version of elrel 5754 for triple Cartesian products. (Contributed by Scott Fenton, 1-Feb-2025.) |
⊢ ((𝐴 ∈ 𝑅 ∧ 𝑅 ⊆ ((𝐵 × 𝐶) × 𝐷)) → ∃𝑥∃𝑦∃𝑧 𝐴 = 〈𝑥, 𝑦, 𝑧〉) | ||
Theorem | 2nd1st 7970 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ◡{𝐴} = 〈(2nd ‘𝐴), (1st ‘𝐴)〉) | ||
Theorem | 1st2nd 7971 | 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 7972 | 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 7973 | 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 7974 | 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 7975* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
⊢ (Rel 𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) | ||
Theorem | reldm 7976* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
⊢ (Rel 𝐴 → dom 𝐴 = ran (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))) | ||
Theorem | releldmdifi 7977* | 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 7978 | 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 7979 | 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 7980* | 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 7981 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3750 that avoids the existential quantifiers of copsexg 5448). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ([(1st ‘𝐴) / 𝑥][(2nd ‘𝐴) / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | csbopeq1a 7982 | Equality theorem for substitution of a class 𝐴 for an ordered pair 〈𝑥, 𝑦〉 in 𝐵 (analogue of csbeq1a 3869). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ⦋(1st ‘𝐴) / 𝑥⦌⦋(2nd ‘𝐴) / 𝑦⦌𝐵 = 𝐵) | ||
Theorem | sbcoteq1a 7983 | 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 7984* | 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 7985* | 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 7986* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | dfoprab4 7987* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} | ||
Theorem | dfoprab4f 7988* | 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 7989* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ∈ V) | ||
Theorem | opabn1stprc 7990* | 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 7991* | 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 7992* | 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 7993* | Define the Cartesian product of three classes. Compare df-xp 5639. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 × 𝐵) × 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)} | ||
Theorem | elopabi 7994* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} → 𝜒) | ||
Theorem | eloprabi 7995* | 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 7996* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
Theorem | mpompts 7997* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶) | ||
Theorem | dmmpossx 7998* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) | ||
Theorem | fmpox 7999* | 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 8000* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |