| Metamath
Proof Explorer Theorem List (p. 66 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 | onssnel2i 6501 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵) | ||
| Theorem | onelini 6502 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
| Theorem | oneluni 6503 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
| Theorem | onunisuci 6504 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
| ⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
| Theorem | onsseli 6505 | Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.) |
| ⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | onun2i 6506 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) |
| ⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
| Theorem | unizlim 6507 | An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
| ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | ||
| Theorem | on0eqel 6508 | An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.) |
| ⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) | ||
| Theorem | snsn0non 6509 | The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7891). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6510. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
| ⊢ ¬ {{∅}} ∈ On | ||
| Theorem | onxpdisj 6510 | Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non 6509. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ (On ∩ (V × V)) = ∅ | ||
| Theorem | onnev 6511 | The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.) (Proof shortened by Wolf Lammen, 27-May-2024.) |
| ⊢ On ≠ V | ||
| Syntax | cio 6512 | Extend class notation with Russell's definition description binder (inverted iota). |
| class (℩𝑥𝜑) | ||
| Theorem | iotajust 6513* | Soundness justification theorem for df-iota 6514. (Contributed by Andrew Salmon, 29-Jun-2011.) |
| ⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
| Definition | df-iota 6514* |
Define Russell's definition description binder, which can be read as
"the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains
𝑥 as a free variable. Our definition
is meaningful only when there
is exactly one 𝑥 such that 𝜑 is true (see iotaval 6532);
otherwise, it evaluates to the empty set (see iotanul 6539). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use riotacl2 7404 (or iotacl 6547 for unbounded iota), as demonstrated in the proof of supub 9499. This can be easier than applying riotasbc 7406 or a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
| Theorem | dfiota2 6515* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| ⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
| Theorem | nfiota1 6516 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥(℩𝑥𝜑) | ||
| Theorem | nfiotadw 6517* | Deduction version of nfiotaw 6518. Version of nfiotad 6519 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
| Theorem | nfiotaw 6518* | Bound-variable hypothesis builder for the ℩ class. Version of nfiota 6520 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 23-Aug-2011.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
| Theorem | nfiotad 6519 | Deduction version of nfiota 6520. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker nfiotadw 6517 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
| Theorem | nfiota 6520 | Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker nfiotaw 6518 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
| Theorem | cbviotaw 6521* | Change bound variables in a description binder. Version of cbviota 6523 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Andrew Salmon, 1-Aug-2011.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
| Theorem | cbviotavw 6522* | Change bound variables in a description binder. Version of cbviotav 6524 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
| Theorem | cbviota 6523 | Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker cbviotaw 6521 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
| Theorem | cbviotav 6524* | Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker cbviotavw 6522 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
| Theorem | sb8iota 6525 | Variable substitution in description binder. Compare sb8eu 2600. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑) | ||
| Theorem | iotaeq 6526 | Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑)) | ||
| Theorem | iotabi 6527 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | ||
| Theorem | uniabio 6528* | Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∪ {𝑥 ∣ 𝜑} = 𝑦) | ||
| Theorem | iotaval2 6529* | Version of iotaval 6532 using df-iota 6514 instead of dfiota2 6515. (Contributed by SN, 6-Nov-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦) | ||
| Theorem | iotauni2 6530* | Version of iotauni 6536 using df-iota 6514 instead of dfiota2 6515. (Contributed by SN, 6-Nov-2024.) |
| ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑}) | ||
| Theorem | iotanul2 6531* | Version of iotanul 6539 using df-iota 6514 instead of dfiota2 6515. (Contributed by SN, 6-Nov-2024.) |
| ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅) | ||
| Theorem | iotaval 6532* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 23-Nov-2024.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) | ||
| Theorem | iotassuni 6533 | The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) Remove dependency on ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 6-Nov-2024.) |
| ⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑} | ||
| Theorem | iotaex 6534 | Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 6-Nov-2024.) |
| ⊢ (℩𝑥𝜑) ∈ V | ||
| Theorem | iotavalOLD 6535* | Obsolete version of iotaval 6532 as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) | ||
| Theorem | iotauni 6536 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑}) | ||
| Theorem | iotaint 6537 | Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
| Theorem | iota1 6538 | Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
| ⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥)) | ||
| Theorem | iotanul 6539 | Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅) | ||
| Theorem | iotassuniOLD 6540 | Obsolete version of iotassuni 6533 as of 23-Dec-2024. (Contributed by Mario Carneiro, 24-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑} | ||
| Theorem | iotaexOLD 6541 | Obsolete version of iotaex 6534 as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (℩𝑥𝜑) ∈ V | ||
| Theorem | iota4 6542 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) | ||
| Theorem | iota4an 6543 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑) | ||
| Theorem | iota5 6544* | A method for computing iota. (Contributed by NM, 17-Sep-2013.) |
| ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
| Theorem | iotabidv 6545* | Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) | ||
| Theorem | iotabii 6546 | Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) | ||
| Theorem | iotacl 6547 |
Membership law for descriptions.
This can be useful for expanding an unbounded iota-based definition (see df-iota 6514). If you have a bounded iota-based definition, riotacl2 7404 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑}) | ||
| Theorem | iota2df 6548 | A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
| Theorem | iota2d 6549* | A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
| Theorem | iota2 6550* | The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴)) | ||
| Theorem | iotan0 6551* | Representation of "the unique element such that 𝜑 " with a class expression 𝐴 which is not the empty set (that means that "the unique element such that 𝜑 " exists). (Contributed by AV, 30-Jan-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = (℩𝑥𝜑)) → 𝜓) | ||
| Theorem | sniota 6552 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)}) | ||
| Theorem | dfiota4 6553 | The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.) |
| ⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅) | ||
| Theorem | csbiota 6554* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) (Revised by NM, 23-Aug-2018.) |
| ⊢ ⦋𝐴 / 𝑥⦌(℩𝑦𝜑) = (℩𝑦[𝐴 / 𝑥]𝜑) | ||
| Syntax | wfun 6555 | Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.) |
| wff Fun 𝐴 | ||
| Syntax | wfn 6556 | Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.) |
| wff 𝐴 Fn 𝐵 | ||
| Syntax | wf 6557 | Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.) |
| wff 𝐹:𝐴⟶𝐵 | ||
| Syntax | wf1 6558 | Extend the definition of a wff to include one-to-one functions. (Read: 𝐹 maps 𝐴 one-to-one into 𝐵.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27. |
| wff 𝐹:𝐴–1-1→𝐵 | ||
| Syntax | wfo 6559 | Extend the definition of a wff to include onto functions. (Read: 𝐹 maps 𝐴 onto 𝐵.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27. |
| wff 𝐹:𝐴–onto→𝐵 | ||
| Syntax | wf1o 6560 | Extend the definition of a wff to include one-to-one onto functions. (Read: 𝐹 maps 𝐴 one-to-one onto 𝐵.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27. |
| wff 𝐹:𝐴–1-1-onto→𝐵 | ||
| Syntax | cfv 6561 | Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴", or "𝐹 of 𝐴". |
| class (𝐹‘𝐴) | ||
| Syntax | wiso 6562 | Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵". |
| wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) | ||
| Definition | df-fun 6563 | Define predicate that determines if some class 𝐴 is a function. Definition 10.1 of [Quine] p. 65. For example, the expression Fun cos is true once we define cosine (df-cos 16106). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5225 with the maps-to notation (see df-mpt 5226 and df-mpo 7436). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6564), a function with a given domain and codomain (df-f 6565), a one-to-one function (df-f1 6566), an onto function (df-fo 6567), or a one-to-one onto function (df-f1o 6568). For alternate definitions, see dffun2 6571, dffun3 6575, dffun4 6577, dffun5 6578, dffun6 6574, dffun7 6593, dffun8 6594, and dffun9 6595. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | ||
| Definition | df-fn 6564 | Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6738, dffn3 6748, dffn4 6826, and dffn5 6967. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) | ||
| Definition | df-f 6565 | Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. 𝐹:𝐴⟶𝐵 can be read as "𝐹 is a function from 𝐴 to 𝐵". For alternate definitions, see dff2 7119, dff3 7120, and dff4 7121. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | ||
| Definition | df-f1 6566 |
Define a one-to-one function. For equivalent definitions see dff12 6803
and dff13 7275. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We
use their notation ("1-1" above the arrow).
A one-to-one function is also called an "injection" or an "injective function", 𝐹:𝐴–1-1→𝐵 can be read as "𝐹 is an injection from 𝐴 into 𝐵". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon 18132. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | ||
| Definition | df-fo 6567 |
Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27.
We use their notation ("onto" under the arrow). For alternate
definitions, see dffo2 6824, dffo3 7122, dffo4 7123, and dffo5 7124.
An onto function is also called a "surjection" or a "surjective function", 𝐹:𝐴–onto→𝐵 can be read as "𝐹 is a surjection from 𝐴 onto 𝐵". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi 18133. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | ||
| Definition | df-f1o 6568 |
Define a one-to-one onto function. For equivalent definitions see
dff1o2 6853, dff1o3 6854, dff1o4 6856, and dff1o5 6857. Compare Definition
6.15(6) of [TakeutiZaring] p. 27.
We use their notation ("1-1" above
the arrow and "onto" below the arrow).
A one-to-one onto function is also called a "bijection" or a "bijective function", 𝐹:𝐴–1-1-onto→𝐵 can be read as "𝐹 is a bijection between 𝐴 and 𝐵". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso 18136. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7344, two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren 8995. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | ||
| Definition | df-fv 6569* | Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 16186 after we define cosine in df-cos 16106). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5226 and df-mpo 7436), but this is not required. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → (𝐹‘3) = 9 (ex-fv 30462). Note that df-ov 7434 will define two-argument functions using ordered pairs as (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6941 and fvprc 6898). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar 𝐹(𝐴) notation for a function's value at 𝐴, i.e., "𝐹 of 𝐴", but without context-dependent notational ambiguity. Alternate definitions are dffv2 7004, dffv3 6902, fv2 6901, and fv3 6924 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6996 and funfv2 6997. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6963. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now Theorem dffv4 6903. (Revised by Scott Fenton, 6-Oct-2017.) |
| ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) | ||
| Definition | df-isom 6570* | Define the isomorphism predicate. We read this as "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵". Normally, 𝑅 and 𝑆 are ordering relations on 𝐴 and 𝐵 respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that 𝑅 and 𝑆 are subscripts. (Contributed by NM, 4-Mar-1997.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | ||
| Theorem | dffun2 6571* | Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2141, ax-12 2177. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2157. (Revised by BTernaryTau, 29-Dec-2024.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) | ||
| Theorem | dffun2OLD 6572* | Obsolete version of dffun2 6571 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2141, ax-12 2177. (Revised by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) | ||
| Theorem | dffun2OLDOLD 6573* | Obsolete version of dffun2 6571 as of 11-Dec-2024. (Contributed by NM, 29-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) | ||
| Theorem | dffun6 6574* | Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2141, ax-12 2177. (Revised by SN, 19-Dec-2024.) |
| ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) | ||
| Theorem | dffun3 6575* | Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof shortened by SN, 19-Dec-2024.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧))) | ||
| Theorem | dffun3OLD 6576* | Obsolete version of dffun3 6575 as of 19-Dec-2024. Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧))) | ||
| Theorem | dffun4 6577* | Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴) → 𝑦 = 𝑧))) | ||
| Theorem | dffun5 6578* | Alternate definition of function. (Contributed by NM, 29-Dec-1996.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑦 = 𝑧))) | ||
| Theorem | dffun6f 6579* | Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦)) | ||
| Theorem | dffun6OLD 6580* | Obsolete version of dffun6 6574 as of 19-Dec-2024. (Contributed by NM, 9-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) | ||
| Theorem | funmo 6581* | A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) (Proof shortened by SN, 19-Dec-2024.) |
| ⊢ (Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦) | ||
| Theorem | funmoOLD 6582* | Obsolete version of funmo 6581 as of 19-Dec-2024. (Contributed by NM, 24-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦) | ||
| Theorem | funrel 6583 | A function is a relation. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (Fun 𝐴 → Rel 𝐴) | ||
| Theorem | 0nelfun 6584 | A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.) |
| ⊢ (Fun 𝑅 → ∅ ∉ 𝑅) | ||
| Theorem | funss 6585 | Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
| ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴)) | ||
| Theorem | funeq 6586 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
| ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | ||
| Theorem | funeqi 6587 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (Fun 𝐴 ↔ Fun 𝐵) | ||
| Theorem | funeqd 6588 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) | ||
| Theorem | nffun 6589 | Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.) |
| ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥Fun 𝐹 | ||
| Theorem | sbcfung 6590 | Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹)) | ||
| Theorem | funeu 6591* | There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦) | ||
| Theorem | funeu2 6592* | There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.) |
| ⊢ ((Fun 𝐹 ∧ 〈𝐴, 𝐵〉 ∈ 𝐹) → ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) | ||
| Theorem | dffun7 6593* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun8 6594 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)) | ||
| Theorem | dffun8 6594* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6593. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)) | ||
| Theorem | dffun9 6595* | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
| ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦)) | ||
| Theorem | funfn 6596 | A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004.) |
| ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) | ||
| Theorem | funfnd 6597 | A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → Fun 𝐴) ⇒ ⊢ (𝜑 → 𝐴 Fn dom 𝐴) | ||
| Theorem | funi 6598 | The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6696. (Contributed by NM, 30-Apr-1998.) |
| ⊢ Fun I | ||
| Theorem | nfunv 6599 | The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.) |
| ⊢ ¬ Fun V | ||
| Theorem | funopg 6600 | A Kuratowski ordered pair of sets is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6617, as relsnopg 5813 is to relop 5861. (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun 〈𝐴, 𝐵〉) → 𝐴 = 𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |