| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-11257) |
(11258-12844) |
(12845-19026) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | curry2 5201 |
Composition with |
| Theorem | curry2f 5202 | Functionality of a curried function with a constant second argument. |
| Theorem | curry2val 5203 | The value of a curried function with a constant second argument. |
| Theorem | fparlem1 5204 | Lemma for fpar 5208. [Auxiliary lemma - not displayed.] |
| Theorem | fparlem2 5205 | Lemma for fpar 5208. [Auxiliary lemma - not displayed.] |
| Theorem | fparlem3 5206 | Lemma for fpar 5208. [Auxiliary lemma - not displayed.] |
| Theorem | fparlem4 5207 | Lemma for fpar 5208. [Auxiliary lemma - not displayed.] |
| Theorem | fpar 5208 |
Merge two functions in parallel. Use as the second argument of a
composition with a (2-place) operation to build compound operations such
as |
| Theorem | fsplit 5209 |
A function that can be used to feed a common value to both operands of
an operation. Use as the second argument of a composition with the
function of fpar 5208 in order to build compound functions such as
|
| Theorem | frxp 5210 | A lexicographical ordering of two well founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
| Theorem | xporderlem 5211 | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) [Auxiliary lemma - not displayed.] |
| Theorem | poxp 5212 | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
| Theorem | soxp 5213 | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
| Theorem | wexp 5214 | A lexicographical ordering of two well ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
| Theorem | fnwelem 5215 | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) |
| Theorem | fnwe 5216 | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) |
| The iota operation ("the unique set such that...") | ||
| Syntax | cio 5217 | Extend class notation with Russell's definition description binder. |
| Theorem | iotajust 5218 | Soundness justification theorem for df-iota 5219. (Contributed by Andrew Salmon, 29-Jun-2011.) |
| Definition | df-iota 5219 |
Define Russell's definition description binder, which can be read as
"the unique |
| Theorem | dfiota2 5220 | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| Theorem | hbiota1 5221 |
Bound-variable hypothesis builder for the |
| Theorem | hbiota 5222 |
Bound-variable hypothesis builder for the |
| Theorem | hbiotad 5223 | Deduction version of hbiota 5222. |
| Theorem | cbviotaf 5224 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| Theorem | cbviota 5225 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| Theorem | sb8iota 5226 | Variable substitution in description binder. Compare sb8eu 2050. |
| Theorem | iotaeq 5227 | Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| Theorem | iotabi 5228 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
| Theorem | uniabio 5229 | 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 5230 | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| Theorem | iotaequ 5231 |
Equivalence between two different forms of |
| Theorem | iotanul 5232 |
Theorem 8.22 in [Quine] p. 57. This theorem is
the result if there
isn't exactly one |
| Theorem | iotaex 5233 |
Theorem 8.23 in [Quine] p. 58. This theorem
proves the existence of the
|
| Theorem | iota4 5234 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| Theorem | iota4an 5235 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| Theorem | iotabidv 5236 | Formula-building deduction rule for iota. |
| Theorem | iotacl 5237 | Membership law for descriptions. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| Theorem | iota1 5238 | Property of iota. Compare euuni 3945. |
| Theorem | reiotacl2 5239 | Membership law for descriptions. Compare reucl2 3952. |
| Theorem | reiotacl 5240 | Membership law for descriptions. Compare reucl 3399. |
| Theorem | reiota4 5241 | Substitution law for descriptions. Compare reuuni4 3951. |
| Theorem | reiota1 5242 | Property of iota. Compare reuuni1 3946. |
| Theorem | reiota2df 5243 | Deduction version of reiota2f 5244. |
| Theorem | reiota2f 5244 |
A condition that allows us to represent "the unique element in |
| Theorem | reiota2 5245 |
A condition that allows us to represent "the unique element in |
| Theorem | reiotass2 5246 | Restriction of a unique element to a smaller class. Compare reuuniss2 3955. |
| Theorem | dffv3 5247 | A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013.) |
| Theorem | fv4 5248 |
Alternate definition of the value of a function. The value of a
function expressed using |
| Cantor's Theorem | ||
| Theorem | canth 5249 |
No set |
| Theorem | ncanth 5250 | Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 3616). Specifically, the identity function maps the universe onto its power class. Compare canth 5249 that works for sets. See also the remark in ru 2697 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. |
| Functions on ordinals; strictly monotone ordinal functions | ||
| Theorem | iunon 5251 |
The indexed union of a set of ordinal numbers |
| Theorem | iinon 5252 |
The nonempty indexed intersection of a class of ordinal numbers
|
| Theorem | onfununi 5253 | A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of [Enderton] p. 218. (Contributed by Eric Schmidt, 26-May-2009.) |
| Theorem | onopruni 5254 | A variant of onfununi 5253 for operations. (Contributed by Eric Schmidt, 26-May-2009.) |
| Theorem | onopriun 5255 | A variant of onopruni 5254 with indexed unions. (Contributed by Eric Schmidt, 26-May-2009.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) |
| Syntax | csmo 5256 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
| Definition | df-smo 5257 | Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. |
| Theorem | dfsmo2 5258 | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
| Theorem | issmo 5259 |
Conditions for which |
| Theorem | issmo2 5260 | Alternative definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| Theorem | smoeq 5261 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| Theorem | smodm 5262 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| Theorem | smores 5263 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| Theorem | smores3 5264 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
| Theorem | smores2 5265 | A strictly monotone ordinal function restricted to an ordinal is still monotone. |
| Theorem | smodm2 5266 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| Theorem | smofvon2 5267 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| Theorem | iordsmo 5268 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| Theorem | smo0 5269 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
| Theorem | smofvon 5270 |
If |
| Theorem | smoel 5271 |
If |
| Theorem | smoiun 5272 | The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.) |
| Theorem | smoiso 5273 |
If |
| Theorem | smoel2 5274 | A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| Theorem | smo11 5275 | A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013.) |
| Theorem | smoord 5276 | A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
| Theorem | smoword 5277 | A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
| Theorem | smogt 5278 | A strictly monotone ordinal function is greater than or equal to its argument. (Contributed by Mario Carneiro, 28-Feb-2013.) |
| Theorem | smorndom 5279 | The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.) |
| Theorem | smoiso2 5280 |
The strictly monotone ordinal functions are also epsilon isomorphisms of
subclasses of |
| Theorem | smoge 5281 |
A strictly monotonic function is always increasing. Exercise 1 in
[TakeutiZaring] p. 50. It holds
even when |
| Transfinite recursion | ||
| Theorem | tfrlem1 5282 | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) |
| Theorem | tfrlem2 5283 | Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 5282 into the main proof. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) [Auxiliary lemma - not displayed.] |
| Theorem | tfrlem3 5284 |
Lemma for transfinite recursion. Let |
| Theorem | tfrlem3a 5285 |
Lemma for transfinite recursion. Let |
| Theorem | tfrlem4 5286 |
Lemma for transfinite recursion. |
| Theorem | tfrlem5 5287 | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. [Auxiliary lemma - not displayed.] |
| Theorem | tfrlem6 5288 | Lemma for transfinite recursion. The union of all acceptable functions is a relation. [Auxiliary lemma - not displayed.] |
| Theorem | tfrlem7 5289 | Lemma for transfinite recursion. The union of all acceptable functions is a function. [Auxiliary lemma - not displayed.] |
| Theorem | tfrlem8 5290 |
Lemma for transfinite recursion. The domain of |
| Theorem | tfrlem9 5291 |
Lemma for transfinite recursion. Here we compute the value of |
| Theorem | tfrlem10 5292 |
Lemma for transfinite recursion. We define class |
| Theorem | tfrlem11 5293 |
Lemma for transfinite recursion. Compute the value of |
| Theorem | tfrlem12 5294 |
Lemma for transfinite recursion. Show |
| Theorem | tfrlem13 5295 |
Lemma for transfinite recursion. If |
| Theorem | tfr1 5296 |
Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of
[TakeutiZaring] p. 47. We start
with an arbitrary class |
| Theorem | tfr2 5297 |
Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of
[TakeutiZaring] p. 47. Here we
show that the function |
| Theorem | tfr3 5298 |
Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of
[TakeutiZaring] p. 47. Finally
we show that |
| Theorem | tz7.44lem1 5299 |
|
| Theorem | tz7.44-1 5300 |
The value of |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |