| Metamath
Proof Explorer Theorem List (p. 80 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nnlim 7901 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
| ⊢ (𝐴 ∈ ω → ¬ Lim 𝐴) | ||
| Theorem | omssnlim 7902 | The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ ω ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} | ||
| Theorem | limom 7903 | Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Theorem 1.23 of [Schloeder] p. 4. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
| ⊢ Lim ω | ||
| Theorem | peano2b 7904 | A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.) |
| ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | ||
| Theorem | nnsuc 7905* | A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) | ||
| Theorem | omsucne 7906 | A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.) |
| ⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴) | ||
| Theorem | ssnlim 7907* | An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) |
| ⊢ ((Ord 𝐴 ∧ 𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω) | ||
| Theorem | omsinds 7908* | Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof shortened by BJ, 16-Oct-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) | ||
| Theorem | omun 7909 | The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∪ 𝐵) ∈ ω) | ||
| Theorem | peano1 7910 | Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7910 through peano5 7915 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) Avoid ax-un 7755. (Revised by BTernaryTau, 29-Nov-2024.) |
| ⊢ ∅ ∈ ω | ||
| Theorem | peano1OLD 7911 | Obsolete version of peano1 7910 as of 29-Nov-2024. (Contributed by NM, 15-May-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∅ ∈ ω | ||
| Theorem | peano2 7912 | The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
| ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) | ||
| Theorem | peano3 7913 | The successor of any natural number is not zero. One of Peano's five postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
| ⊢ (𝐴 ∈ ω → suc 𝐴 ≠ ∅) | ||
| Theorem | peano4 7914 | Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's five postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43. (Contributed by NM, 3-Sep-2003.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | peano5 7915* | The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as Theorem findes 7922. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2141, ax-12 2177. (Revised by GG, 3-Oct-2024.) |
| ⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
| Theorem | nn0suc 7916* | A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.) |
| ⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
| Theorem | find 7917* | The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that 𝐴 is a set of natural numbers, zero belongs to 𝐴, and given any member of 𝐴 the member's successor also belongs to 𝐴. The conclusion is that every natural number is in 𝐴. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Wolf Lammen, 28-May-2024.) |
| ⊢ (𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) ⇒ ⊢ 𝐴 = ω | ||
| Theorem | finds 7918* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.) |
| ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ω → 𝜏) | ||
| Theorem | findsg 7919* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number 𝐵 instead of zero. (Contributed by NM, 16-Sep-1995.) |
| ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ ω → 𝜓) & ⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏) | ||
| Theorem | finds2 7920* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.) |
| ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝜏 → 𝜓) & ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃))) ⇒ ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑)) | ||
| Theorem | finds1 7921* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.) |
| ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
| Theorem | findes 7922 | 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 7884 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.) |
| ⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ ω → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
| Theorem | dmexg 7923 | 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 7924 | 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 7925 | The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ V) | ||
| Theorem | fndmexd 7926 | If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
| Theorem | dmfex 7927 | 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 | fndmexb 7928 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| ⊢ (𝐹 Fn 𝐴 → (𝐴 ∈ V ↔ 𝐹 ∈ V)) | ||
| Theorem | fdmexb 7929 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| ⊢ (𝐹:𝐴⟶𝐵 → (𝐴 ∈ V ↔ 𝐹 ∈ V)) | ||
| Theorem | dmfexALT 7930 | Alternate proof of dmfex 7927: shorter but using ax-rep 5279. (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 7931 | 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 7932 | 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 7933 | 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 23265. (Contributed by NM, 1-Jan-2007.) |
| ⊢ ¬ I ∈ V | ||
| Theorem | resiexg 7934 | The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7235). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) | ||
| Theorem | imaexg 7935 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) | ||
| Theorem | imaex 7936 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 “ 𝐵) ∈ V | ||
| Theorem | rnexd 7937 | The range of a set is a set. Deduction version of rnexd 7937. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran 𝐴 ∈ V) | ||
| Theorem | imaexd 7938 | The image of a set is a set. Deduction version of imaexg 7935. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) ∈ V) | ||
| Theorem | exse2 7939 | Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.) |
| ⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
| Theorem | xpexr 7940 | 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 7941 | If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.) |
| ⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
| Theorem | xpexcnv 7942 | A condition where the converse of xpex 7773 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
| ⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V) | ||
| Theorem | soex 7943 | 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 7944 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7945, elxp6 8048, and elxp7 8049. (Contributed by NM, 17-Feb-2004.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
| Theorem | elxp5 7945 | Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7944 when the double intersection does not create class existence problems (caused by int0 4962). (Contributed by NM, 1-Aug-2004.) |
| ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
| Theorem | cnvexg 7946 | 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 7947 | 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 7948 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
| ⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V)) | ||
| Theorem | f1oexrnex 7949 | 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 7950* | 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 7951 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) | ||
| Theorem | coex 7952 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∘ 𝐵) ∈ V | ||
| Theorem | coexd 7953 | The composition of two sets is a set. (Contributed by SN, 7-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ V) | ||
| Theorem | funcnvuni 7954* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6635 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
| ⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) | ||
| Theorem | fun11uni 7955* | 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 | resf1extb 7956 | Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → (((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ (𝐹 ↾ (𝐶 ∪ {𝑋})):(𝐶 ∪ {𝑋})–1-1→𝐵)) | ||
| Theorem | resf1ext2b 7957 | Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → ((Fun ◡(𝐹 ↾ 𝐶) ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ Fun ◡(𝐹 ↾ (𝐶 ∪ {𝑋})))) | ||
| Theorem | fex2 7958 | A function with bounded domain and codomain is a set. This version of fex 7246 is proven without the Axiom of Replacement ax-rep 5279, but depends on ax-un 7755, which is not required for the proof of fex 7246. (Contributed by Mario Carneiro, 24-Jun-2015.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | ||
| Theorem | fabexd 7959* | Existence of a set of functions. In contrast to fabex 7962 or fabexg 7960, the condition in the class abstraction does not contain the function explicitly, but the function can be derived from it. Therefore, this theorem is also applicable for more special functions like one-to-one, onto or one-to-one onto functions. (Contributed by AV, 20-May-2025.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝑓:𝑋⟶𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) ⇒ ⊢ (𝜑 → {𝑓 ∣ 𝜓} ∈ V) | ||
| Theorem | fabexg 7960* | Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.) |
| ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
| Theorem | fabexgOLD 7961* | Obsolete version of fabexg 7960 as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
| Theorem | fabex 7962* | Existence of a set of functions. (Contributed by NM, 3-Dec-2007.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
| Theorem | mapex 7963* | The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) (Proof shortened by AV, 16-Jun-2025.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) | ||
| Theorem | f1oabexg 7964* | The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.) |
| ⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
| Theorem | f1oabexgOLD 7965* | Obsolete version of f1oabexg 7964 as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
| Theorem | fiunlem 7966* | Lemma for fiun 7967 and f1iun 7968. Formerly part of f1iun 7968. (Contributed by AV, 6-Oct-2023.) |
| ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | ||
| Theorem | fiun 7967* | The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7968. (Contributed by AV, 6-Oct-2023.) |
| ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) | ||
| Theorem | f1iun 7968* | 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 7969* | 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 7970* | Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
| Theorem | f11o 7971* | 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 7972 | Alternate proof of resfunexg 7235, shorter but requiring ax-pow 5365 and ax-un 7755. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
| Theorem | cofunexg 7973 | Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.) |
| ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) | ||
| Theorem | cofunex2g 7974 | Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) | ||
| Theorem | fnexALT 7975 | Alternate proof of fnex 7237, derived using the Axiom of Replacement in the form of funimaexg 6653. This version uses ax-pow 5365 and ax-un 7755, whereas fnex 7237 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
| Theorem | funexw 7976 | Weak version of funex 7239 that holds without ax-rep 5279. 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 7977* | Weak version of mptex 7243 that holds without ax-rep 5279. 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 7978 | 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 7239. (Contributed by NM, 11-Nov-1995.) |
| ⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) | ||
| Theorem | zfrep6 7979* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5296 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 5279. (Contributed by NM, 10-Oct-2003.) |
| ⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
| Theorem | focdmex 7980 | If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.) |
| ⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | ||
| Theorem | f1dmex 7981 | 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 5279. (Contributed by NM, 4-Sep-2004.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
| Theorem | f1ovv 7982 | 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 7983* | Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V | ||
| Theorem | fvresex 7984* | 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 7985* | 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 5290, axrep6 5288, ax-rep 5279. See also abrexex2g 7989. There are partial converses under additional conditions, see for instance abnexg 7776. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2141, ax-11 2157, ax-12 2177, ax-pr 5432, ax-un 7755 and shorten proof. (Revised by SN, 11-Dec-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
| Theorem | abrexexgOLD 7986* |
Obsolete version of abrexexg 7985 as of 11-Dec-2024. EDITORIAL: Comment
kept since the line of equivalences to ax-rep 5279 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 7241, funex 7239, fnex 7237, resfunexg 7235, and funimaexg 6653. See also abrexex2g 7989. There are partial converses under additional conditions, see for instance abnexg 7776. (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 7987* | Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7985. See also abrexex2 7994. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V | ||
| Theorem | iunexg 7988* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
| Theorem | abrexex2g 7989* | Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) | ||
| Theorem | opabex3d 7990* | 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 7991* | 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 7992* | Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
| Theorem | iunex 7993* | 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 7994* | Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 7987. (Contributed by NM, 12-Sep-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V | ||
| Theorem | abexssex 7995* | 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 7996* | 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 7997* | Alternate proof of f1owe 7373, more direct since not using the isomorphism predicate, but requiring ax-un 7755. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
| Theorem | wemoiso 7998* | Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 10153. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
| ⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
| Theorem | wemoiso2 7999* | 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 8000* | Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by AV, 9-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓) & ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |