Home | Metamath
Proof Explorer Theorem List (p. 77 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | findes 7601 | Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction step. Theorem Schema 22 of [Suppes] p. 136. See tfindes 7566 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.) |
⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ ω → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
Theorem | dmexg 7602 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.) |
⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) | ||
Theorem | rnexg 7603 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) |
⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V) | ||
Theorem | dmexd 7604 | The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ V) | ||
Theorem | dmex 7605 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.) |
⊢ 𝐴 ∈ V ⇒ ⊢ dom 𝐴 ∈ V | ||
Theorem | rnex 7606 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ran 𝐴 ∈ V | ||
Theorem | iprc 7607 | The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn 21793. (Contributed by NM, 1-Jan-2007.) |
⊢ ¬ I ∈ V | ||
Theorem | resiexg 7608 | The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6969). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) | ||
Theorem | imaexg 7609 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | imaex 7610 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 “ 𝐵) ∈ V | ||
Theorem | exse2 7611 | Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | xpexr 7612 | If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐴 × 𝐵) ∈ 𝐶 → (𝐴 ∈ V ∨ 𝐵 ∈ V)) | ||
Theorem | xpexr2 7613 | If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.) |
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | xpexcnv 7614 | A condition where the converse of xpex 7465 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V) | ||
Theorem | soex 7615 | 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 7616 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7617, elxp6 7712, and elxp7 7713. (Contributed by NM, 17-Feb-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | elxp5 7617 | Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7616 when the double intersection does not create class existence problems (caused by int0 4881). (Contributed by NM, 1-Aug-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | cnvexg 7618 | 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 7619 | 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 7620 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V)) | ||
Theorem | f1oexrnex 7621 | 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 7622* | 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 7623 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | coex 7624 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∘ 𝐵) ∈ V | ||
Theorem | funcnvuni 7625* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6416 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) | ||
Theorem | fun11uni 7626* | 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 7627 | A function with bounded domain and range is a set. This version of fex 6980 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | ||
Theorem | fabexg 7628* | Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
Theorem | fabex 7629* | Existence of a set of functions. (Contributed by NM, 3-Dec-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | dmfex 7630 | 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 7631* | 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 | fiunlem 7632* | Lemma for fiun 7633 and f1iun 7634. Formerly part of f1iun 7634. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | ||
Theorem | fiun 7633* | The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7634. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) | ||
Theorem | f1iun 7634* | 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.) (Proof shortened by AV, 5-Nov-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆) | ||
Theorem | fviunfun 7635* | The function value of an indexed union is the value of one of the indexed functions. (Contributed by AV, 4-Nov-2023.) |
⊢ 𝑈 = ∪ 𝑖 ∈ 𝐼 (𝐹‘𝑖) ⇒ ⊢ ((Fun 𝑈 ∧ 𝐽 ∈ 𝐼 ∧ 𝑋 ∈ dom (𝐹‘𝐽)) → (𝑈‘𝑋) = ((𝐹‘𝐽)‘𝑋)) | ||
Theorem | ffoss 7636* | Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | f11o 7637* | 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 7638 | Alternate proof of resfunexg 6969, shorter but requiring ax-pow 5257 and ax-un 7450. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | cofunexg 7639 | Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | cofunex2g 7640 | Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | fnexALT 7641 | Alternate proof of fnex 6971, derived using the Axiom of Replacement in the form of funimaexg 6433. This version uses ax-pow 5257 and ax-un 7450, whereas fnex 6971 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | funexw 7642 | Weak version of funex 6973 that holds without ax-rep 5181. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | mptexw 7643* | Weak version of mptex 6977 that holds without ax-rep 5181. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | funrnex 7644 | 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 6973. (Contributed by NM, 11-Nov-1995.) |
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) | ||
Theorem | zfrep6 7645* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5194 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 5181. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Theorem | fornex 7646 | If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.) |
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | ||
Theorem | f1dmex 7647 | 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 5181. (Contributed by NM, 4-Sep-2004.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | f1ovv 7648 | 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 7649* | Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.) |
⊢ 𝐹 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V | ||
Theorem | fvresex 7650* | 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 | abrexexg 7651* | Existence of a class abstraction of existentially restricted sets. The class 𝐵 can be thought of as an expression in 𝑥 (which is typically a free variable in the class expression substituted for 𝐵) and the class abstraction appearing in the statement as the class of values 𝐵 as 𝑥 varies through 𝐴. If the "domain" 𝐴 is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg 6975, funex 6973, fnex 6971, resfunexg 6969, and funimaexg 6433. See also abrexex2g 7654. There are partial converses under additional conditions, see for instance abnexg 7467. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | abrexex 7652* | Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7651. See also abrexex2 7659. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V | ||
Theorem | iunexg 7653* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | abrexex2g 7654* | Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) | ||
Theorem | opabex3d 7655* | Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) | ||
Theorem | opabex3rd 7656* | Existence of an ordered pair abstraction if the second components are elements of a set. (Contributed by AV, 17-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ∈ V) | ||
Theorem | opabex3 7657* | Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | iunex 7658* | 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 7659* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7652. (Contributed by NM, 12-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | abexssex 7660* | 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 7661* | 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 7662* | Alternate proof of f1owe 7095, more direct since not using the isomorphism predicate, but requiring ax-un 7450. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | wemoiso 7663* | Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 9527. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | wemoiso2 7664* | 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 7665* | Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓) & ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | oprabex 7666* | Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabex3 7667* | Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabrexex2 7668* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | ab2rexex 7669* | 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 7652. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V | ||
Theorem | ab2rexex2 7670* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7659. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V | ||
Theorem | xpexgALT 7671 | Alternate proof of xpexg 7462 requiring Replacement (ax-rep 5181) but not Power Set (ax-pow 5257). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | offval3 7672* | General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | offres 7673 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷))) | ||
Theorem | ofmres 7674* | Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 7675, allowing it to be used as a function or structure argument. By ofmresval 7411, 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 7675 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) | ||
Syntax | c1st 7676 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7677 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7678 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7686 proves that it does this. For example, (1st ‘〈3, 4〉) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6075 and op1stb 5354). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | ||
Definition | df-2nd 7679 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7687 proves that it does this. For example, (2nd ‘〈3, 4〉) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6078 and op2ndb 6077). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | ||
Theorem | 1stval 7680 | 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 7681 | 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 7682 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅) | ||
Theorem | 2ndnpr 7683 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅) | ||
Theorem | 1st0 7684 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (1st ‘∅) = ∅ | ||
Theorem | 2nd0 7685 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (2nd ‘∅) = ∅ | ||
Theorem | op1st 7686 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (1st ‘〈𝐴, 𝐵〉) = 𝐴 | ||
Theorem | op2nd 7687 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (2nd ‘〈𝐴, 𝐵〉) = 𝐵 | ||
Theorem | op1std 7688 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) | ||
Theorem | op2ndd 7689 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) | ||
Theorem | op1stg 7690 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) | ||
Theorem | op2ndg 7691 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) | ||
Theorem | ot1stg 7692 | 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 7692, ot2ndg 7693, ot3rdg 7694.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) | ||
Theorem | ot2ndg 7693 | Extract the second member of an ordered triple. (See ot1stg 7692 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) | ||
Theorem | ot3rdg 7694 | Extract the third member of an ordered triple. (See ot1stg 7692 comment.) (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐶 ∈ 𝑉 → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) | ||
Theorem | 1stval2 7695 | 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 7696 | 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 7697 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (𝑇 = 〈𝐴, 𝐵, 𝐶〉 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
Theorem | fo1st 7698 | 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 7699 | 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 7700 | 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 𝐶 ↔ 𝐶 = 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |