![]() |
Metamath
Proof Explorer Theorem List (p. 79 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tfinds3 7801* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝜂 → 𝜓) & ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃))) & ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) ⇒ ⊢ (𝐴 ∈ On → (𝜂 → 𝜏)) | ||
Syntax | com 7802 | Extend class notation to include the class of natural numbers. |
class ω | ||
Definition | df-om 7803* |
Define the class of natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e., all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7804 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 9579, and ω can
then be defined per dfom3 9583 (the smallest inductive set) and dfom4 9585.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 6321. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12154) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.) |
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom2 7804 | An alternate definition of the set of natural numbers ω. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the restricted class abstraction of non-limit ordinal numbers (see nlimon 7787). (Contributed by NM, 1-Nov-2004.) |
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} | ||
Theorem | elom 7805* | Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9584. (Contributed by NM, 15-May-1994.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))) | ||
Theorem | omsson 7806 | Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ On | ||
Theorem | limomss 7807 | The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → ω ⊆ 𝐴) | ||
Theorem | nnon 7808 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | ||
Theorem | nnoni 7809 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ 𝐴 ∈ ω ⇒ ⊢ 𝐴 ∈ On | ||
Theorem | nnord 7810 | A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
⊢ (𝐴 ∈ ω → Ord 𝐴) | ||
Theorem | trom 7811 | The class of finite ordinals ω is a transitive class. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Tr ω | ||
Theorem | ordom 7812 | The class of finite ordinals ω is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ord ω | ||
Theorem | elnn 7813 | A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) | ||
Theorem | omon 7814 | The class of natural numbers ω is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43. (Contributed by NM, 10-May-1998.) |
⊢ (ω ∈ On ∨ ω = On) | ||
Theorem | omelon2 7815 | Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.) |
⊢ (ω ∈ V → ω ∈ On) | ||
Theorem | nnlim 7816 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴) | ||
Theorem | omssnlim 7817 | 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 7818 | 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 7819 | A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.) |
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | ||
Theorem | nnsuc 7820* | A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) | ||
Theorem | omsucne 7821 | A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.) |
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴) | ||
Theorem | ssnlim 7822* | 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 7823* | Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) | ||
Theorem | omsindsOLD 7824* | Obsolete version of omsinds 7823 as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) | ||
Theorem | peano1 7825 | 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 7825 through peano5 7830 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 7672. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ ∅ ∈ ω | ||
Theorem | peano1OLD 7826 | Obsolete version of peano1 7825 as of 29-Nov-2024. (Contributed by NM, 15-May-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ ∈ ω | ||
Theorem | peano2 7827 | 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 7828 | 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 7829 | 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 7830* | 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 7839. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2137, ax-12 2171. (Revised by Gino Giotto, 3-Oct-2024.) |
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
Theorem | peano5OLD 7831* | Obsolete version of peano5 7830 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
Theorem | nn0suc 7832* | A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
Theorem | find 7833* | 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 | findOLD 7834* | Obsolete version of find 7833 as of 28-May-2024. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) ⇒ ⊢ 𝐴 = ω | ||
Theorem | finds 7835* | 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 7836* | 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 7837* | 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 7838* | 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 7839 | 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 7799 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.) |
⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ ω → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ ω → 𝜑) | ||
Theorem | dmexg 7840 | 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 7841 | 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 7842 | The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ V) | ||
Theorem | fndmexd 7843 | If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ V) | ||
Theorem | dmfex 7844 | 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 7845 | 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 7846 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐴 ∈ V ↔ 𝐹 ∈ V)) | ||
Theorem | dmfexALT 7847 | Alternate proof of dmfex 7844: shorter but using ax-rep 5242. (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 7848 | 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 7849 | 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 7850 | 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 22608. (Contributed by NM, 1-Jan-2007.) |
⊢ ¬ I ∈ V | ||
Theorem | resiexg 7851 | The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7165). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) | ||
Theorem | imaexg 7852 | The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | imaex 7853 | 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 7854 | Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | xpexr 7855 | 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 7856 | If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.) |
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | xpexcnv 7857 | A condition where the converse of xpex 7687 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V) | ||
Theorem | soex 7858 | 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 7859 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7860, elxp6 7955, and elxp7 7956. (Contributed by NM, 17-Feb-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | elxp5 7860 | Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7859 when the double intersection does not create class existence problems (caused by int0 4923). (Contributed by NM, 1-Aug-2004.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | ||
Theorem | cnvexg 7861 | 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 7862 | 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 7863 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V)) | ||
Theorem | f1oexrnex 7864 | 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 7865* | 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 7866 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | coex 7867 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∘ 𝐵) ∈ V | ||
Theorem | funcnvuni 7868* | The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6570 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.) |
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴) | ||
Theorem | fun11uni 7869* | 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 7870 | A function with bounded domain and codomain is a set. This version of fex 7176 is proven without the Axiom of Replacement ax-rep 5242, but depends on ax-un 7672, which is not required for the proof of fex 7176. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) | ||
Theorem | fabexg 7871* | Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V) | ||
Theorem | fabex 7872* | Existence of a set of functions. (Contributed by NM, 3-Dec-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V | ||
Theorem | f1oabexg 7873* | 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 7874* | Lemma for fiun 7875 and f1iun 7876. Formerly part of f1iun 7876. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) | ||
Theorem | fiun 7875* | The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7876. (Contributed by AV, 6-Oct-2023.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) | ||
Theorem | f1iun 7876* | 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 7877* | 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 7878* | Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | f11o 7879* | 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 7880 | Alternate proof of resfunexg 7165, shorter but requiring ax-pow 5320 and ax-un 7672. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | cofunexg 7881 | Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | cofunex2g 7882 | Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) | ||
Theorem | fnexALT 7883 | Alternate proof of fnex 7167, derived using the Axiom of Replacement in the form of funimaexg 6587. This version uses ax-pow 5320 and ax-un 7672, whereas fnex 7167 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | funexw 7884 | Weak version of funex 7169 that holds without ax-rep 5242. 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 7885* | Weak version of mptex 7173 that holds without ax-rep 5242. 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 7886 | 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 7169. (Contributed by NM, 11-Nov-1995.) |
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) | ||
Theorem | zfrep6 7887* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5256 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 5242. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Theorem | focdmex 7888 | If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.) |
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) | ||
Theorem | f1dmex 7889 | 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 5242. (Contributed by NM, 4-Sep-2004.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | f1ovv 7890 | 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 7891* | Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.) |
⊢ 𝐹 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ∈ V | ||
Theorem | fvresex 7892* | 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 7893* | 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 5250, axrep6 5249, ax-rep 5242. See also abrexex2g 7897. There are partial converses under additional conditions, see for instance abnexg 7690. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2137, ax-11 2154, ax-12 2171, ax-pr 5384, ax-un 7672 and shorten proof. (Revised by SN, 11-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | abrexexgOLD 7894* |
Obsolete version of abrexexg 7893 as of 11-Dec-2024. EDITORIAL: Comment
kept since the line of equivalences to ax-rep 5242 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 7171, funex 7169, fnex 7167, resfunexg 7165, and funimaexg 6587. See also abrexex2g 7897. There are partial converses under additional conditions, see for instance abnexg 7690. (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 7895* | Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7893. See also abrexex2 7902. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V | ||
Theorem | iunexg 7896* | The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | abrexex2g 7897* | Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) | ||
Theorem | opabex3d 7898* | 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 7899* | 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 7900* | Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |