mmtheorems53 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 5201-5300 - Page 53 of 191

Type	Label	Description
Statement
Theorem	curry2 5201	Composition with `'(1st |` (_V X. {C})) turns any binary operation F with a constant second operand into a function G of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.)
|- G = (F o. `'(1st |` (_V X. {C})))   =>   |- ((F Fn (A X. B) /\ C e. B) -> G = {<.x, y>. | (x e. A /\ y = (xFC))})
Theorem	curry2f 5202	Functionality of a curried function with a constant second argument.
|- G = (F o. `'(1st |` (_V X. {C})))   =>   |- ((F:(A X. B)-->D /\ C e. B) -> G:A-->D)
Theorem	curry2val 5203	The value of a curried function with a constant second argument.
|- G = (F o. `'(1st |` (_V X. {C})))   =>   |- ((F Fn (A X. B) /\ C e. B /\ D e. U) -> (G` D) = (DFC))
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 z = ((sqr` x) + (abs` y)).
|- H = ((`'(1st |` (_V X. _V)) o. (F o. (1st |` (_V X. _V)))) i^i (`'(2nd |` (_V X. _V)) o. (G o. (2nd |` (_V X. _V)))))   =>   |- ((F Fn A /\ G Fn B) -> H = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = <.(F` x), (G` y)>.)})
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 y = ((sqr` x) + (abs` x)).
|- `'(1st |` _I ) = {<.x, y>. | y = <.x, x>.}
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.)
|- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}   =>   |- ((R Fr A /\ S Fr B) -> T Fr (A X. B))
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.)
|- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}   =>   |- ((R Po A /\ S Po B) -> T Po (A X. B))
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.)
|- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}   =>   |- ((R Or A /\ S Or B) -> T Or (A X. B))
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.)
|- T = {<.x, y>. | ((x e. (A X. B) /\ y e. (A X. B)) /\ ((1st` x)R(1st` y) \/ ((1st` x) = (1st` y) /\ (2nd` x)S(2nd` y))))}   =>   |- ((R We A /\ S We B) -> T We (A X. B))
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.)
|- T = {<.x, y>. | ((x e. A /\ y e. A) /\ ((F` x)R(F` y) \/ ((F` x) = (F` y) /\ xSy)))}   &   |- Q = {<.u, v>. | ((u e. (B X. A) /\ v e. (B X. A)) /\ ((1st` u)R(1st` v) \/ ((1st` u) = (1st` v) /\ (2nd` u)S(2nd` v))))}   &   |- G = (z e. A |-> <.(F` z), z>.)   =>   |- ((F:A-->B /\ R We B /\ S We A) -> T We A)
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.)
|- T = {<.x, y>. | ((x e. A /\ y e. A) /\ ((F` x)R(F` y) \/ ((F` x) = (F` y) /\ xSy)))}   =>   |- ((F:A-->B /\ R We B /\ S We A) -> T We A)
The iota operation ("the unique set such that...")
Syntax	cio 5217	Extend class notation with Russell's definition description binder.
class (iotaxph)
Theorem	iotajust 5218	Soundness justification theorem for df-iota 5219. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- U.{y | {x | ph} = {y}} = U.{z | {x | ph} = {z}}
Definition	df-iota 5219	Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 5230); otherwise, it evaluates to the empty set (see iotanul 5232).
|- (iotaxph) = U.{y | {x | ph} = {y}}
Theorem	dfiota2 5220	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (iotaxph) = U.{y | A.x(ph <-> x = y)}
Theorem	hbiota1 5221	Bound-variable hypothesis builder for the iota class. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (y e. (iotaxph) -> A.x y e. (iotaxph))
Theorem	hbiota 5222	Bound-variable hypothesis builder for the iota class.
|- (ph -> A.xph)   =>   |- (z e. (iotayph) -> A.x z e. (iotayph))
Theorem	hbiotad 5223	Deduction version of hbiota 5222.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (z e. (iotayps) -> A.x z e. (iotayps)))
Theorem	cbviotaf 5224	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- (x = y -> (ph <-> ps))   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (iotaxph) = (iotayps)
Theorem	cbviota 5225	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- (x = y -> (ph <-> ps))   =>   |- (iotaxph) = (iotayps)
Theorem	sb8iota 5226	Variable substitution in description binder. Compare sb8eu 2050.
|- (ph -> A.yph)   =>   |- (iotaxph) = (iotay[y / x]ph)
Theorem	iotaeq 5227	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (A.x x = y -> (iotaxph) = (iotayph))
Theorem	iotabi 5228	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (A.x(ph <-> ps) -> (iotaxph) = (iotaxps))
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.)
|- (A.x(ph <-> x = y) -> U.{x | ph} = y)
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.)
|- (A.x(ph <-> x = y) -> (iotaxph) = y)
Theorem	iotaequ 5231	Equivalence between two different forms of iota. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!xph -> (iotaxph) = U.{x | ph})
Theorem	iotanul 5232	Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies ph. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (-. E!xph -> (iotaxph) = (/))
Theorem	iotaex 5233	Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (iotaxph) e. _V
Theorem	iota4 5234	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!xph -> [(iotaxph) / x]ph)
Theorem	iota4an 5235	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!x(ph /\ ps) -> [(iotax(ph /\ ps)) / x]ph)
Theorem	iotabidv 5236	Formula-building deduction rule for iota.
|- (ph -> (ps <-> ch))   =>   |- (ph -> (iotaxps) = (iotaxch))
Theorem	iotacl 5237	Membership law for descriptions. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- (E!xph -> (iotaxph) e. {x | ph})
Theorem	iota1 5238	Property of iota. Compare euuni 3945.
|- (E!xph -> (ph <-> (iotaxph) = x))
Theorem	reiotacl2 5239	Membership law for descriptions. Compare reucl2 3952.
|- (E!x e. A ph -> (iotax(x e. A /\ ph)) e. {x e. A | ph})
Theorem	reiotacl 5240	Membership law for descriptions. Compare reucl 3399.
|- (E!x e. A ph -> (iotax(x e. A /\ ph)) e. A)
Theorem	reiota4 5241	Substitution law for descriptions. Compare reuuni4 3951.
|- (E!x e. A ph -> [(iotax(x e. A /\ ph)) / x]ph)
Theorem	reiota1 5242	Property of iota. Compare reuuni1 3946.
|- ((x e. A /\ E!x e. A ph) -> (ph <-> (iotax(x e. A /\ ph)) = x))
Theorem	reiota2df 5243	Deduction version of reiota2f 5244.
|- (ph -> A.xph)   &   |- (ph -> (y e. B -> A.x y e. B))   &   |- ((ph /\ B e. A) -> (ch -> A.xch))   &   |- (ph -> (x = B -> (ps <-> ch)))   =>   |- ((ph /\ B e. A /\ E!x e. A ps) -> (ch <-> (iotax(x e. A /\ ps)) = B))
Theorem	reiota2f 5244	A condition that allows us to represent "the unique element in A such that ph " with a class expression B. The second hypothesis is a weakened bound variable condition that allows hbsbc1g 2706 to be used. Compare reuuni2f 3947.
|- (y e. B -> A.x y e. B)   &   |- (B e. A -> (ps -> A.xps))   &   |- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> (iotax(x e. A /\ ph)) = B))
Theorem	reiota2 5245	A condition that allows us to represent "the unique element in A such that ph " with a class expression B. Compare reuuni2 3948.
|- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> (iotax(x e. A /\ ph)) = B))
Theorem	reiotass2 5246	Restriction of a unique element to a smaller class. Compare reuuniss2 3955.
|- (((A C_ B /\ A.x e. A (ph -> ps)) /\ (E.x e. A ph /\ E!x e. B ps)) -> (iotax(x e. A /\ ph)) = (iotax(x e. B /\ ps)))
Theorem	dffv3 5247	A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013.)
|- (F` A) = (iotaxx e. (F"{A}))
Theorem	fv4 5248	Alternate definition of the value of a function. The value of a function expressed using iota. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- A e. _V   =>   |- (F` A) = (iotaxAFx)
Cantor's Theorem
Theorem	canth 5249	No set A is equinumerous to its power set (Cantor's theorem), i.e. no function can map A it onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 5717. Note that A must be a set: this theorem does not hold when A is too large to be a set; see ncanth 5250 for a counterexample. (Use nex 1739 if you want the form -. E.ff:A-onto->~PA.)
|- A e. _V   =>   |- -. F:A-onto->~PA
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.
|- _I :_V-onto->~P_V
Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 5251	The indexed union of a set of ordinal numbers B(x) is an ordinal number.
|- A e. _V   &   |- B e. _V   =>   |- (A.x e. A B e. On -> U_x e. A B e. On)
Theorem	iinon 5252	The nonempty indexed intersection of a class of ordinal numbers B(x) is an ordinal number.
|- B e. _V   =>   |- ((A.x e. A B e. On /\ A =/= (/)) -> |^|_x e. A B e. On)
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.)
|- (Lim y -> (F` y) = U_x e. y (F` x))   &   |- ((x e. On /\ y e. On /\ x C_ y) -> (F` x) C_ (F` y))   =>   |- ((S e. T /\ S C_ On /\ S =/= (/)) -> (F` U.S) = U_x e. S (F` x))
Theorem	onopruni 5254	A variant of onfununi 5253 for operations. (Contributed by Eric Schmidt, 26-May-2009.)
|- (Lim y -> (AFy) = U_x e. y (AFx))   &   |- ((x e. On /\ y e. On /\ x C_ y) -> (AFx) C_ (AFy))   =>   |- ((S e. T /\ S C_ On /\ S =/= (/)) -> (AFU.S) = U_x e. S (AFx))
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.)
|- (Lim y -> (AFy) = U_x e. y (AFx))   &   |- ((x e. On /\ y e. On /\ x C_ y) -> (AFx) C_ (AFy))   =>   |- ((K e. T /\ A.z e. K L e. On /\ K =/= (/)) -> (AFU_z e. K L) = U_z e. K (AFL))
Syntax	csmo 5256	Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.
wff Smo A
Definition	df-smo 5257	Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50.
|- (Smo A <-> (A:dom A-->On /\ Ord dom A /\ A.x e. dom AA.y e. dom A(x e. y -> (A` x) e. (A` y))))
Theorem	dfsmo2 5258	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- (Smo F <-> (F:dom F-->On /\ Ord dom F /\ A.x e. dom FA.y e. x (F` y) e. (F` x)))
Theorem	issmo 5259	Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.)
|- A:B-->On   &   |- Ord B   &   |- ((x e. B /\ y e. B) -> (x e. y -> (A` x) e. (A` y)))   &   |- dom A = B   =>   |- Smo A
Theorem	issmo2 5260	Alternative definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- (F:A-->B -> ((B C_ On /\ Ord A /\ A.x e. A A.y e. x (F` y) e. (F` x)) -> Smo F))
Theorem	smoeq 5261	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- (A = B -> (Smo A <-> Smo B))
Theorem	smodm 5262	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- (Smo A -> Ord dom A)
Theorem	smores 5263	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ((Smo A /\ B e. dom A) -> Smo (A |` B))
Theorem	smores3 5264	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
|- ((Smo (A |` B) /\ C e. (dom A i^i B) /\ Ord B) -> Smo (A |` C))
Theorem	smores2 5265	A strictly monotone ordinal function restricted to an ordinal is still monotone.
|- ((Smo F /\ Ord A) -> Smo (F |` A))
Theorem	smodm2 5266	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ((F Fn A /\ Smo F) -> Ord A)
Theorem	smofvon2 5267	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- (Smo F -> (F` B) e. On)
Theorem	iordsmo 5268	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- Ord A   =>   |- Smo ( _I |` A)
Theorem	smo0 5269	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 5270	If B is a strictly monotone ordinal function, and A is in the domain of B, then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- ((Smo B /\ A e. dom B) -> (B` A) e. On)
Theorem	smoel 5271	If x is less than y then a strictly monotone function's value will be strictly less at x than at y. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ((Smo B /\ A e. dom B /\ C e. A) -> (B` C) e. (B` A))
Theorem	smoiun 5272	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ((Smo B /\ A e. dom B) -> U_x e. A (B` x) C_ (B` A))
Theorem	smoiso 5273	If F is an isomorphism from an ordinal A onto B, which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
|- ((F Isom _E , _E (A, B) /\ Ord A /\ B C_ On) -> Smo F)
Theorem	smoel2 5274	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- (((F Fn A /\ Smo F) /\ (B e. A /\ C e. B)) -> (F` C) e. (F` B))
Theorem	smo11 5275	A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ((F:A-->B /\ Smo F) -> F:A-1-1->B)
Theorem	smoord 5276	A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- (((F Fn A /\ Smo F) /\ (C e. A /\ D e. A)) -> (C e. D <-> (F` C) e. (F` D)))
Theorem	smoword 5277	A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- (((F Fn A /\ Smo F) /\ (C e. A /\ D e. A)) -> (C C_ D <-> (F` C) C_ (F` D)))
Theorem	smogt 5278	A strictly monotone ordinal function is greater than or equal to its argument. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ((F Fn A /\ Smo F /\ C e. A) -> C C_ (F` C))
Theorem	smorndom 5279	The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.)
|- ((F:A-->B /\ Smo F /\ Ord B) -> A C_ B)
Theorem	smoiso2 5280	The strictly monotone ordinal functions are also epsilon isomorphisms of subclasses of On.
|- ((Ord A /\ B C_ On) -> ((F:A-onto->B /\ Smo F) <-> F Isom _E , _E (A, B)))
Theorem	smoge 5281	A strictly monotonic function is always increasing. Exercise 1 in [TakeutiZaring] p. 50. It holds even when C is transfinite. (Contributed by Andrew Salmon, 23-Nov-2011.)
|- dom A = B   &   |- Smo A   =>   |- (C e. B -> C C_ (A` C))
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.)
|- (A e. On -> ((F Fn A /\ G Fn A) -> (A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. A (F` x) = (G` x))))
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 A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. [Auxiliary lemma - not displayed.]
Theorem	tfrlem3a 5285	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. [Auxiliary lemma - not displayed.]
Theorem	tfrlem4 5286	Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function. [Auxiliary lemma - not displayed.]
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 F is ordinal. (The proof was shortened by Alan Sare, 11-Mar-2008.) [Auxiliary lemma - not displayed.]
Theorem	tfrlem9 5291	Lemma for transfinite recursion. Here we compute the value of F (the union of all acceptable functions). [Auxiliary lemma - not displayed.]
Theorem	tfrlem10 5292	Lemma for transfinite recursion. We define class C by extending F with one ordered pair. We will assume, falsely, that domain of F is a member of, and thus not equal to, On. Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem13 5295, thus showing the domain of F does in fact equal On. Here we show (under the false assumption) that C is a function extending the domain of F by one. (The proof was shortened by Alan Sare, 20-Feb-2008.) [Auxiliary lemma - not displayed.]
Theorem	tfrlem11 5293	Lemma for transfinite recursion. Compute the value of C. [Auxiliary lemma - not displayed.]
Theorem	tfrlem12 5294	Lemma for transfinite recursion. Show C is an acceptable function. [Auxiliary lemma - not displayed.]
Theorem	tfrlem13 5295	Lemma for transfinite recursion. If dom F is in On, then C is acceptable, and thus a subset of F, but dom C is bigger than dom F. This is a contradiction, so dom F must be On. [Auxiliary lemma - not displayed.]
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 G, normally a function, and define a class A of all "acceptable" functions. The final function we're interested in is the union F of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F. In this first part we show that F is a function whose domain is all ordinal numbers.
|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}   &   |- F = U.A   =>   |- F Fn On
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 F has the property that for any function G whatsoever, the "next" value of F is G recursively applied to all "previous" values of F.
|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}   &   |- F = U.A   =>   |- (z e. On -> (F` z) = (G` (F |` z)))
Theorem	tfr3 5298	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F.
|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}   &   |- F = U.A   =>   |- ((B Fn On /\ A.x e. On (B` x) = (G` (B |` x))) -> B = F)
Theorem	tz7.44lem1 5299	G is a function. Lemma for tz7.44-1 5300, tz7.44-2 5301, and tz7.44-3 5302. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.)
|- G = {<.x, y>. | ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x))}   =>   |- Fun G
Theorem	tz7.44-1 5300	The value of F at (/). Part 1 of Theorem 7.44 of [TakeutiZaring] p. 49.
|- G = {<.x, y>. | ((x = (/) /\ y = A) \/ (-. (x = (/) \/ Lim dom x) /\ y = (H` (x` U.dom x))) \/ (Lim dom x /\ y = U.ran x))}   &   |- F Fn On   &   |- (x e. On -> (F` x) = (G` (F |` x)))   &   |- A e. _V   =>   |- (F` (/)) = A