Home | Metamath
Proof Explorer Theorem List (p. 64 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onun2i 6301 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
Theorem | unizlim 6302 | An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | ||
Theorem | on0eqel 6303 | An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.) |
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) | ||
Theorem | snsn0non 6304 | The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7578). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6305. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ¬ {{∅}} ∈ On | ||
Theorem | onxpdisj 6305 | 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 6304. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (On ∩ (V × V)) = ∅ | ||
Theorem | onnev 6306 | 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.) |
⊢ On ≠ V | ||
Syntax | cio 6307 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩𝑥𝜑) | ||
Theorem | iotajust 6308* | Soundness justification theorem for df-iota 6309. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-iota 6309* |
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 6324);
otherwise, it evaluates to the empty set (see iotanul 6328). 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 7124 (or iotacl 6336 for unbounded iota), as demonstrated in the proof of supub 8917. This can be easier than applying riotasbc 7126 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 6310* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | nfiota1 6311 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥𝜑) | ||
Theorem | nfiotadw 6312* | Version of nfiotad 6314 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
Theorem | nfiotaw 6313* | Version of nfiota 6315 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
Theorem | nfiotad 6314 | Deduction version of nfiota 6315. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker nfiotadw 6312 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
Theorem | nfiota 6315 | Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker nfiotaw 6313 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
Theorem | cbviotaw 6316* | Version of cbviota 6318 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | cbviotavw 6317* | Version of cbviotav 6319 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | cbviota 6318 | Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbviotaw 6316 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | cbviotav 6319* | Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbviotavw 6317 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | sb8iota 6320 | Variable substitution in description binder. Compare sb8eu 2682. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | iotaeq 6321 | Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑)) | ||
Theorem | iotabi 6322 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | ||
Theorem | uniabio 6323* | 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 | iotaval 6324* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) | ||
Theorem | iotauni 6325 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑}) | ||
Theorem | iotaint 6326 | Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | iota1 6327 | Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥)) | ||
Theorem | iotanul 6328 | 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 | iotassuni 6329 | The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑} | ||
Theorem | iotaex 6330 | 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.) |
⊢ (℩𝑥𝜑) ∈ V | ||
Theorem | iota4 6331 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) | ||
Theorem | iota4an 6332 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑) | ||
Theorem | iota5 6333* | A method for computing iota. (Contributed by NM, 17-Sep-2013.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
Theorem | iotabidv 6334* | Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) | ||
Theorem | iotabii 6335 | Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) | ||
Theorem | iotacl 6336 |
Membership law for descriptions.
This can be useful for expanding an unbounded iota-based definition (see df-iota 6309). If you have a bounded iota-based definition, riotacl2 7124 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑}) | ||
Theorem | iota2df 6337 | A condition that allows us to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
Theorem | iota2d 6338* | A condition that allows us to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
Theorem | iota2 6339* | The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴)) | ||
Theorem | iotan0 6340* | 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 6341 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)}) | ||
Theorem | dfiota4 6342 | The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.) |
⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅) | ||
Theorem | csbiota 6343* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦𝜑) = (℩𝑦[𝐴 / 𝑥]𝜑) | ||
Syntax | wfun 6344 | Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.) |
wff Fun 𝐴 | ||
Syntax | wfn 6345 | Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.) |
wff 𝐴 Fn 𝐵 | ||
Syntax | wf 6346 | Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.) |
wff 𝐹:𝐴⟶𝐵 | ||
Syntax | wf1 6347 | 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 6348 | 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 6349 | 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 6350 | Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴", or "𝐹 of 𝐴". |
class (𝐹‘𝐴) | ||
Syntax | wiso 6351 | Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵". |
wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) | ||
Definition | df-fun 6352 | 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 15418). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5139 with the maps-to notation (see df-mpt 5140 and df-mpo 7155). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6353), a function with a given domain and codomain (df-f 6354), a one-to-one function (df-f1 6355), an onto function (df-fo 6356), or a one-to-one onto function (df-f1o 6357). For alternate definitions, see dffun2 6360, dffun3 6361, dffun4 6362, dffun5 6363, dffun6 6365, dffun7 6377, dffun8 6378, and dffun9 6379. (Contributed by NM, 1-Aug-1994.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | ||
Definition | df-fn 6353 | Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6511, dffn3 6520, dffn4 6591, and dffn5 6719. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) | ||
Definition | df-f 6354 | 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 6860, dff3 6861, and dff4 6862. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | ||
Definition | df-f1 6355 |
Define a one-to-one function. For equivalent definitions see dff12 6569
and dff13 7007. 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 17341. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | ||
Definition | df-fo 6356 |
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 6589, dffo3 6863, dffo4 6864, and dffo5 6865.
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 17342. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | ||
Definition | df-f1o 6357 |
Define a one-to-one onto function. For equivalent definitions see
dff1o2 6615, dff1o3 6616, dff1o4 6618, and dff1o5 6619. 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 17345. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7071, 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 8512. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | ||
Definition | df-fv 6358* | Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 15497 after we define cosine in df-cos 15418). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5140 and df-mpo 7155), but this is not required. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → (𝐹‘3) = 9 (ex-fv 28216). Note that df-ov 7153 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 6695 and fvprc 6658). 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 6751, dffv3 6661, fv2 6660, and fv3 6683 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6745 and funfv2 6746. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6716. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now theorem dffv4 6662. (Revised by Scott Fenton, 6-Oct-2017.) |
⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥) | ||
Definition | df-isom 6359* | 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 6360* | Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) | ||
Theorem | dffun3 6361* | Alternate definition of function. (Contributed by NM, 29-Dec-1996.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧))) | ||
Theorem | dffun4 6362* | Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴) → 𝑦 = 𝑧))) | ||
Theorem | dffun5 6363* | Alternate definition of function. (Contributed by NM, 29-Dec-1996.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑦 = 𝑧))) | ||
Theorem | dffun6f 6364* | 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 | dffun6 6365* | Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) |
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) | ||
Theorem | funmo 6366* | A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) |
⊢ (Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦) | ||
Theorem | funrel 6367 | A function is a relation. (Contributed by NM, 1-Aug-1994.) |
⊢ (Fun 𝐴 → Rel 𝐴) | ||
Theorem | 0nelfun 6368 | A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.) |
⊢ (Fun 𝑅 → ∅ ∉ 𝑅) | ||
Theorem | funss 6369 | Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴)) | ||
Theorem | funeq 6370 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | ||
Theorem | funeqi 6371 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Fun 𝐴 ↔ Fun 𝐵) | ||
Theorem | funeqd 6372 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) | ||
Theorem | nffun 6373 | Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥Fun 𝐹 | ||
Theorem | sbcfung 6374 | Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | funeu 6375* | 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 6376* | There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.) |
⊢ ((Fun 𝐹 ∧ 〈𝐴, 𝐵〉 ∈ 𝐹) → ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) | ||
Theorem | dffun7 6377* | 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 6378 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)) | ||
Theorem | dffun8 6378* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6377. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)) | ||
Theorem | dffun9 6379* | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦)) | ||
Theorem | funfn 6380 | 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 6381 | A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → Fun 𝐴) ⇒ ⊢ (𝜑 → 𝐴 Fn dom 𝐴) | ||
Theorem | funi 6382 | The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6470. (Contributed by NM, 30-Apr-1998.) |
⊢ Fun I | ||
Theorem | nfunv 6383 | The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.) |
⊢ ¬ Fun V | ||
Theorem | funopg 6384 | A Kuratowski ordered pair of sets is a function only if its components are equal. Compare with funsng 6400. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun 〈𝐴, 𝐵〉) → 𝐴 = 𝐵) | ||
Theorem | funopab 6385* | A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.) |
⊢ (Fun {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∀𝑥∃*𝑦𝜑) | ||
Theorem | funopabeq 6386* | A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.) |
⊢ Fun {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐴} | ||
Theorem | funopab4 6387* | A class of ordered pairs of values in the form used by df-mpt 5140 is a function. (Contributed by NM, 17-Feb-2013.) |
⊢ Fun {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝑦 = 𝐴)} | ||
Theorem | funmpt 6388 | A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | funmpt2 6389 | Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ Fun 𝐹 | ||
Theorem | funco 6390 | The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) | ||
Theorem | funresfunco 6391 | Composition of two functions, generalization of funco 6390. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ ((Fun (𝐹 ↾ ran 𝐺) ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺)) | ||
Theorem | funres 6392 | A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.) |
⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) | ||
Theorem | funssres 6393 | The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.) |
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺) | ||
Theorem | fun2ssres 6394 | Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.) |
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) | ||
Theorem | funun 6395 | The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺)) | ||
Theorem | fununmo 6396* | If the union of classes is a function, there is at most one element in relation to an arbitrary element regarding one of these classes. (Contributed by AV, 18-Jul-2019.) |
⊢ (Fun (𝐹 ∪ 𝐺) → ∃*𝑦 𝑥𝐹𝑦) | ||
Theorem | fununfun 6397 | If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.) |
⊢ (Fun (𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺)) | ||
Theorem | fundif 6398 | A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.) |
⊢ (Fun 𝐹 → Fun (𝐹 ∖ 𝐴)) | ||
Theorem | funcnvsn 6399 | The converse singleton of an ordered pair is a function. This is equivalent to funsn 6402 via cnvsn 6078, but stating it this way allows us to skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM, 30-Apr-2015.) |
⊢ Fun ◡{〈𝐴, 𝐵〉} | ||
Theorem | funsng 6400 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |