![]() |
Metamath
Proof Explorer Theorem List (p. 421 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onepsuc 42001 | 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 42002 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7762 and weso 5668. (Contributed by RP, 15-Jan-2025.) |
β’ E Or On | ||
Theorem | epirron 42003 | 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 42004 | 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 42005 | 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 42006 | 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 42007 | 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 42008 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
β’ ((Ord π΄ β§ Ord π΅) β (πΆ β (π΄ β π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldifsucon 42009 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΅ β On) β (πΆ β (π΄ β suc π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldif1o 42010 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
β’ (Ord π΄ β (π΅ β (π΄ β 1o) β (π΅ β π΄ β§ π΅ β β ))) | ||
Theorem | ordne0gt0 42011 | 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 42012 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8501. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β (On β 1o) β β β π΄) | ||
Theorem | onsucelab 42013* | 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 42014* | 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 42015* | 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 42016 | 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 7806. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β On β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | ordnexbtwnsuc 42017* | 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 42018 | 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 42019* | 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 42020* | 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 42021* | 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 42022* | 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 42023* | 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 7837. (Contributed by RP, 17-Jan-2025.) |
β’ (Lim π΄ β (Ord π΄ β§ βπ β π΄ suc π β π΄ β§ π΄ β β )) | ||
Theorem | onov0suclim 42024 | 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 42025* | 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 8516, oasuc 8524, and oalim 8532. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ +o π΅) = π΄) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ +o π΅) = suc (π΄ +o πΆ)) β§ (Lim π΅ β (π΄ +o π΅) = βͺ π β π΅ (π΄ +o π)))) | ||
Theorem | om0suclim 42026* | 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 8517, omsuc 8526, and omlim 8533. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ Β·o π΅) = β ) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ Β·o π΅) = ((π΄ Β·o πΆ) +o π΄)) β§ (Lim π΅ β (π΄ Β·o π΅) = βͺ π β π΅ (π΄ Β·o π)))) | ||
Theorem | oe0suclim 42027* | 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 8522, oesuc 8527, oe0m1 8521, and oelim 8534. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ βo π΅) = 1o) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ βo π΅) = ((π΄ βo πΆ) Β·o π΄)) β§ (Lim π΅ β (π΄ βo π΅) = if(β β π΄, βͺ π β π΅ (π΄ βo π), β )))) | ||
Theorem | oaomoecl 42028 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8535, omcl 8536, oecl 8537. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +o π΅) β On β§ (π΄ Β·o π΅) β On β§ (π΄ βo π΅) β On)) | ||
Theorem | onsupsucismax 42029* | 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 42030* | 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 42031 | 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 42032* | 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 42033* | 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 42034 | Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8542 and om1r 8543 for individual statements. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β On β ((1o Β·o π΄) = (π΄ Β·o 1o) β§ (π΄ Β·o 1o) = π΄)) | ||
Theorem | oe0rif 42035 | 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 42036* | 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 42037 | Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8611, nnmcl 8612, nnecl 8613. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β ((π΄ +o π΅) β Ο β§ (π΄ Β·o π΅) β Ο β§ (π΄ βo π΅) β Ο)) | ||
Theorem | onsucwordi 42038 | 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 42039 | 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 42040 | 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 42041 | 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 42042 | 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 42043 | Ordinal one plus omega is equal to omega. See oaabs 8647 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 8648 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 42044 | 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 42045 | 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 42046* | 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 42047 | 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 8573. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ Β·o π΅)) | ||
Theorem | omge2 42048 | 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 8574. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΄ β β ) β π΅ β (π΄ Β·o π΅)) | ||
Theorem | omlim2 42049 | 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 42050 | 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 42051 | 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 42052 | 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 42053 | Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.) |
β’ (2o Β·o Ο) = Ο | ||
Theorem | omnord1ex 42054 | 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 42055* | 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 42056 | 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 8591. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ π΅ β β ) β π΄ β (π΄ βo π΅)) | ||
Theorem | oege2 42057 | 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 8593. (Contributed by RP, 29-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ π΅ β On) β π΅ β (π΄ βo π΅)) | ||
Theorem | rp-oelim2 42058 | 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 8600. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim π΅ β§ π΅ β π)) β Lim (π΄ βo π΅)) | ||
Theorem | oeord2lim 42059 | 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 8587. (Contributed by RP, 30-Jan-2025.) |
β’ (((π΄ β On β§ 1o β π΄) β§ (Lim πΆ β§ πΆ β π)) β (π΅ β πΆ β (π΄ βo π΅) β (π΄ βo πΆ))) | ||
Theorem | oeord2i 42060 | 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 42061 | 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 42062 | 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 42063 | Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , 1o, 2o} | ||
Theorem | df3o3 42064 | Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.) |
β’ 3o = {β , {β }, {β , {β }}} | ||
Theorem | oenord1ex 42065 | 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 42066* | 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 42067* | 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 42068 | 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 42069* | 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 42070 | 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 42071* | 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 42072* | 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 42073* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27287. (Contributed by RP, 26-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} β β’ (π΄π π΅ β ((π΄ β V β§ π΅ β V) β§ π)) | ||
Theorem | cantnfresb 42074* | 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 42075* | 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 42076* | If πΆ is between π΄ (inclusive) and (π΄ +o π΅) (exclusive), there is an ordinal which equals πΆ when summed to π΄. This is a slightly different statement than oawordex 8557 or oawordeu 8555. (Contributed by RP, 7-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (π΄ β πΆ β§ πΆ β (π΄ +o π΅))) β βπ₯ β π΅ (π΄ +o π₯) = πΆ) | ||
Theorem | nnawordexg 42077* | 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 8637. (Contributed by RP, 7-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π΅ β§ π΅ β (π΄ +o Ο)) β βπ₯ β Ο (π΄ +o π₯) = π΅) | ||
Theorem | succlg 42078 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
β’ ((π΄ β π΅ β§ (π΅ = β β¨ (π΅ = (Ο Β·o πΆ) β§ πΆ β (On β 1o)))) β suc π΄ β π΅) | ||
Theorem | dflim5 42079* | 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 42080 | 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 42081 | 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 42082 | 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 42083 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | omcl3g 42084 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ β 3o β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | ordsssucb 42085 | 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 42153, limsssuc 7839. (Contributed by RP, 22-Feb-2025.) |
β’ ((π΄ β On β§ Ord π΅) β (π΄ β suc π΅ β (π΄ β π΅ β¨ π΄ = suc π΅))) | ||
Theorem | tfsconcatlem 42086* | Lemma for tfsconcatun 42087. (Contributed by RP, 23-Feb-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β ((π΄ +o π΅) β π΄)) β β!π₯βπ¦ β π΅ (πΆ = (π΄ +o π¦) β§ π₯ = (πΉβπ¦))) | ||
Theorem | tfsconcatun 42087* | 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 42088* | 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 42089* | 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 42090* | 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 42091* | 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 42092* | 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 42093* | 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 42094* | 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 42095* | 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 42096* | 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 42097* | 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 42098* | 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 π£ = π·)) | ||
Theorem | tfsconcatrnss12 42099* | The range of the concatenation of transfinite sequences is a superset of the ranges of both sequences. Theorem 3 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 πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (ran π΄ β ran (π΄ + π΅) β§ ran π΅ β ran (π΄ + π΅))) | ||
Theorem | tfsconcatrnss 42100* | The concatenation of transfinite sequences yields elements from a class iff both sequences yield elements from that class. (Contributed by RP, 2-Mar-2025.) |
β’ + = (π β V, π β V β¦ (π βͺ {β¨π₯, π¦β© β£ (π₯ β ((dom π +o dom π) β dom π) β§ βπ§ β dom π(π₯ = (dom π +o π§) β§ π¦ = (πβπ§)))})) β β’ (((π΄ Fn πΆ β§ π΅ Fn π·) β§ (πΆ β On β§ π· β On)) β (ran (π΄ + π΅) β π β (ran π΄ β π β§ ran π΅ β π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |