![]() |
Metamath
Proof Explorer Theorem List (p. 80 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmfexALT 7901 | Alternate proof of dmfex 7898: shorter but using ax-rep 5286. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 23-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V) | ||
Theorem | dmex 7902 | 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 7903 | 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 7904 | 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 22761. (Contributed by NM, 1-Jan-2007.) |
⊢ ¬ I ∈ V | ||
Theorem | resiexg 7905 | The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7217). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) | ||
Theorem | imaexg 7906 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | imaex 7907 | 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 7908 | Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | xpexr 7909 | 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 7910 | If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.) |
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | xpexcnv 7911 | A condition where the converse of xpex 7740 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V) | ||
Theorem | soex 7912 | 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 7913 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7914, elxp6 8009, and elxp7 8010. (Contributed by NM, 17-Feb-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | elxp5 7914 | Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7913 when the double intersection does not create class existence problems (caused by int0 4967). (Contributed by NM, 1-Aug-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | cnvexg 7915 | 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 7916 | 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 7917 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V)) | ||
Theorem | f1oexrnex 7918 | 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 7919* | 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 7920 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | coex 7921 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∘ 𝐵) ∈ V | ||
Theorem | funcnvuni 7922* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6618 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) | ||
Theorem | fun11uni 7923* | 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 7924 | A function with bounded domain and codomain is a set. This version of fex 7228 is proven without the Axiom of Replacement ax-rep 5286, but depends on ax-un 7725, which is not required for the proof of fex 7228. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | ||
Theorem | fabexg 7925* | Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
Theorem | fabex 7926* | Existence of a set of functions. (Contributed by NM, 3-Dec-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | f1oabexg 7927* | 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 7928* | Lemma for fiun 7929 and f1iun 7930. Formerly part of f1iun 7930. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | ||
Theorem | fiun 7929* | The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7930. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) | ||
Theorem | f1iun 7930* | 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 7931* | 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 7932* | Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | f11o 7933* | 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 7934 | Alternate proof of resfunexg 7217, shorter but requiring ax-pow 5364 and ax-un 7725. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | cofunexg 7935 | Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | cofunex2g 7936 | Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | fnexALT 7937 | Alternate proof of fnex 7219, derived using the Axiom of Replacement in the form of funimaexg 6635. This version uses ax-pow 5364 and ax-un 7725, whereas fnex 7219 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | funexw 7938 | Weak version of funex 7221 that holds without ax-rep 5286. 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 7939* | Weak version of mptex 7225 that holds without ax-rep 5286. 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 7940 | 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 7221. (Contributed by NM, 11-Nov-1995.) |
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) | ||
Theorem | zfrep6 7941* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5300 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 5286. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Theorem | focdmex 7942 | If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.) |
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | ||
Theorem | f1dmex 7943 | 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 5286. (Contributed by NM, 4-Sep-2004.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | f1ovv 7944 | The codomain/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 7945* | Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.) |
⊢ 𝐹 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V | ||
Theorem | fvresex 7946* | 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 7947* | 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 axrep6g 5294, axrep6 5293, ax-rep 5286. See also abrexex2g 7951. There are partial converses under additional conditions, see for instance abnexg 7743. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2138, ax-11 2155, ax-12 2172, ax-pr 5428, ax-un 7725 and shorten proof. (Revised by SN, 11-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | abrexexgOLD 7948* |
Obsolete version of abrexexg 7947 as of 11-Dec-2024. EDITORIAL: Comment
kept since the line of equivalences to ax-rep 5286 is different.
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 7223, funex 7221, fnex 7219, resfunexg 7217, and funimaexg 6635. See also abrexex2g 7951. There are partial converses under additional conditions, see for instance abnexg 7743. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | abrexex 7949* | Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7947. See also abrexex2 7956. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V | ||
Theorem | iunexg 7950* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | abrexex2g 7951* | Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) | ||
Theorem | opabex3d 7952* | Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 9-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) | ||
Theorem | opabex3rd 7953* | Existence of an ordered pair abstraction if the second components are elements of a set. (Contributed by AV, 17-Sep-2023.) (Revised by AV, 9-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑥 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} ∈ V) | ||
Theorem | opabex3 7954* | Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | iunex 7955* | 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 7956* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7949. (Contributed by NM, 12-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | abexssex 7957* | 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 7958* | 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 7959* | Alternate proof of f1owe 7350, more direct since not using the isomorphism predicate, but requiring ax-un 7725. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | wemoiso 7960* | Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 10108. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | wemoiso2 7961* | 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 7962* | Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by AV, 9-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓) & ⊢ (𝜑 → 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | oprabex 7963* | Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑) & ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabex3 7964* | Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.) |
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | oprabrexex2 7965* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V ⇒ ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V | ||
Theorem | ab2rexex 7966* | 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 7949. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V | ||
Theorem | ab2rexex2 7967* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7956. (Contributed by NM, 20-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V | ||
Theorem | xpexgALT 7968 | Alternate proof of xpexg 7737 requiring Replacement (ax-rep 5286) but not Power Set (ax-pow 5364). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | offval3 7969* | General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | offres 7970 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷))) | ||
Theorem | ofmres 7971* | Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 7972, allowing it to be used as a function or structure argument. By ofmresval 7686, 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 7972 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) | ||
Syntax | c1st 7973 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7974 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7975 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7983 proves that it does this. For example, (1st ‘⟨3, 4⟩) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6225 and op1stb 5472). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | ||
Definition | df-2nd 7976 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7984 proves that it does this. For example, (2nd ‘⟨3, 4⟩) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6228 and op2ndb 6227). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | ||
Theorem | 1stval 7977 | 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 7978 | 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 7979 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅) | ||
Theorem | 2ndnpr 7980 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅) | ||
Theorem | 1st0 7981 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (1st ‘∅) = ∅ | ||
Theorem | 2nd0 7982 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
⊢ (2nd ‘∅) = ∅ | ||
Theorem | op1st 7983 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴 | ||
Theorem | op2nd 7984 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵 | ||
Theorem | op1std 7985 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴) | ||
Theorem | op2ndd 7986 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵) | ||
Theorem | op1stg 7987 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴) | ||
Theorem | op2ndg 7988 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵) | ||
Theorem | ot1stg 7989 | 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 7989, ot2ndg 7990, ot3rdg 7991.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴) | ||
Theorem | ot2ndg 7990 | Extract the second member of an ordered triple. (See ot1stg 7989 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵) | ||
Theorem | ot3rdg 7991 | Extract the third member of an ordered triple. (See ot1stg 7989 comment.) (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐶 ∈ 𝑉 → (2nd ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶) | ||
Theorem | 1stval2 7992 | 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 7993 | 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 7994 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (𝑇 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶))) | ||
Theorem | fo1st 7995 | 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 7996 | 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 7997 | 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 7998 | 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 7999 | 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 8000 | 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 ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |