![]() |
Metamath
Proof Explorer Theorem List (p. 424 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onsupnub 42301* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ (π΅ β On β§ βπ§ β π΄ π§ β π΅)) β βͺ π΄ β π΅) | ||
Theorem | onfisupcl 42302 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9296. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β ((π΄ β Fin β§ π΄ β β ) β βͺ π΄ β π΄)) | ||
Theorem | onelord 42303 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6390 and eloni 6375. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β π΄) β Ord π΅) | ||
Theorem | onepsuc 42304 | Every ordinal is less than its successor, relationship version. Lemma 1.7 of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.) |
β’ (π΄ β On β π΄ E suc π΄) | ||
Theorem | epsoon 42305 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7765 and weso 5668. (Contributed by RP, 15-Jan-2025.) |
β’ E Or On | ||
Theorem | epirron 42306 | The strict order on the ordinals is irreflexive. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.) |
β’ (π΄ β On β Β¬ π΄ E π΄) | ||
Theorem | oneptr 42307 | The strict order on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ E π΅ β§ π΅ E πΆ) β π΄ E πΆ)) | ||
Theorem | oneltr 42308 | The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6411. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ)) | ||
Theorem | oneptri 42309 | The strict, complete (linear) order on the ordinals is complete. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ E π΅ β¨ π΅ E π΄ β¨ π΄ = π΅)) | ||
Theorem | oneltri 42310 | The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6397. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅ β¨ π΅ β π΄ β¨ π΄ = π΅)) | ||
Theorem | ordeldif 42311 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
β’ ((Ord π΄ β§ Ord π΅) β (πΆ β (π΄ β π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldifsucon 42312 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΅ β On) β (πΆ β (π΄ β suc π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldif1o 42313 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
β’ (Ord π΄ β (π΅ β (π΄ β 1o) β (π΅ β π΄ β§ π΅ β β ))) | ||
Theorem | ordne0gt0 42314 | Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6420. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΄ β β ) β β β π΄) | ||
Theorem | ondif1i 42315 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8504. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β (On β 1o) β β β π΄) | ||
Theorem | onsucelab 42316* | The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β On β suc π΄ β {π β On β£ βπ β On π = suc π}) | ||
Theorem | dflim6 42317* | A limit ordinal is a non-zero ordinal which is not a succesor ordinal. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.) |
β’ (Lim π΄ β (Ord π΄ β§ π΄ β β β§ Β¬ βπ β On π΄ = suc π)) | ||
Theorem | limnsuc 42318* | A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.) |
β’ (Lim π΄ β Β¬ π΄ β {π β On β£ βπ β On π = suc π}) | ||
Theorem | onsucss 42319 | If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of [Schloeder] p. 2. See ordsucss 7809. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β On β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | ordnexbtwnsuc 42320* | For any distinct pair of ordinals, if there is no ordinal between the lesser and the greater, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.) |
β’ ((π΄ β π΅ β§ Ord π΅) β (βπ β On Β¬ (π΄ β π β§ π β π΅) β π΅ = suc π΄)) | ||
Theorem | orddif0suc 42321 | For any distinct pair of ordinals, if the set difference between the greater and the successor of the lesser is empty, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 17-Jan-2025.) |
β’ ((π΄ β π΅ β§ Ord π΅) β ((π΅ β suc π΄) = β β π΅ = suc π΄)) | ||
Theorem | onsucf1lem 42322* | For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the succesor of. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.) |
β’ (π΄ β On β β*π β On π΄ = suc π) | ||
Theorem | onsucf1olem 42323* | The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β β§ Β¬ Lim π΄) β β!π β On π΄ = suc π) | ||
Theorem | onsucrn 42324* | The successor operation is surjective onto its range, the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.) |
β’ πΉ = (π₯ β On β¦ suc π₯) β β’ ran πΉ = {π β On β£ βπ β On π = suc π} | ||
Theorem | onsucf1o 42325* | The successor operation is a bijective function between the ordinals and the class of succesor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.) |
β’ πΉ = (π₯ β On β¦ suc π₯) β β’ πΉ:Onβ1-1-ontoβ{π β On β£ βπ β On π = suc π} | ||
Theorem | dflim7 42326* | A limit ordinal is a non-zero ordinal that contains all the successors of its elements. Lemma 1.18 of [Schloeder] p. 2. Closely related to dflim4 7840. (Contributed by RP, 17-Jan-2025.) |
β’ (Lim π΄ β (Ord π΄ β§ βπ β π΄ suc π β π΄ β§ π΄ β β )) | ||
Theorem | onov0suclim 42327 | Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025.) |
β’ (π΄ β On β (π΄ β β ) = π·) & β’ ((π΄ β On β§ πΆ β On) β (π΄ β suc πΆ) = πΈ) & β’ (((π΄ β On β§ π΅ β On) β§ Lim π΅) β (π΄ β π΅) = πΉ) β β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ β π΅) = π·) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ β π΅) = πΈ) β§ (Lim π΅ β (π΄ β π΅) = πΉ))) | ||
Theorem | oa0suclim 42328* | Closed form expression of the value of ordinal addition for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.3 of [Schloeder] p. 4. See oa0 8519, oasuc 8527, and oalim 8535. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ +o π΅) = π΄) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ +o π΅) = suc (π΄ +o πΆ)) β§ (Lim π΅ β (π΄ +o π΅) = βͺ π β π΅ (π΄ +o π)))) | ||
Theorem | om0suclim 42329* | Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of [Schloeder] p. 4. See om0 8520, omsuc 8529, and omlim 8536. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ Β·o π΅) = β ) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ Β·o π΅) = ((π΄ Β·o πΆ) +o π΄)) β§ (Lim π΅ β (π΄ Β·o π΅) = βͺ π β π΅ (π΄ Β·o π)))) | ||
Theorem | oe0suclim 42330* | Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of [Schloeder] p. 4. See oe0 8525, oesuc 8530, oe0m1 8524, and oelim 8537. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ βo π΅) = 1o) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ βo π΅) = ((π΄ βo πΆ) Β·o π΄)) β§ (Lim π΅ β (π΄ βo π΅) = if(β β π΄, βͺ π β π΅ (π΄ βo π), β )))) | ||
Theorem | oaomoecl 42331 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8538, omcl 8539, oecl 8540. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +o π΅) β On β§ (π΄ Β·o π΅) β On β§ (π΄ βo π΅) β On)) | ||
Theorem | onsupsucismax 42332* | If the union of a set of ordinals is a successor ordinal, then that union is the maximum element of the set. This is not a bijection because sets where the maximum element is zero or a limit ordinal exist. Lemma 2.11 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β (βπ β On βͺ π΄ = suc π β βͺ π΄ β π΄)) | ||
Theorem | onsssupeqcond 42333* | If for every element of a set of ordinals there is an element of a subset which is at least as large, then the union of the set and the subset is the same. Lemma 2.12 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β ((π΅ β π΄ β§ βπ β π΄ βπ β π΅ π β π) β βͺ π΄ = βͺ π΅)) | ||
Theorem | limexissup 42334 | An ordinal which is a limit ordinal is equal to its supremum. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.) |
β’ ((Lim π΄ β§ π΄ β π) β π΄ = sup(π΄, On, E )) | ||
Theorem | limiun 42335* | A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6426. (Contributed by RP, 27-Jan-2025.) |
β’ (Lim π΄ β π΄ = βͺ π₯ β π΄ π₯) | ||
Theorem | limexissupab 42336* | An ordinal which is a limit ordinal is equal to the supremum of the class of all its elements. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.) |
β’ ((Lim π΄ β§ π΄ β π) β π΄ = sup({π₯ β£ π₯ β π΄}, On, E )) | ||
Theorem | om1om1r 42337 | Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8545 and om1r 8546 for individual statements. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β On β ((1o Β·o π΄) = (π΄ Β·o 1o) β§ (π΄ Β·o 1o) = π΄)) | ||
Theorem | oe0rif 42338 | Ordinal zero raised to any non-zero ordinal power is zero and zero to the zeroth power is one. Lemma 2.18 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β On β (β βo π΄) = if(β β π΄, β , 1o)) | ||
Theorem | oasubex 42339* | While subtraction can't be a binary operation on ordinals, for any pair of ordinals there exists an ordinal that can be added to the lessor (or equal) one which will sum to the greater. Theorem 2.19 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β π΄) β βπ β On (π β π΄ β§ (π΅ +o π) = π΄)) | ||
Theorem | nnamecl 42340 | Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8614, nnmcl 8615, nnecl 8616. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β ((π΄ +o π΅) β Ο β§ (π΄ Β·o π΅) β Ο β§ (π΄ βo π΅) β Ο)) | ||
Theorem | onsucwordi 42341 | The successor operation preserves the less-than-or-equal relationship between ordinals. Lemma 3.1 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅ β suc π΄ β suc π΅)) | ||
Theorem | oalim2cl 42342 | The ordinal sum of any ordinal with a limit ordinal on the right is a limit ordinal. (Contributed by RP, 6-Feb-2025.) |
β’ ((π΄ β On β§ Lim π΅ β§ π΅ β π) β Lim (π΄ +o π΅)) | ||
Theorem | oaltublim 42343 | Given πΆ is a limit ordinal, the sum of any ordinal with an ordinal less than πΆ is less than the sum of the first ordinal with πΆ. Lemma 3.5 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β πΆ β§ (Lim πΆ β§ πΆ β π)) β (π΄ +o π΅) β (π΄ +o πΆ)) | ||
Theorem | oaordi3 42344 | Ordinal addition of the same number on the left preserves the ordering of the numbers on the right. Lemma 3.6 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΅ β πΆ β (π΄ +o π΅) β (π΄ +o πΆ))) | ||
Theorem | oaord3 42345 | When the same ordinal is added on the left, ordering of the sums is equivalent to the ordering of the ordinals on the right. Theorem 3.7 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΅ β πΆ β (π΄ +o π΅) β (π΄ +o πΆ))) | ||
Theorem | 1oaomeqom 42346 | Ordinal one plus omega is equal to omega. See oaabs 8650 for the sum of any natural number on the left and ordinal at least as large as omega on the right. Lemma 3.8 of [Schloeder] p. 8. See oaabs2 8651 where a power of omega is the upper bound of the left and a lower bound on the right. (Contributed by RP, 29-Jan-2025.) |
β’ (1o +o Ο) = Ο | ||
Theorem | oaabsb 42347 | The right addend absorbs the sum with an ordinal iff that ordinal times omega is less than or equal to the right addend. (Contributed by RP, 19-Feb-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ Β·o Ο) β π΅ β (π΄ +o π΅) = π΅)) | ||
Theorem | oaordnrex 42348 | When omega is added on the right to ordinals zero and one, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.) |
β’ Β¬ (β β 1o β (β +o Ο) β (1o +o Ο)) | ||
Theorem | oaordnr 42349* | When the same ordinal is added on the right, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.) |
β’ βπ β On βπ β On βπ β On Β¬ (π β π β (π +o π) β (π +o π)) | ||
Theorem | omge1 42350 | Any non-zero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of [Schloeder] p. 8. See omword1 8576. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ Β·o π΅)) | ||
Theorem | omge2 42351 | Any non-zero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of [Schloeder] p. 9. See omword2 8577. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΄ β β ) β π΅ β (π΄ Β·o π΅)) | ||
Theorem | omlim2 42352 | The non-zero product with an limit ordinal on the right is a limit ordinal. Lemma 3.13 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β β ) β§ (Lim π΅ β§ π΅ β π)) β Lim (π΄ Β·o π΅)) | ||
Theorem | omord2lim 42353 | Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β β ) β§ (Lim πΆ β§ πΆ β π)) β (π΅ β πΆ β (π΄ Β·o π΅) β (π΄ Β·o πΆ))) | ||
Theorem | omord2i 42354 | Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β β ) β§ πΆ β On) β (π΅ β πΆ β (π΄ Β·o π΅) β (π΄ Β·o πΆ))) | ||
Theorem | omord2com 42355 | When the same non-zero ordinal is multiplied on the left, ordering of the products is equivalent to the ordering of the ordinals on the right. Theorem 3.16 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΅ β πΆ β§ β β π΄) β (π΄ Β·o π΅) β (π΄ Β·o πΆ))) | ||
Theorem | 2omomeqom 42356 | Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.) |
β’ (2o Β·o Ο) = Ο | ||
Theorem | omnord1ex 42357 | When omega is multiplied on the right to ordinals one and two, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 29-Jan-2025.) |
β’ Β¬ (1o β 2o β (1o Β·o Ο) β (2o Β·o Ο)) | ||
Theorem | omnord1 42358* | When the same non-zero ordinal is multiplied on the right, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 4-Feb-2025.) |
β’ βπ β On βπ β On βπ β (On β 1o) Β¬ (π β π β (π Β·o π) β (π Β·o π)) | ||
Theorem | oege1 42359 | Any non-zero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of [Schloeder] p. 10. See oewordi 8594. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ βo π΅)) | ||
Theorem | oege2 42360 | Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of [Schloeder] p. 10. See oeworde 8596. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ π΅ β On) β π΅ β (π΄ βo π΅)) | ||
Theorem | rp-oelim2 42361 | The power of an ordinal at least as large as two with a limit ordinal on thr right is a limit ordinal. Lemma 3.21 of [Schloeder] p. 10. See oelimcl 8603. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim π΅ β§ π΅ β π)) β Lim (π΄ βo π΅)) | ||
Theorem | oeord2lim 42362 | Given a limit ordinal, the power of any base at least as large as two raised to an ordinal less than that limit ordinal is less than the power of that base raised to the limit ordinal . Lemma 3.22 of [Schloeder] p. 10. See oeordi 8590. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim πΆ β§ πΆ β π)) β (π΅ β πΆ β (π΄ βo π΅) β (π΄ βo πΆ))) | ||
Theorem | oeord2i 42363 | Ordinal exponentiation of the same base at least as large as two preserves the ordering of the exponents. Lemma 3.23 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ πΆ β On) β (π΅ β πΆ β (π΄ βo π΅) β (π΄ βo πΆ))) | ||
Theorem | oeord2com 42364 | When the same base at least as large as two is raised to ordinal powers, , ordering of the power is equivalent to the ordering of the exponents. Theorem 3.24 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ π΅ β On β§ πΆ β On) β (π΅ β πΆ β (π΄ βo π΅) β (π΄ βo πΆ))) | ||
Theorem | nnoeomeqom 42365 | Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
β’ ((π΄ β Ο β§ 1o β π΄) β (π΄ βo Ο) = Ο) | ||
Theorem | df3o2 42366 | Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , 1o, 2o} | ||
Theorem | df3o3 42367 | Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , {β }, {β , {β }}} | ||
Theorem | oenord1ex 42368 | When ordinals two and three are both raised to the power of omega, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
β’ Β¬ (2o β 3o β (2o βo Ο) β (3o βo Ο)) | ||
Theorem | oenord1 42369* | When two ordinals (both at least as large as two) are raised to the same power, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 4-Feb-2025.) |
β’ βπ β (On β 2o)βπ β (On β 2o)βπ β (On β 1o) Β¬ (π β π β (π βo π) β (π βo π)) | ||
Theorem | oaomoencom 42370* | Ordinal addition, multiplication, and exponentiation do not generally commute. Theorem 4.1 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.) |
β’ (βπ β On βπ β On Β¬ (π +o π) = (π +o π) β§ βπ β On βπ β On Β¬ (π Β·o π) = (π Β·o π) β§ βπ β On βπ β On Β¬ (π βo π) = (π βo π)) | ||
Theorem | oenassex 42371 | Ordinal two raised to two to the zeroth power is not the same as two squared then raised to the zeroth power. (Contributed by RP, 30-Jan-2025.) |
β’ Β¬ (2o βo (2o βo β )) = ((2o βo 2o) βo β ) | ||
Theorem | oenass 42372* | Ordinal exponentiation is not associative. Remark 4.6 of [Schloeder] p. 14. (Contributed by RP, 30-Jan-2025.) |
β’ βπ β On βπ β On βπ β On Β¬ (π βo (π βo π)) = ((π βo π) βo π) | ||
Theorem | cantnftermord 42373 | For terms of the form of a power of omega times a non-zero natural number, ordering of the exponents implies ordering of the terms. Lemma 5.1 of [Schloeder] p. 15. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (πΆ β (Ο β 1o) β§ π· β (Ο β 1o))) β (π΄ β π΅ β ((Ο βo π΄) Β·o πΆ) β ((Ο βo π΅) Β·o π·))) | ||
Theorem | cantnfub 42374* | Given a finite number of terms of the form ((Ο βo (π΄βπ)) Β·o (πβπ)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (Ο βo π) when (π΄βπ) is less than π and (πβπ) is less than Ο. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 31-Jan-2025.) |
β’ (π β π β On) & β’ (π β π β Ο) & β’ (π β π΄:πβ1-1βπ) & β’ (π β π:πβΆΟ) & β’ πΉ = (π₯ β π β¦ if(π₯ β ran π΄, (πβ(β‘π΄βπ₯)), β )) β β’ (π β (πΉ β dom (Ο CNF π) β§ ((Ο CNF π)βπΉ) β (Ο βo π))) | ||
Theorem | cantnfub2 42375* | Given a finite number of terms of the form ((Ο βo (π΄βπ)) Β·o (πβπ)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (Ο βo suc βͺ ran π΄) when (πβπ) is less than Ο. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 9-Feb-2025.) |
β’ (π β π β Ο) & β’ (π β π΄:πβ1-1βOn) & β’ (π β π:πβΆΟ) & β’ πΉ = (π₯ β suc βͺ ran π΄ β¦ if(π₯ β ran π΄, (πβ(β‘π΄βπ₯)), β )) β β’ (π β (suc βͺ ran π΄ β On β§ πΉ β dom (Ο CNF suc βͺ ran π΄) β§ ((Ο CNF suc βͺ ran π΄)βπΉ) β (Ο βo suc βͺ ran π΄))) | ||
Theorem | bropabg 42376* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27520. (Contributed by RP, 26-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} β β’ (π΄π π΅ β ((π΄ β V β§ π΅ β V) β§ π)) | ||
Theorem | cantnfresb 42377* | A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025.) |
β’ (((π΄ β (On β 2o) β§ π΅ β On) β§ (πΆ β On β§ πΉ β dom (π΄ CNF π΅))) β (((π΄ CNF π΅)βπΉ) β (π΄ βo πΆ) β βπ₯ β (π΅ β πΆ)(πΉβπ₯) = β )) | ||
Theorem | cantnf2 42378* | For every ordinal, π΄, there is a an ordinal exponent π such that π΄ is less than (Ο βo π) and for every ordinal at least as large as π there is a unique Cantor normal form, π, with zeros for all the unnecessary higher terms, that sums to π΄. Theorem 5.3 of [Schloeder] p. 16. (Contributed by RP, 3-Feb-2025.) |
β’ (π΄ β On β βπ β On βπ β (On β π)β!π β dom (Ο CNF π)((π΄ β (Ο βo π) β§ π finSupp β ) β§ (((Ο CNF π)β(π βΎ π)) = π΄ β§ ((Ο CNF π)βπ) = π΄))) | ||
Theorem | oawordex2 42379* | If πΆ is between π΄ (inclusive) and (π΄ +o π΅) (exclusive), there is an ordinal which equals πΆ when summed to π΄. This is a slightly different statement than oawordex 8560 or oawordeu 8558. (Contributed by RP, 7-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (π΄ β πΆ β§ πΆ β (π΄ +o π΅))) β βπ₯ β π΅ (π΄ +o π₯) = πΆ) | ||
Theorem | nnawordexg 42380* | If an ordinal, π΅, is in a half-open interval between some π΄ and the next limit ordinal, π΅ is the sum of the π΄ and some natural number. This weakens the antecedent of nnawordex 8640. (Contributed by RP, 7-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π΅ β§ π΅ β (π΄ +o Ο)) β βπ₯ β Ο (π΄ +o π₯) = π΅) | ||
Theorem | succlg 42381 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
β’ ((π΄ β π΅ β§ (π΅ = β β¨ (π΅ = (Ο Β·o πΆ) β§ πΆ β (On β 1o)))) β suc π΄ β π΅) | ||
Theorem | dflim5 42382* | A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025.) |
β’ (Lim π΄ β (π΄ = On β¨ βπ₯ β (On β 1o)π΄ = (Ο Β·o π₯))) | ||
Theorem | oacl2g 42383 | Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo π·) β§ π· β On))) β (π΄ +o π΅) β πΆ) | ||
Theorem | onmcl 42384 | If an ordinal is less than a power of omega, the product with a natural number is also less than that power of omega. (Contributed by RP, 19-Feb-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π β Ο) β (π΄ β (Ο βo π΅) β (π΄ Β·o π) β (Ο βo π΅))) | ||
Theorem | omabs2 42385 | Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or Ο raised to some power of Ο. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β π΅ β§ β β π΄) β§ (π΅ = β β¨ π΅ = 2o β¨ (π΅ = (Ο βo (Ο βo πΆ)) β§ πΆ β On))) β (π΄ Β·o π΅) = π΅) | ||
Theorem | omcl2 42386 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | omcl3g 42387 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ β 3o β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | ordsssucb 42388 | An ordinal number is less than or equal to the successor of an ordinal class iff the ordinal number is either less than or equal to the ordinal class or the ordinal number is equal to the successor of the ordinal class. See also ordsssucim 42456, limsssuc 7842. (Contributed by RP, 22-Feb-2025.) |
β’ ((π΄ β On β§ Ord π΅) β (π΄ β suc π΅ β (π΄ β π΅ β¨ π΄ = suc π΅))) | ||
Theorem | tfsconcatlem 42389* | Lemma for tfsconcatun 42390. (Contributed by RP, 23-Feb-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β ((π΄ +o π΅) β π΄)) β β!π₯βπ¦ β π΅ (πΆ = (π΄ +o π¦) β§ π₯ = (πΉβπ¦))) | ||
Theorem | tfsconcatun 42390* | The concatenation of two transfinite series is a union of functions. (Contributed by RP, 23-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (π΄ + π΅) = (π΄ βͺ {β¨π₯, π¦β© β£ (π₯ β ((πΆ +o π·) β πΆ) β§ βπ§ β π· (π₯ = (πΆ +o π§) β§ π¦ = (π΅βπ§)))})) | ||
Theorem | tfsconcatfn 42391* | The concatenation of two transfinite series is a transfinite series. (Contributed by RP, 22-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (π΄ + π΅) Fn (πΆ +o π·)) | ||
Theorem | tfsconcatfv1 42392* | An early value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ ((((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β§ π β πΆ) β ((π΄ + π΅)βπ) = (π΄βπ)) | ||
Theorem | tfsconcatfv2 42393* | A latter value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ ((((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β§ π β π·) β ((π΄ + π΅)β(πΆ +o π)) = (π΅βπ)) | ||
Theorem | tfsconcatfv 42394* | The value of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ ((((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β§ π β (πΆ +o π·)) β ((π΄ + π΅)βπ) = if(π β πΆ, (π΄βπ), (π΅β(β©π β π· (πΆ +o π) = π)))) | ||
Theorem | tfsconcatrn 42395* | The range of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β ran (π΄ + π΅) = (ran π΄ βͺ ran π΅)) | ||
Theorem | tfsconcatfo 42396* | The concatenation of two transfinite series is onto the union of the ranges. (Contributed by RP, 24-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (π΄ + π΅):(πΆ +o π·)βontoβ(ran π΄ βͺ ran π΅)) | ||
Theorem | tfsconcatb0 42397* | The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 25-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (π΅ = β β (π΄ + π΅) = π΄)) | ||
Theorem | tfsconcat0i 42398* | The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (π΄ = β β (π΄ + π΅) = π΅)) | ||
Theorem | tfsconcat0b 42399* | The concatentation with the empty series leaves the finite series unchanged. (Contributed by RP, 1-Mar-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β Ο)) β (π΄ = β β (π΄ + π΅) = π΅)) | ||
Theorem | tfsconcat00 42400* | The concatentation of two empty series results in an empty series. (Contributed by RP, 25-Feb-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β ((π΄ = β β§ π΅ = β ) β (π΄ + π΅) = β )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |