![]() |
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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onfisupcl 42301 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9295. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β ((π΄ β Fin β§ π΄ β β ) β βͺ π΄ β π΄)) | ||
Theorem | onelord 42302 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6388 and eloni 6373. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β π΄) β Ord π΅) | ||
Theorem | onepsuc 42303 | 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 42304 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7764 and weso 5666. (Contributed by RP, 15-Jan-2025.) |
β’ E Or On | ||
Theorem | epirron 42305 | 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 42306 | 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 42307 | The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6409. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ)) | ||
Theorem | oneptri 42308 | 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 42309 | The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6395. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅ β¨ π΅ β π΄ β¨ π΄ = π΅)) | ||
Theorem | ordeldif 42310 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
β’ ((Ord π΄ β§ Ord π΅) β (πΆ β (π΄ β π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldifsucon 42311 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΅ β On) β (πΆ β (π΄ β suc π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldif1o 42312 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
β’ (Ord π΄ β (π΅ β (π΄ β 1o) β (π΅ β π΄ β§ π΅ β β ))) | ||
Theorem | ordne0gt0 42313 | Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6418. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΄ β β ) β β β π΄) | ||
Theorem | ondif1i 42314 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8503. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β (On β 1o) β β β π΄) | ||
Theorem | onsucelab 42315* | 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 42316* | 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 42317* | 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 42318 | 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 7808. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β On β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | ordnexbtwnsuc 42319* | 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 42320 | 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 42321* | 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 42322* | 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 42323* | 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 42324* | 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 42325* | 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 7839. (Contributed by RP, 17-Jan-2025.) |
β’ (Lim π΄ β (Ord π΄ β§ βπ β π΄ suc π β π΄ β§ π΄ β β )) | ||
Theorem | onov0suclim 42326 | 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 42327* | 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 8518, oasuc 8526, and oalim 8534. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ +o π΅) = π΄) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ +o π΅) = suc (π΄ +o πΆ)) β§ (Lim π΅ β (π΄ +o π΅) = βͺ π β π΅ (π΄ +o π)))) | ||
Theorem | om0suclim 42328* | 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 8519, omsuc 8528, and omlim 8535. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ Β·o π΅) = β ) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ Β·o π΅) = ((π΄ Β·o πΆ) +o π΄)) β§ (Lim π΅ β (π΄ Β·o π΅) = βͺ π β π΅ (π΄ Β·o π)))) | ||
Theorem | oe0suclim 42329* | 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 8524, oesuc 8529, oe0m1 8523, and oelim 8536. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ βo π΅) = 1o) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ βo π΅) = ((π΄ βo πΆ) Β·o π΄)) β§ (Lim π΅ β (π΄ βo π΅) = if(β β π΄, βͺ π β π΅ (π΄ βo π), β )))) | ||
Theorem | oaomoecl 42330 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8537, omcl 8538, oecl 8539. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +o π΅) β On β§ (π΄ Β·o π΅) β On β§ (π΄ βo π΅) β On)) | ||
Theorem | onsupsucismax 42331* | 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 42332* | 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 42333 | 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 42334* | A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6424. (Contributed by RP, 27-Jan-2025.) |
β’ (Lim π΄ β π΄ = βͺ π₯ β π΄ π₯) | ||
Theorem | limexissupab 42335* | 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 42336 | Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8544 and om1r 8545 for individual statements. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β On β ((1o Β·o π΄) = (π΄ Β·o 1o) β§ (π΄ Β·o 1o) = π΄)) | ||
Theorem | oe0rif 42337 | 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 42338* | 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 42339 | Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8613, nnmcl 8614, nnecl 8615. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β ((π΄ +o π΅) β Ο β§ (π΄ Β·o π΅) β Ο β§ (π΄ βo π΅) β Ο)) | ||
Theorem | onsucwordi 42340 | 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 42341 | 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 42342 | 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 42343 | 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 42344 | 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 42345 | Ordinal one plus omega is equal to omega. See oaabs 8649 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 8650 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 42346 | 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 42347 | 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 42348* | 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 42349 | 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 8575. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ Β·o π΅)) | ||
Theorem | omge2 42350 | 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 8576. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΄ β β ) β π΅ β (π΄ Β·o π΅)) | ||
Theorem | omlim2 42351 | 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 42352 | 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 42353 | 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 42354 | 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 42355 | Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.) |
β’ (2o Β·o Ο) = Ο | ||
Theorem | omnord1ex 42356 | 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 42357* | 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 42358 | 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 8593. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ βo π΅)) | ||
Theorem | oege2 42359 | 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 8595. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ π΅ β On) β π΅ β (π΄ βo π΅)) | ||
Theorem | rp-oelim2 42360 | 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 8602. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim π΅ β§ π΅ β π)) β Lim (π΄ βo π΅)) | ||
Theorem | oeord2lim 42361 | 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 8589. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim πΆ β§ πΆ β π)) β (π΅ β πΆ β (π΄ βo π΅) β (π΄ βo πΆ))) | ||
Theorem | oeord2i 42362 | 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 42363 | 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 42364 | 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 42365 | Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , 1o, 2o} | ||
Theorem | df3o3 42366 | Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , {β }, {β , {β }}} | ||
Theorem | oenord1ex 42367 | 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 42368* | 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 42369* | 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 42370 | 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 42371* | 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 42372 | 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 42373* | 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 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 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 42375* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27523. (Contributed by RP, 26-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} β β’ (π΄π π΅ β ((π΄ β V β§ π΅ β V) β§ π)) | ||
Theorem | cantnfresb 42376* | 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 42377* | 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 42378* | If πΆ is between π΄ (inclusive) and (π΄ +o π΅) (exclusive), there is an ordinal which equals πΆ when summed to π΄. This is a slightly different statement than oawordex 8559 or oawordeu 8557. (Contributed by RP, 7-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (π΄ β πΆ β§ πΆ β (π΄ +o π΅))) β βπ₯ β π΅ (π΄ +o π₯) = πΆ) | ||
Theorem | nnawordexg 42379* | 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 8639. (Contributed by RP, 7-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π΅ β§ π΅ β (π΄ +o Ο)) β βπ₯ β Ο (π΄ +o π₯) = π΅) | ||
Theorem | succlg 42380 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
β’ ((π΄ β π΅ β§ (π΅ = β β¨ (π΅ = (Ο Β·o πΆ) β§ πΆ β (On β 1o)))) β suc π΄ β π΅) | ||
Theorem | dflim5 42381* | 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 42382 | 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 42383 | 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 42384 | 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 42385 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | omcl3g 42386 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ β 3o β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | ordsssucb 42387 | 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 42455, limsssuc 7841. (Contributed by RP, 22-Feb-2025.) |
β’ ((π΄ β On β§ Ord π΅) β (π΄ β suc π΅ β (π΄ β π΅ β¨ π΄ = suc π΅))) | ||
Theorem | tfsconcatlem 42388* | Lemma for tfsconcatun 42389. (Contributed by RP, 23-Feb-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β ((π΄ +o π΅) β π΄)) β β!π₯βπ¦ β π΅ (πΆ = (π΄ +o π¦) β§ π₯ = (πΉβπ¦))) | ||
Theorem | tfsconcatun 42389* | 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 42390* | 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 42391* | 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 42392* | 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 42393* | 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 42394* | 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 42395* | 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 42396* | 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 42397* | 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 42398* | 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 42399* | 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)) β ((π΄ = β β§ π΅ = β ) β (π΄ + π΅) = β )) | ||
Theorem | tfsconcatrev 42400* | If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249β256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ ((πΉ Fn (πΆ +o π·) β§ (πΆ β On β§ π· β On)) β βπ’ β (ran πΉ βm πΆ)βπ£ β (ran πΉ βm π·)((π’ + π£) = πΉ β§ dom π’ = πΆ β§ dom π£ = π·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |