Home | Metamath
Proof Explorer Theorem List (p. 71 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xpexcnv 7001 | A condition where the converse of xpex 6860 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V) | ||
Theorem | soex 7002 | If the relation in a strict order is a set, then the base field is also a set. (Contributed by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → 𝐴 ∈ V) | ||
Theorem | elxp4 7003 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7004, elxp6 7091, and elxp7 7092. (Contributed by NM, 17-Feb-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | elxp5 7004 | Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7003 when the double intersection does not create class existence problems (caused by int0 4425). (Contributed by NM, 1-Aug-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | cnvexg 7005 | The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.) |
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V) | ||
Theorem | cnvex 7006 | The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ◡𝐴 ∈ V | ||
Theorem | relcnvexb 7007 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V)) | ||
Theorem | f1oexrnex 7008 | If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐹 ∈ V) | ||
Theorem | f1oexbi 7009* | There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018.) |
⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ↔ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴) | ||
Theorem | coexg 7010 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | coex 7011 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∘ 𝐵) ∈ V | ||
Theorem | funcnvuni 7012* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5872 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) | ||
Theorem | fun11uni 7013* | The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 ((Fun 𝑓 ∧ Fun ◡𝑓) ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ∪ 𝐴 ∧ Fun ◡∪ 𝐴)) | ||
Theorem | fex2 7014 | A function with bounded domain and range is a set. This version of fex 6394 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | ||
Theorem | fabexg 7015* | Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
Theorem | fabex 7016* | Existence of a set of functions. (Contributed by NM, 3-Dec-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | dmfex 7017 | If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V) | ||
Theorem | f1oabexg 7018* | The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
Theorem | fun11iun 7019* | The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆) | ||
Theorem | ffoss 7020* | Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | f11o 7021* | Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ ∃𝑥(𝐹:𝐴–1-1-onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | resfunexgALT 7022 | Alternate proof of resfunexg 6384, shorter but requiring ax-pow 4769 and ax-un 6847. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | cofunexg 7023 | Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | cofunex2g 7024 | Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | fnexALT 7025 | Alternate proof of fnex 6386, derived using the Axiom of Replacement in the form of funimaexg 5889. This version uses ax-pow 4769 and ax-un 6847, whereas fnex 6386 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | funrnex 7026 | If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 6387. (Contributed by NM, 11-Nov-1995.) |
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) | ||
Theorem | zfrep6 7027* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4709 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 4699. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Theorem | fornex 7028 | If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.) |
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | ||
Theorem | f1dmex 7029 | If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep 4699. (Contributed by NM, 4-Sep-2004.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | f1ovv 7030 | The range of a 1-1 onto function is a set iff its domain is a set. (Contributed by AV, 21-Mar-2019.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | ||
Theorem | fvclex 7031* | Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.) |
⊢ 𝐹 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V | ||
Theorem | fvresex 7032* | Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)} ∈ V | ||
Theorem | abrexex 7033* | Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be thought of as 𝐵(𝑥). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 6389, funex 6387, fnex 6386, resfunexg 6384, and funimaexg 5889. See also abrexex2 7040. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V | ||
Theorem | abrexexg 7034* | Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in 𝐵. The antecedent assures us that 𝐴 is a set. (Contributed by NM, 3-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | iunexg 7035* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | abrexex2g 7036* | Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) | ||
Theorem | opabex3d 7037* | Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) | ||
Theorem | opabex3 7038* | Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | iunex 7039* | 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 7040* | Existence of an existentially restricted class abstraction. 𝜑 is normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7033. (Contributed by NM, 12-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | abexssex 7041* | 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 7042* | A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V | ||
Theorem | f1oweALT 7043* | Alternate proof of f1owe 6503, more direct since not using the isomorphism predicate, but requiring ax-un 6847. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | wemoiso 7044* | Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 8819. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | wemoiso2 7045* | 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 7046* | Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓) & ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | oprabex 7047* | Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabex3 7048* | Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabrexex2 7049* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | ab2rexex 7050* | 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 7033. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V | ||
Theorem | ab2rexex2 7051* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7040. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V | ||
Theorem | xpexgALT 7052 | Alternate proof of xpexg 6858 requiring Replacement (ax-rep 4699) but not Power Set (ax-pow 4769). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | offval3 7053* | General value of (𝐹 ∘𝑓 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | offres 7054 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷))) | ||
Theorem | ofmres 7055* | Equivalent expressions for a restriction of the function operation map. Unlike ∘𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ∣ ‘(𝐴 × 𝐵)) can be a set by ofmresex 7056, allowing it to be used as a function or structure argument. By ofmresval 6808, the restricted operation map values are the same as the original values, allowing theorems for ∘𝑓 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.) |
⊢ ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘𝑓 𝑅𝑔)) | ||
Theorem | ofmresex 7056 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) | ||
Syntax | c1st 7057 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7058 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7059 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7067 proves that it does this. For example, (1st ‘〈3, 4〉) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5535 and op1stb 4867). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | ||
Definition | df-2nd 7060 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7068 proves that it does this. For example, (2nd ‘〈3, 4〉) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5538 and op2ndb 5537). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | ||
Theorem | 1stval 7061 | 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 7062 | 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 7063 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅) | ||
Theorem | 2ndnpr 7064 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅) | ||
Theorem | 1st0 7065 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (1st ‘∅) = ∅ | ||
Theorem | 2nd0 7066 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (2nd ‘∅) = ∅ | ||
Theorem | op1st 7067 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 | ||
Theorem | op2nd 7068 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 | ||
Theorem | op1std 7069 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) | ||
Theorem | op2ndd 7070 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) | ||
Theorem | op1stg 7071 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) | ||
Theorem | op2ndg 7072 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) | ||
Theorem | ot1stg 7073 | 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 7073, ot2ndg 7074, ot3rdg 7075.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) | ||
Theorem | ot2ndg 7074 | Extract the second member of an ordered triple. (See ot1stg 7073 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) | ||
Theorem | ot3rdg 7075 | Extract the third member of an ordered triple. (See ot1stg 7073 comment.) (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐶 ∈ 𝑉 → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) | ||
Theorem | 1stval2 7076 | 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 7077 | 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 7078 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (𝑇 = 〈𝐴, 𝐵, 𝐶〉 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
Theorem | fo1st 7079 | 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 7080 | 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 | f1stres 7081 | 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 7082 | 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 7083 | 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 7084 | 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 7085* | 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 7086* | 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 7087 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵) | ||
Theorem | 2ndcof 7088 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶) | ||
Theorem | xp1st 7089 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) | ||
Theorem | xp2nd 7090 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) | ||
Theorem | elxp6 7091 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7003. (Contributed by NM, 9-Oct-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | elxp7 7092 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7003. (Contributed by NM, 19-Aug-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | ||
Theorem | eqopi 7093 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = 〈𝐵, 𝐶〉) | ||
Theorem | xp2 7094* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)} | ||
Theorem | unielxp 7095 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶)) | ||
Theorem | 1st2nd2 7096 | 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 7097 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | ||
Theorem | xpopth 7098 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | eqop 7099 | 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 7100 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |