Home | Metamath
Proof Explorer Theorem List (p. 415 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cytpval 41401* | 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 41402* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {β¨π, πβ© β£ ((π β π΄ β§ π β π΅) β§ (πΉβπ) = π)}) | ||
Theorem | fgraphxp 41403* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {π₯ β (π΄ Γ π΅) β£ (πΉβ(1st βπ₯)) = (2nd βπ₯)}) | ||
Theorem | hausgraph 41404 | 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 41405 | The class of separable topologies. |
class TopSep | ||
Syntax | ctoplnd 41406 | The class of LindelΓΆf topologies. |
class TopLnd | ||
Definition | df-topsep 41407* | 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 41408* | 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 41409 | Deductive form of r1sssuc 9652. (Contributed by Noam Pasman, 19-Jan-2025.) |
β’ (π β π΄ β On) β β’ (π β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | iocunico 41410 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | iocinico 41411 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) β© (π΅[,)πΆ)) = {π΅}) | ||
Theorem | iocmbl 41412 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β dom vol) | ||
Theorem | cnioobibld 41413* | 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 25127 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | arearect 41414 | 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 41415* | 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 | omlimcl2 41416 | 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 | oawordex2 41417* | If πΆ is between π΄ (inclusive) and (π΄ +o π΅) (exclusive), there is an ordinal which equals πΆ when summed to π΄. This is a slightly different statement than oawordex 8471 or oawordeu 8469. (Contributed by RP, 7-Jan-2025.) |
β’ (((π΄ β On β§ π΅ β On) β§ (π΄ β πΆ β§ πΆ β (π΄ +o π΅))) β βπ₯ β π΅ (π΄ +o π₯) = πΆ) | ||
Theorem | nnawordexg 41418* | 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 8551. (Contributed by RP, 7-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π΅ β§ π΅ β (π΄ +o Ο)) β βπ₯ β Ο (π΄ +o π₯) = π΅) | ||
Theorem | succlg 41419 | Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.) |
β’ ((π΄ β π΅ β§ (π΅ = β β¨ (π΅ = (Ο Β·o πΆ) β§ πΆ β (On β 1o)))) β suc π΄ β π΅) | ||
Theorem | dflim5 41420* | 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 41421 | 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 | omabs2 41422 | 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 41423 | Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ = β β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | omcl3g 41424 | Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.) |
β’ (((π΄ β πΆ β§ π΅ β πΆ) β§ (πΆ β 3o β¨ (πΆ = (Ο βo (Ο βo π·)) β§ π· β On))) β (π΄ Β·o π΅) β πΆ) | ||
Theorem | ofoafg 41425* | Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β π β§ πΆ = (π΄ β© π΅)) β§ (π· β On β§ πΈ β On β§ πΉ = βͺ π β π· (π +o πΈ))) β ( βf +o βΎ ((π· βm π΄) Γ (πΈ βm π΅))):((π· βm π΄) Γ (πΈ βm π΅))βΆ(πΉ βm πΆ)) | ||
Theorem | ofoaf 41426 | Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β π β§ πΆ = (π΄ β© π΅)) β§ (π· β On β§ πΈ = (Ο βo π·))) β ( βf +o βΎ ((πΈ βm π΄) Γ (πΈ βm π΅))):((πΈ βm π΄) Γ (πΈ βm π΅))βΆ(πΈ βm πΆ)) | ||
Theorem | ofoafo 41427 | Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025.) |
β’ ((π΄ β π β§ (π΅ β On β§ πΆ = (Ο βo π΅))) β ( βf +o βΎ ((πΆ βm π΄) Γ (πΆ βm π΄))):((πΆ βm π΄) Γ (πΆ βm π΄))βontoβ(πΆ βm π΄)) | ||
Theorem | ofoacl 41428 | Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ (π΅ β On β§ πΆ = (Ο βo π΅))) β§ (πΉ β (πΆ βm π΄) β§ πΊ β (πΆ βm π΄))) β (πΉ βf +o πΊ) β (πΆ βm π΄)) | ||
Theorem | ofoaid1 41429 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ πΉ β (π΅ βm π΄)) β (πΉ βf +o (π΄ Γ {β })) = πΉ) | ||
Theorem | ofoaid2 41430 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ πΉ β (π΅ βm π΄)) β ((π΄ Γ {β }) βf +o πΉ) = πΉ) | ||
Theorem | ofoaass 41431 | Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025.) |
β’ (((π΄ β π β§ π΅ β On) β§ (πΉ β (π΅ βm π΄) β§ πΊ β (π΅ βm π΄) β§ π» β (π΅ βm π΄))) β ((πΉ βf +o πΊ) βf +o π») = (πΉ βf +o (πΊ βf +o π»))) | ||
Theorem | ofoacom 41432 | Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.) |
β’ ((π΄ β π β§ (πΉ β (Ο βm π΄) β§ πΊ β (Ο βm π΄))) β (πΉ βf +o πΊ) = (πΊ βf +o πΉ)) | ||
Theorem | naddcnff 41433 | Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)):(π Γ π)βΆπ) | ||
Theorem | naddcnffn 41434 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)) Fn (π Γ π)) | ||
Theorem | naddcnffo 41435 | Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)):(π Γ π)βontoβπ) | ||
Theorem | naddcnfcl 41436 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π)) β (πΉ βf +o πΊ) β π) | ||
Theorem | naddcnfcom 41437 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π)) β (πΉ βf +o πΊ) = (πΊ βf +o πΉ)) | ||
Theorem | naddcnfid1 41438 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ πΉ β π) β (πΉ βf +o (π Γ {β })) = πΉ) | ||
Theorem | naddcnfid2 41439 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ πΉ β π) β ((π Γ {β }) βf +o πΉ) = πΉ) | ||
Theorem | naddcnfass 41440 | Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π β§ π» β π)) β ((πΉ βf +o πΊ) βf +o π») = (πΉ βf +o (πΊ βf +o π»))) | ||
Theorem | abeqabi 41441 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
β’ π΄ = {π₯ β£ π} β β’ ({π₯ β£ π} = π΄ β βπ₯(π β π)) | ||
Theorem | abpr 41442* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
β’ ({π₯ β£ π} = {π, π} β βπ₯(π β (π₯ = π β¨ π₯ = π))) | ||
Theorem | abtp 41443* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
β’ ({π₯ β£ π} = {π, π, π} β βπ₯(π β (π₯ = π β¨ π₯ = π β¨ π₯ = π))) | ||
Theorem | ralopabb 41444* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
β’ π = {β¨π₯, π¦β© β£ π} & β’ (π = β¨π₯, π¦β© β (π β π)) β β’ (βπ β π π β βπ₯βπ¦(π β π)) | ||
Theorem | bropabg 41445* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27047. (Contributed by RP, 26-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} β β’ (π΄π π΅ β ((π΄ β V β§ π΅ β V) β§ π)) | ||
Theorem | fpwfvss 41446 | Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024.) |
β’ πΉ:πΆβΆπ« π΅ β β’ (πΉβπ΄) β π΅ | ||
Theorem | sdomne0 41447 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
β’ (π΅ βΊ π΄ β π΄ β β ) | ||
Theorem | sdomne0d 41448 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
β’ (π β π΅ βΊ π΄) & β’ (π β π΅ β π) β β’ (π β π΄ β β ) | ||
Theorem | safesnsupfiss 41449 | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) β β’ (π β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅) β π΅) | ||
Theorem | safesnsupfiub 41450* | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) & β’ (π β βπ₯ β π΅ βπ¦ β πΆ π₯π π¦) β β’ (π β βπ₯ β if (π βΊ π΅, {sup(π΅, π΄, π )}, π΅)βπ¦ β πΆ π₯π π¦) | ||
Theorem | safesnsupfidom1o 41451 | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) β β’ (π β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅) βΌ 1o) | ||
Theorem | safesnsupfilb 41452* | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 3-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) β β’ (π β βπ₯ β (π΅ β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅))βπ¦ β if (π βΊ π΅, {sup(π΅, π΄, π )}, π΅)π₯π π¦) | ||
Theorem | isoeq145d 41453 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
β’ (π β πΉ = πΊ) & β’ (π β π΄ = πΆ) & β’ (π β π΅ = π·) β β’ (π β (πΉ Isom π , π (π΄, π΅) β πΊ Isom π , π (πΆ, π·))) | ||
Theorem | resisoeq45d 41454 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
β’ (π β π΄ = πΆ) & β’ (π β π΅ = π·) β β’ (π β ((πΉ βΎ π΄) Isom π , π (π΄, π΅) β (πΉ βΎ πΆ) Isom π , π (πΆ, π·))) | ||
Theorem | negslem1 41455 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
β’ (π΄ = π΅ β ((πΉ βΎ π΄) Isom π , β‘π (π΄, π΄) β (πΉ βΎ π΅) Isom π , β‘π (π΅, π΅))) | ||
Theorem | nvocnvb 41456* | Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024.) |
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (πΉ:π΄β1-1-ontoβπ΄ β§ βπ₯ β π΄ (πΉβ(πΉβπ₯)) = π₯)) | ||
Theorem | rp-brsslt 41457* | Binary relation form of a relation, <, which has been extended from relation π to subsets of class π. Usually, we will assume π Or π. Definition in [Alling], p. 2. Generalization of brsslt 27047. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} β β’ (π΄ < π΅ β ((π΄ β V β§ π΅ β V) β§ (π΄ β π β§ π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ π₯π π¦))) | ||
Theorem | nla0002 41458* | Extending a linear order to subsets, the empty set is less than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} & β’ (π β π΄ β V) & β’ (π β π΄ β π) β β’ (π β β < π΄) | ||
Theorem | nla0003 41459* | Extending a linear order to subsets, the empty set is greater than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} & β’ (π β π΄ β V) & β’ (π β π΄ β π) β β’ (π β π΄ < β ) | ||
Theorem | nla0001 41460* | Extending a linear order to subsets, the empty set is less than itself. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} β β’ (π β β < β ) | ||
Theorem | faosnf0.11b 41461* |
π΅
is called a non-limit ordinal if it is not a limit ordinal.
(Contributed by RP, 27-Sep-2023.)
Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243. |
β’ ((Ord π΄ β§ Β¬ Lim π΄ β§ π΄ β β ) β βπ₯ β On π΄ = suc π₯) | ||
Theorem | dfno2 41462 | A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.) |
β’ No = {π β π« (On Γ {1o, 2o}) β£ (Fun π β§ dom π β On)} | ||
Theorem | onnog 41463 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β {1o, 2o}) β (π΄ Γ {π΅}) β No ) | ||
Theorem | onnobdayg 41464 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β {1o, 2o}) β ( bday β(π΄ Γ {π΅})) = π΄) | ||
Theorem | bdaybndex 41465 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β No β§ π΅ = ( bday βπ΄) β§ πΆ β {1o, 2o}) β (π΅ Γ {πΆ}) β No ) | ||
Theorem | bdaybndbday 41466 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
β’ ((π΄ β No β§ π΅ = ( bday βπ΄) β§ πΆ β {1o, 2o}) β ( bday β(π΅ Γ {πΆ})) = ( bday βπ΄)) | ||
Theorem | onno 41467 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (π΄ β On β (π΄ Γ {2o}) β No ) | ||
Theorem | onnoi 41468 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ π΄ β On β β’ (π΄ Γ {2o}) β No | ||
Theorem | 0no 41469 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ β β No | ||
Theorem | 1no 41470 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (1o Γ {2o}) β No | ||
Theorem | 2no 41471 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (2o Γ {2o}) β No | ||
Theorem | 3no 41472 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (3o Γ {2o}) β No | ||
Theorem | 4no 41473 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (4o Γ {2o}) β No | ||
Theorem | fnimafnex 41474 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
β’ πΉ Fn π΅ β β’ (πΉ β (πΊβπ΄)) β V | ||
Theorem | nlimsuc 41475 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ (π΄ β On β Β¬ Lim suc π΄) | ||
Theorem | nlim1NEW 41476 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
β’ Β¬ Lim 1o | ||
Theorem | nlim2NEW 41477 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
β’ Β¬ Lim 2o | ||
Theorem | nlim3 41478 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ Β¬ Lim 3o | ||
Theorem | nlim4 41479 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ Β¬ Lim 4o | ||
Theorem | oa1un 41480 | Given π΄ β On, let π΄ +o 1o be defined to be the union of π΄ and {π΄}. Compare with oa1suc 8444. (Contributed by RP, 27-Sep-2023.) |
β’ (π΄ β On β (π΄ +o 1o) = (π΄ βͺ {π΄})) | ||
Theorem | oa1cl 41481 | π΄ +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
β’ (π΄ β On β (π΄ +o 1o) β On) | ||
Theorem | 0finon 41482 | 0 is a finite ordinal. See peano1 7815. (Contributed by RP, 27-Sep-2023.) |
β’ β β (On β© Fin) | ||
Theorem | 1finon 41483 | 1 is a finite ordinal. See 1onn 8553. (Contributed by RP, 27-Sep-2023.) |
β’ 1o β (On β© Fin) | ||
Theorem | 2finon 41484 | 2 is a finite ordinal. See 1onn 8553. (Contributed by RP, 27-Sep-2023.) |
β’ 2o β (On β© Fin) | ||
Theorem | 3finon 41485 | 3 is a finite ordinal. See 1onn 8553. (Contributed by RP, 27-Sep-2023.) |
β’ 3o β (On β© Fin) | ||
Theorem | 4finon 41486 | 4 is a finite ordinal. See 1onn 8553. (Contributed by RP, 27-Sep-2023.) |
β’ 4o β (On β© Fin) | ||
Theorem | finona1cl 41487 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
β’ (π β (On β© Fin) β (π +o 1o) β (On β© Fin)) | ||
Theorem | finonex 41488 | The finite ordinals are a set. See also onprc 7702 and fiprc 8922 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
β’ (On β© Fin) β V | ||
Theorem | fzunt 41489 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ (πΎ β€ π β§ π β€ π)) β ((πΎ...π) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzuntd 41490 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ π) β β’ (π β ((πΎ...π) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzunt1d 41491 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β πΏ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ πΏ) & β’ (π β πΏ β€ π) β β’ (π β ((πΎ...πΏ) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzuntgd 41492 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β πΏ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ (πΏ + 1)) & β’ (π β πΏ β€ π) β β’ (π β ((πΎ...πΏ) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | ifpan123g 41493 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
β’ ((if-(π, π, π) β§ if-(π, π, π)) β (((Β¬ π β¨ π) β§ (π β¨ π)) β§ ((Β¬ π β¨ π) β§ (π β¨ π)))) | ||
Theorem | ifpan23 41494 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
β’ ((if-(π, π, π) β§ if-(π, π, π)) β if-(π, (π β§ π), (π β§ π))) | ||
Theorem | ifpdfor2 41495 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β¨ π) β if-(π, π, π)) | ||
Theorem | ifporcor 41496 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
β’ (if-(π, π, π) β if-(π, π, π)) | ||
Theorem | ifpdfan2 41497 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
β’ ((π β§ π) β if-(π, π, π)) | ||
Theorem | ifpancor 41498 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, π, π) β if-(π, π, π)) | ||
Theorem | ifpdfor 41499 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β¨ π) β if-(π, β€, π)) | ||
Theorem | ifpdfan 41500 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β§ π) β if-(π, π, β₯)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |