![]() |
Metamath
Proof Explorer Theorem List (p. 418 of 475) | < 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-30034) |
![]() (30035-31557) |
![]() (31558-47498) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mendvscafval 41701* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) β β’ ( Β·π βπ΄) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) | ||
Theorem | mendvsca 41702 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) & β’ β = ( Β·π βπ΄) β β’ ((π β πΎ β§ π β π΅) β (π β π) = ((πΈ Γ {π}) βf Β· π)) | ||
Theorem | mendring 41703 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π β LMod β π΄ β Ring) | ||
Theorem | mendlmod 41704 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β LMod) | ||
Theorem | mendassa 41705 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β AssAlg) | ||
Theorem | idomrootle 41706* | No element of an integral domain can have more than π π-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (.gβ(mulGrpβπ )) β β’ ((π β IDomn β§ π β π΅ β§ π β β) β (β―β{π¦ β π΅ β£ (π β π¦) = π}) β€ π) | ||
Theorem | idomodle 41707* | Limit on the number of π-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β) β (β―β{π₯ β π΅ β£ (πβπ₯) β₯ π}) β€ π) | ||
Theorem | fiuneneq 41708 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π΄ β π΅ β§ π΄ β Fin) β ((π΄ βͺ π΅) β π΄ β π΄ = π΅)) | ||
Theorem | idomsubgmo 41709* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) β β’ ((π β IDomn β§ π β β) β β*π¦ β (SubGrpβπΊ)(β―βπ¦) = π) | ||
Theorem | proot1mul 41710 | Any primitive π-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (((π β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) | ||
Theorem | proot1hash 41711 | If an integral domain has a primitive π-th root of unity, it has exactly (Οβπ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β β§ π β (β‘π β {π})) β (β―β(β‘π β {π})) = (Οβπ)) | ||
Theorem | proot1ex 41712 | The complex field has primitive π-th roots of unity for all π. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπΊ) β β’ (π β β β (-1βπ(2 / π)) β (β‘π β {π})) | ||
Syntax | ccytp 41713 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 41714* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP = (π β β β¦ ((mulGrpβ(Poly1ββfld)) Ξ£g (π β (β‘(odβ((mulGrpββfld) βΎs (β β {0}))) β {π}) β¦ ((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) | ||
Theorem | isdomn3 41715 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (mulGrpβπ ) β β’ (π β Domn β (π β Ring β§ (π΅ β { 0 }) β (SubMndβπ))) | ||
Theorem | mon1pid 41716 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ 1 = (1rβπ) & β’ π = (Monic1pβπ ) & β’ π· = ( deg1 βπ ) β β’ (π β NzRing β ( 1 β π β§ (π·β 1 ) = 0)) | ||
Theorem | mon1psubm 41717 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ π = (Monic1pβπ ) & β’ π = (mulGrpβπ) β β’ (π β NzRing β π β (SubMndβπ)) | ||
Theorem | deg1mhm 41718 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = ((mulGrpβπ) βΎs (π΅ β { 0 })) & β’ π = (βfld βΎs β0) β β’ (π β Domn β (π· βΎ (π΅ β { 0 })) β (π MndHom π)) | ||
Theorem | cytpfn 41719 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP Fn β | ||
Theorem | cytpval 41720* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπ) & β’ π = (Poly1ββfld) & β’ π = (var1ββfld) & β’ π = (mulGrpβπ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) β β’ (π β β β (CytPβπ) = (π Ξ£g (π β (β‘π β {π}) β¦ (π β (π΄βπ))))) | ||
Theorem | fgraphopab 41721* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {β¨π, πβ© β£ ((π β π΄ β§ π β π΅) β§ (πΉβπ) = π)}) | ||
Theorem | fgraphxp 41722* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {π₯ β (π΄ Γ π΅) β£ (πΉβ(1st βπ₯)) = (2nd βπ₯)}) | ||
Theorem | hausgraph 41723 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ β (Clsdβ(π½ Γt πΎ))) | ||
Syntax | ctopsep 41724 | The class of separable topologies. |
class TopSep | ||
Syntax | ctoplnd 41725 | The class of LindelΓΆf topologies. |
class TopLnd | ||
Definition | df-topsep 41726* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopSep = {π β Top β£ βπ₯ β π« βͺ π(π₯ βΌ Ο β§ ((clsβπ)βπ₯) = βͺ π)} | ||
Definition | df-toplnd 41727* | A topology is LindelΓΆf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopLnd = {π₯ β Top β£ βπ¦ β π« π₯(βͺ π₯ = βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ = βͺ π§))} | ||
Theorem | r1sssucd 41728 | Deductive form of r1sssuc 9760. (Contributed by Noam Pasman, 19-Jan-2025.) |
β’ (π β π΄ β On) β β’ (π β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | iocunico 41729 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | iocinico 41730 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) β© (π΅[,)πΆ)) = {π΅}) | ||
Theorem | iocmbl 41731 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β dom vol) | ||
Theorem | cnioobibld 41732* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider πΉ = (π₯ β (0(,)1) β¦ (1 / π₯)). See cniccibl 25287 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | arearect 41733 | The area of a rectangle whose sides are parallel to the coordinate axes in (β Γ β) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ π΄ β€ π΅ & β’ πΆ β€ π· & β’ π = ((π΄[,]π΅) Γ (πΆ[,]π·)) β β’ (areaβπ) = ((π΅ β π΄) Β· (π· β πΆ)) | ||
Theorem | areaquad 41734* | The area of a quadrilateral with two sides which are parallel to the y-axis in (β Γ β) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ πΈ β β & β’ πΉ β β & β’ π΄ < π΅ & β’ πΆ β€ πΈ & β’ π· β€ πΉ & β’ π = (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) & β’ π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) & β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} β β’ (areaβπ) = ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) | ||
Theorem | uniel 41735* | Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΅ β βπ₯ β π΅ βπ§(π§ β π₯ β βπ¦ β π΄ π§ β π¦)) | ||
Theorem | unielss 41736* | Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β π΅ β (βͺ π΅ β π΄ β βπ₯ β π΄ βπ¦ β π΅ π¦ β π₯)) | ||
Theorem | unielid 41737* | Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΄ β βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯) | ||
Theorem | ssunib 41738* | Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β βͺ π΅ β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) | ||
Theorem | rp-intrabeq 41739* | Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} = β© {π₯ β On β£ βπ¦ β π΅ π¦ β π₯}) | ||
Theorem | rp-unirabeq 41740* | Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} = βͺ {π₯ β On β£ βπ¦ β π΅ π₯ β π¦}) | ||
Theorem | onmaxnelsup 41741* | Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (Β¬ π΄ β βͺ π΄ β βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯)) | ||
Theorem | onsupneqmaxlim0 41742 | If the supremum of a class of ordinals is not in that class, then the supremum is a limit ordinal or empty. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (π΄ β βͺ π΄ β βͺ π΄ = βͺ βͺ π΄)) | ||
Theorem | onsupcl2 41743 | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β βͺ π΄ β On) | ||
Theorem | onuniintrab 41744* | The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Closed form of uniordint 7772. (Contributed by RP, 28-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β βͺ π΄ = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onintunirab 41745* | The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β β© π΄ = βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦}) | ||
Theorem | onsupnmax 41746 | If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since π΄ could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (Β¬ βͺ π΄ β π΄ β βͺ π΄ = βͺ βͺ π΄)) | ||
Theorem | onsupuni 41747 | The supremum of a set of ordinals is the union of that set. Lemma 2.10 of [Schloeder] p. 5. (Contributed by RP, 19-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β sup(π΄, On, E ) = βͺ π΄) | ||
Theorem | onsupuni2 41748 | The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025.) |
β’ (π΄ β π« On β sup(π΄, On, E ) = βͺ π΄) | ||
Theorem | onsupintrab 41749* | The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Definition 2.9 of [Schloeder] p. 5. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β sup(π΄, On, E ) = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onsupintrab2 41750* | The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β sup(π΄, On, E ) = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onsupcl3 41751* | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β On) | ||
Theorem | onsupex3 41752* | The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β V) | ||
Theorem | onuniintrab2 41753* | The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β βͺ π΄ = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | oninfint 41754 | The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β inf(π΄, On, E ) = β© π΄) | ||
Theorem | oninfunirab 41755* | The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β inf(π΄, On, E ) = βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦}) | ||
Theorem | oninfcl2 41756* | The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β On) | ||
Theorem | onsupmaxb 41757 | The union of a class of ordinals is an element is an element of that class if and only if there is a maximum element of that class under the epsilon relation, which is to say that the domain of the restricted epsilon relation is not the whole class. (Contributed by RP, 25-Jan-2025.) |
β’ (π΄ β On β (dom ( E β© (π΄ Γ π΄)) = π΄ β Β¬ βͺ π΄ β π΄)) | ||
Theorem | onexgt 41758* | For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β π₯) | ||
Theorem | onexomgt 41759* | For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο Β·o π₯)) | ||
Theorem | omlimcl2 41760 | The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.) |
β’ (((π΄ β On β§ (π΅ β πΆ β§ Lim π΅)) β§ β β π΄) β Lim (π΅ Β·o π΄)) | ||
Theorem | onexlimgt 41761* | For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On (Lim π₯ β§ π΄ β π₯)) | ||
Theorem | onexoegt 41762* | For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο βo π₯)) | ||
Theorem | oninfex2 41763* | The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β V) | ||
Theorem | onsupeqmax 41764* | Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β (βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯ β βͺ π΄ β π΄)) | ||
Theorem | onsupeqnmax 41765* | Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (βπ₯ β π΄ βπ¦ β π΄ π₯ β π¦ β (βͺ π΄ = βͺ βͺ π΄ β§ Β¬ βͺ π΄ β π΄))) | ||
Theorem | onsuplub 41766* | The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ π΅ β On) β (π΅ β βͺ π΄ β βπ§ β π΄ π΅ β π§)) | ||
Theorem | onsupnub 41767* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ (π΅ β On β§ βπ§ β π΄ π§ β π΅)) β βͺ π΄ β π΅) | ||
Theorem | onfisupcl 41768 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9276. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β ((π΄ β Fin β§ π΄ β β ) β βͺ π΄ β π΄)) | ||
Theorem | onelord 41769 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6378 and eloni 6363. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β π΄) β Ord π΅) | ||
Theorem | onepsuc 41770 | 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 41771 | The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7745 and weso 5660. (Contributed by RP, 15-Jan-2025.) |
β’ E Or On | ||
Theorem | epirron 41772 | 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 41773 | 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 41774 | The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6399. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ)) | ||
Theorem | oneptri 41775 | 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 41776 | The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6385. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅ β¨ π΅ β π΄ β¨ π΄ = π΅)) | ||
Theorem | ordeldif 41777 | Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.) |
β’ ((Ord π΄ β§ Ord π΅) β (πΆ β (π΄ β π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldifsucon 41778 | Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΅ β On) β (πΆ β (π΄ β suc π΅) β (πΆ β π΄ β§ π΅ β πΆ))) | ||
Theorem | ordeldif1o 41779 | Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.) |
β’ (Ord π΄ β (π΅ β (π΄ β 1o) β (π΅ β π΄ β§ π΅ β β ))) | ||
Theorem | ordne0gt0 41780 | Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6408. (Contributed by RP, 16-Jan-2025.) |
β’ ((Ord π΄ β§ π΄ β β ) β β β π΄) | ||
Theorem | ondif1i 41781 | Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8483. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β (On β 1o) β β β π΄) | ||
Theorem | onsucelab 41782* | 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 41783* | 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 41784* | 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 41785 | 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 7789. (Contributed by RP, 16-Jan-2025.) |
β’ (π΄ β On β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | ordnexbtwnsuc 41786* | 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 41787 | 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 41788* | 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 41789* | 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 41790* | 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 41791* | 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 41792* | 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 7820. (Contributed by RP, 17-Jan-2025.) |
β’ (Lim π΄ β (Ord π΄ β§ βπ β π΄ suc π β π΄ β§ π΄ β β )) | ||
Theorem | onov0suclim 41793 | 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 41794* | 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 8498, oasuc 8506, and oalim 8514. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ +o π΅) = π΄) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ +o π΅) = suc (π΄ +o πΆ)) β§ (Lim π΅ β (π΄ +o π΅) = βͺ π β π΅ (π΄ +o π)))) | ||
Theorem | om0suclim 41795* | 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 8499, omsuc 8508, and omlim 8515. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ Β·o π΅) = β ) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ Β·o π΅) = ((π΄ Β·o πΆ) +o π΄)) β§ (Lim π΅ β (π΄ Β·o π΅) = βͺ π β π΅ (π΄ Β·o π)))) | ||
Theorem | oe0suclim 41796* | 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 8504, oesuc 8509, oe0m1 8503, and oelim 8516. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΅ = β β (π΄ βo π΅) = 1o) β§ ((π΅ = suc πΆ β§ πΆ β On) β (π΄ βo π΅) = ((π΄ βo πΆ) Β·o π΄)) β§ (Lim π΅ β (π΄ βo π΅) = if(β β π΄, βͺ π β π΅ (π΄ βo π), β )))) | ||
Theorem | oaomoecl 41797 | The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8517, omcl 8518, oecl 8519. (Contributed by RP, 18-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +o π΅) β On β§ (π΄ Β·o π΅) β On β§ (π΄ βo π΅) β On)) | ||
Theorem | onsupsucismax 41798* | 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 41799* | 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 41800 | 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 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |