mmtheorems82 - 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-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19465

Statement List for Metamath Proof Explorer - 8101-8200 - Page 82 of 195

Type	Label	Description
Statement
Theorem	nninfm 8101	The infimum of the set of natural numbers is one. Note that "`' < " turns sup into inf.
|- sup(NN, RR, `' < ) = 1
Theorem	nn0infm 8102	The infimum of the set of nonnegative integers is zero. Note that "`' < " turns sup into inf.
|- sup(NN0, RR, `' < ) = 0
Theorem	infmssuzle 8103	The infimum of a subset of a set of upper integers is less than or equal to all members of the subset. Note that the "`' < " argument turns supremum into infimum (for which we do not currently have a separate notation).
|- ((S C_ (ZZ>=` M) /\ A e. S) -> sup(S, RR, `' < ) <_ A)
Theorem	infmssuzleOLD 8104	The infimum of a subset of a set of upper integers is less than or equal to all members of the subset. Note that the "`' < " argument turns supremum into infimum (for which we do not currently have a separate notation).
|- ((S C_ (ZZ>=` M) /\ S =/= (/) /\ A e. S) -> sup(S, RR, `' < ) <_ A)
Theorem	infmssuzcl 8105	The infimum of a subset of a set of upper integers belongs to the subset.
|- ((S C_ (ZZ>=` M) /\ S =/= (/)) -> sup(S, RR, `' < ) e. S)
Theorem	ublbneg 8106	The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.)
|- (E.x e. RR A.y e. A y <_ x -> E.x e. RR A.y e. {z e. RR | -uz e. A}x <_ y)
Theorem	eqreznegel 8107	Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.)
|- (A C_ ZZ -> {z e. RR | -uz e. A} = {z e. ZZ | -uz e. A})
Theorem	negn0 8108	The image under negation of a nonempty set of reals is nonempty. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ((A C_ RR /\ A =/= (/)) -> {z e. RR | -uz e. A} =/= (/))
Theorem	supminf 8109	The supremum of a bounded-above set of reals is the negation of the supremum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ((A C_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> sup(A, RR, < ) = -usup({z e. RR | -uz e. A}, RR, `' < ))
Theorem	lbzbi 8110	If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.)
|- (A C_ RR -> (E.x e. RR A.y e. A x <_ y <-> E.x e. ZZ A.y e. A x <_ y))
Theorem	suprzcl 8111	The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ((A C_ ZZ /\ A =/= (/) /\ E.x e. RR A.y e. A y <_ x) -> sup(A, RR, < ) e. A)
Finite intervals of integers
Syntax	cfz 8112	Extend class notation to include the notation for a contiguous finite set of integers. Read "M...N " as "the set of integers from M to N inclusive."
class ...
Definition	df-fz 8113	Define an operation that produces a finite set of sequential integers. Read "M...N " as "the set of integers from M to N inclusive." See fzval 8114 for its value and additional comments.
|- ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
Theorem	fzval 8114	The value of a finite set of sequential integers. E.g., 2...5 means the set {2, 3, 4, 5}. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where NN_k means our 1...k; he calls these sets segments of the integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M...N) = {k e. ZZ | (M <_ k /\ k <_ N)})
Theorem	elfz1 8115	Membership in a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> (K e. (M...N) <-> (K e. ZZ /\ M <_ K /\ K <_ N)))
Theorem	elfz 8116	Membership in a finite set of sequential integers.
|- ((K e. ZZ /\ M e. ZZ /\ N e. ZZ) -> (K e. (M...N) <-> (M <_ K /\ K <_ N)))
Theorem	elfz2 8117	Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ.
|- (N e. A -> (K e. (M...N) <-> ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) /\ (M <_ K /\ K <_ N))))
Theorem	elfzlem 8118	Lemma for elfzel1 8126 and others. [Auxiliary lemma - not displayed.]
Theorem	elfz5 8119	Membership in a finite set of sequential integers.
|- ((K e. (ZZ>=` M) /\ N e. ZZ) -> (K e. (M...N) <-> K <_ N))
Theorem	elfz4 8120	Membership in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ /\ K e. ZZ) /\ (M <_ K /\ K <_ N)) -> K e. (M...N))
Theorem	elfzuzb 8121	Membership in a finite set of sequential integers in terms of sets of upper integers.
|- (N e. A -> (K e. (M...N) <-> (K e. (ZZ>=` M) /\ N e. (ZZ>=` K))))
Theorem	eluzfz 8122	Membership in a finite set of sequential integers.
|- ((K e. (ZZ>=` M) /\ N e. (ZZ>=` K)) -> K e. (M...N))
Theorem	elfzuz3 8123	Membership in a finite set of sequential integers implies membership in a set of upper integers.
|- ((N e. A /\ K e. (M...N)) -> N e. (ZZ>=` K))
Theorem	elfzel2i 8124	Membership in a finite set of sequential integer implies the upper bound is an integer.
|- N e. _V   =>   |- (K e. (M...N) -> N e. ZZ)
Theorem	elfzel2g 8125	Membership in a finite set of sequential integers implies the upper bound is an integer.
|- ((N e. A /\ K e. (M...N)) -> N e. ZZ)
Theorem	elfzel1 8126	Membership in a finite set of sequential integer implies the lower bound is an integer.
|- (K e. (M...N) -> M e. ZZ)
Theorem	elfzelz 8127	A member of a finite set of sequential integer is an integer.
|- (K e. (M...N) -> K e. ZZ)
Theorem	elfzle1 8128	A member of a finite set of sequential integer is greater than or equal to the lower bound.
|- (K e. (M...N) -> M <_ K)
Theorem	elfzle2 8129	A member of a finite set of sequential integer is less than or equal to the upper bound.
|- (K e. (M...N) -> K <_ N)
Theorem	elfzle3 8130	Membership in a finite set of sequential integer implies the bounds are comparable.
|- ((N e. A /\ K e. (M...N)) -> M <_ N)
Theorem	elfzuz2 8131	Implication of membership in a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> N e. (ZZ>=` M))
Theorem	eluzfz1 8132	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>=` M) -> M e. (M...N))
Theorem	elfzuz 8133	A member of a finite set of sequential integers belongs to a set of upper integers.
|- (K e. (M...N) -> K e. (ZZ>=` M))
Theorem	eluzfz2 8134	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>=` M) -> N e. (M...N))
Theorem	eluzfz2b 8135	Membership in a finite set of sequential integers - special case.
|- (N e. (ZZ>=` M) <-> N e. (M...N))
Theorem	elfz3 8136	Membership in a finite set of sequential integers containing one integer.
|- (N e. ZZ -> N e. (N...N))
Theorem	elfz1eq 8137	Membership in a finite set of sequential integers containing one integer.
|- (K e. (N...N) -> K = N)
Theorem	fzn 8138	A finite set of sequential integers is empty if the bounds are reversed.
|- ((M e. ZZ /\ N e. ZZ) -> (N < M <-> (M...N) = (/)))
Theorem	fzen 8139	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
|- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (M...N) ~~ ((M + K)...(N + K)))
Theorem	fz1n 8140	A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (N e. NN0 -> ((1...N) = (/) <-> N = 0))
Theorem	0fz1 8141	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
|- ((N e. NN0 /\ F Fn (1...N)) -> (F = (/) <-> N = 0))
Theorem	fz01en 8142	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
|- (N e. ZZ -> (0...(N - 1)) ~~ (1...N))
Theorem	elfznn 8143	A member of a finite set of sequential integers starting at 1 is a natural number.
|- (K e. (1...N) -> K e. NN)
Theorem	elfz2nn0 8144	Membership in a finite set of sequential integers starting at 0.
|- (N e. A -> (K e. (0...N) <-> (K e. NN0 /\ N e. NN0 /\ K <_ N)))
Theorem	elfznn0 8145	A member of a finite set of sequential integers starting at 0 is a nonnegative integer.
|- (K e. (0...N) -> K e. NN0)
Theorem	elfz3nn0 8146	The upper bound of a nonempty finite set of sequential integers starting at 0 is a nonnegative integer.
|- ((N e. A /\ K e. (0...N)) -> N e. NN0)
Theorem	fznn0sub 8147	Subtraction closure for a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> (N - K) e. NN0)
Theorem	fznn0sub2 8148	Subtraction closure for a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (0...N)) -> (N - K) e. (0...N))
Theorem	fzaddel 8149	Membership of a sum in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (J e. (M...N) <-> (J + K) e. ((M + K)...(N + K))))
Theorem	fzsubel 8150	Membership of a difference in a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (J e. (M...N) <-> (J - K) e. ((M - K)...(N - K))))
Theorem	fzopth 8151	A finite set of sequential integers can represent an ordered pair.
|- ((N e. (ZZ>=` M) /\ K e. A) -> ((M...N) = (J...K) <-> (M = J /\ N = K)))
Theorem	fzss1 8152	Subset relationship for finite sets of sequential integers.
|- ((K e. (ZZ>=` M) /\ N e. ZZ) -> (K...N) C_ (M...N))
Theorem	fzss2 8153	Subset relationship for finite sets of sequential integers.
|- ((N e. (ZZ>=` K) /\ M e. ZZ) -> (M...K) C_ (M...N))
Theorem	fzssuz 8154	A finite set of sequential integers is a subset of a set of upper integers.
|- (M...N) C_ (ZZ>=` M)
Theorem	fzsuc 8155	Join a successor to the end of a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ /\ M <_ (N + 1)) -> (M...(N + 1)) = ((M...N) u. {(N + 1)}))
Theorem	fzssp1 8156	Subset relationship for finite sets of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M...N) C_ (M...(N + 1)))
Theorem	fzp1ss 8157	Subset relationship for finite sets of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> ((M + 1)...N) C_ (M...N))
Theorem	fzelp1 8158	Membership in a set of sequential integers with an appended element.
|- ((N e. A /\ K e. (M...N)) -> K e. (M...(N + 1)))
Theorem	fzelp1i 8159	Membership in a set of sequential integers with an appended element.
|- N e. _V   =>   |- (K e. (M...N) -> K e. (M...(N + 1)))
Theorem	elfzp1 8160	Append an element to a finite set of sequential integers.
|- (N e. (ZZ>=` M) -> (K e. (M...(N + 1)) <-> (K e. (M...N) \/ K = (N + 1))))
Theorem	fzsn 8161	A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009 )
|- (M e. ZZ -> (M...M) = {M})
Theorem	fzpr 8162	A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009 )
|- (M e. ZZ -> (M...(M + 1)) = {M, (M + 1)})
Theorem	fztp 8163	A finite interval of integers with three elements.
|- (M e. ZZ -> (M...(M + 2)) = {M, (M + 1), (M + 2)})
Theorem	fzprval 8164	Two ways of defining the first two values of a sequence on NN.
|- (A.x e. (1...2)(F` x) = if(x = 1, A, B) <-> ((F` 1) = A /\ (F` 2) = B))
Theorem	fztpval 8165	Two ways of defining the first three values of a sequence on NN.
|- (A.x e. (1...3)(F` x) = if(x = 1, A, if(x = 2, B, C)) <-> ((F` 1) = A /\ (F` 2) = B /\ (F` 3) = C))
Theorem	fzrev 8166	Reversal of start and end of a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (K e. ((J - N)...(J - M)) <-> (J - K) e. (M...N)))
Theorem	fzrev2 8167	Reversal of start and end of a finite set of sequential integers.
|- (((M e. ZZ /\ N e. ZZ) /\ (J e. ZZ /\ K e. ZZ)) -> (K e. (M...N) <-> (J - K) e. ((J - N)...(J - M))))
Theorem	fzrev2i 8168	Reversal of start and end of a finite set of sequential integers.
|- ((N e. A /\ J e. ZZ /\ K e. (M...N)) -> (J - K) e. ((J - N)...(J - M)))
Theorem	fzrev3 8169	The "complement" of a member of a finite set of sequential integers.
|- ((N e. A /\ K e. ZZ) -> (K e. (M...N) <-> ((M + N) - K) e. (M...N)))
Theorem	fzrev3i 8170	The "complement" of a member of a finite set of sequential integers.
|- ((N e. A /\ K e. (M...N)) -> ((M + N) - K) e. (M...N))
Theorem	fznn0 8171	Finite set of sequential integers starting at 0.
|- (N e. NN0 -> (K e. (0...N) <-> (K e. NN0 /\ K <_ N)))
Theorem	fznn 8172	Finite set of sequential integers starting at 1.
|- (N e. NN -> (K e. (1...N) <-> (K e. NN /\ K <_ N)))
Theorem	elfzm11 8173	Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ((M e. ZZ /\ N e. ZZ) -> (K e. (M...(N - 1)) <-> (K e. ZZ /\ M <_ K /\ K < N)))
Theorem	fz1eqblem 8174	Lemma for fz1eqb 8175 $. [Auxiliary lemma - not displayed.]
Theorem	fz1eqb 8175	Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ((M e. NN0 /\ N e. NN0) -> ((1...M) = (1...N) <-> M = N))
Theorem	fseq1p1m1lem1 8176	Lemma for fseq1p1m1 8179. [Auxiliary lemma - not displayed.]
Theorem	fseq1p1m1lem2 8177	Lemma for fseq1p1m1 8179. [Auxiliary lemma - not displayed.]
Theorem	fseq1p1m1lem3 8178	Lemma for fseq1p1m1 8179. [Auxiliary lemma - not displayed.]
Theorem	fseq1p1m1 8179	Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.)
|- H = {<.(N + 1), B>.}   =>   |- (N e. NN0 -> ((F:(1...N)-->A /\ B e. A /\ G = (F u. H)) <-> (G:(1...(N + 1))-->A /\ (G` (N + 1)) = B /\ F = (G |` (1...N)))))
Theorem	fseq1m1p1 8180	Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.)
|- H = {<.N, B>.}   =>   |- (N e. NN -> ((F:(1...(N - 1))-->A /\ B e. A /\ G = (F u. H)) <-> (G:(1...N)-->A /\ (G` N) = B /\ F = (G |` (1...(N - 1))))))
Theorem	fz1sbc 8181	Quantification over a one-member finite set of sequential integers in terms of substitution.
|- (N e. ZZ -> (A.k e. (N...N)ph <-> [N / k]ph))
Theorem	fzneuz 8182	No finite set of sequential integers equals a set of upper integers.
|- ((N e. (ZZ>=` M) /\ K e. ZZ) -> -. (M...N) = (ZZ>=` K))
Theorem	fzrevral 8183	Reversal of scanning order inside of a quantification over a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. (M...N)ph <-> A.k e. ((K - N)...(K - M))[(K - k) / j]ph))
Theorem	fzrevral2 8184	Reversal of scanning order inside of a quantification over a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. ((K - N)...(K - M))ph <-> A.k e. (M...N)[(K - k) / j]ph))
Theorem	fzrevral3 8185	Reversal of scanning order inside of a quantification over a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ) -> (A.j e. (M...N)ph <-> A.k e. (M...N)[((M + N) - k) / j]ph))
Theorem	fzshftral 8186	Shift the scanning order inside of a quantification over a finite set of sequential integers.
|- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. (M...N)ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))
Theorem	fsequb 8187	The values of a finite real sequence have an upper bound. Warning: The HTML proof page is 1/2 megabyte in size.
|- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(F` k) e. RR) -> E.x e. RR A.k e. (M...N)(F` k) < x)
Theorem	fsequb2 8188	The values of a finite real sequence have an upper bound.
|- ((N e. (ZZ>=` M) /\ F:(M...N)-->RR) -> E.x e. RR A.y e. ran F y <_ x)
Theorem	fseqsupcl 8189	The values of a finite real sequence have a supremum.
|- ((N e. (ZZ>=` M) /\ F:(M...N)-->RR) -> sup(ran F, RR, < ) e. RR)
Theorem	fseqsupubi 8190	The values of a finite real sequence are bounded by their supremum.
|- N e. _V   =>   |- ((K e. (M...N) /\ F:(M...N)-->RR) -> (F` K) <_ sup(ran F, RR, < ))
The infinite sequence builder "seq1"
Theorem	om2uz0i 8191	The mapping G is a one-to-one mapping from om onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number C (normally 0 for the upper integers NN0 or 1 for the upper integers NN), 1 maps to C + 1, etc. This theorem shows the value of G at ordinal natural number zero. (This series of theorems generalizes an earlier series for NN0 contributed by Raph Levien, 10-Apr-2004.)
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (G` (/)) = C
Theorem	om2uzsuci 8192	The value of G (see om2uz0i 8191) at a successor.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (A e. om -> (G` suc A) = ((G` A) + 1))
Theorem	om2uzuzi 8193	The value G (see om2uz0i 8191) at an ordinal natural number is in the upper integers.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (A e. om -> (G` A) e. {z e. ZZ | C <_ z})
Theorem	om2uzlti 8194	Less-than relation for G (see om2uz0i 8191).
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- ((A e. om /\ B e. om) -> (A e. B -> (G` A) < (G` B)))
Theorem	om2uzlt2i 8195	The mapping G (see om2uz0i 8191) preserves order.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- ((A e. om /\ B e. om) -> (A e. B <-> (G` A) < (G` B)))
Theorem	om2uzrani 8196	Range of G (see om2uz0i 8191).
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- ran G = {z e. ZZ | C <_ z}
Theorem	om2uzf1oi 8197	G (see om2uz0i 8191) is a one-to-one onto mapping.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- G:om-1-1-onto->{z e. ZZ | C <_ z}
Theorem	om2uzisoi 8198	G (see om2uz0i 8191) is an isomorphism from natural ordinals to upper integers.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- G Isom _E , < (om, {z e. ZZ | C <_ z})
Theorem	uzrdgvali 8199	A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0) with characteristic function F and initial value A. Normally F is a function on the partition, and A is a member of the partition. See also comment in om2uz0i 8191.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (B e. {z e. ZZ | C <_ z} -> ((rec(F, A) o. `'G)` B) = (rec(F, A)` (`'G` B)))
Theorem	uzrdginii 8200	Initial value of a recursive definition generator on upper integers. See comment in uzrdgvali 8199.
|- C e. ZZ   &   |- G = (rec({<.x, y>. | y = (x + 1)}, C) |` om)   =>   |- (A e. B -> ((rec(F, A) o. `'G)` C) = A)