![]() |
Metamath
Proof Explorer Theorem List (p. 274 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssltsn 27301 | Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β π΄ <s π΅) β β’ (π β {π΄} <<s {π΅}) | ||
Theorem | ssltsepc 27302 | Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ π β π΄ β§ π β π΅) β π <s π) | ||
Theorem | ssltsepcd 27303 | Two elements of separated sets obey less-than. Deduction form of ssltsepc 27302. (Contributed by Scott Fenton, 25-Sep-2024.) |
β’ (π β π΄ <<s π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) β β’ (π β π <s π) | ||
Theorem | sssslt1 27304 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ πΆ β π΄) β πΆ <<s π΅) | ||
Theorem | sssslt2 27305 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ πΆ β π΅) β π΄ <<s πΆ) | ||
Theorem | nulsslt 27306 | The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ β π« No β β <<s π΄) | ||
Theorem | nulssgt 27307 | The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ β π« No β π΄ <<s β ) | ||
Theorem | conway 27308* | Conway's Simplicity Theorem. Given π΄ preceeding π΅, there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from [Alling] p. 185. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β β!π₯ β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)} ( bday βπ₯) = β© ( bday β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)})) | ||
Theorem | scutval 27309* | The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β (π΄ |s π΅) = (β©π₯ β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)} ( bday βπ₯) = β© ( bday β {π¦ β No β£ (π΄ <<s {π¦} β§ {π¦} <<s π΅)}))) | ||
Theorem | scutcut 27310 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β ((π΄ |s π΅) β No β§ π΄ <<s {(π΄ |s π΅)} β§ {(π΄ |s π΅)} <<s π΅)) | ||
Theorem | scutcl 27311 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
β’ (π΄ <<s π΅ β (π΄ |s π΅) β No ) | ||
Theorem | scutcld 27312 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
β’ (π β π΄ <<s π΅) β β’ (π β (π΄ |s π΅) β No ) | ||
Theorem | scutbday 27313* | The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ (π΄ <<s π΅ β ( bday β(π΄ |s π΅)) = β© ( bday β {π₯ β No β£ (π΄ <<s {π₯} β§ {π₯} <<s π΅)})) | ||
Theorem | eqscut 27314* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((πΏ <<s π β§ π β No ) β ((πΏ |s π ) = π β (πΏ <<s {π} β§ {π} <<s π β§ ( bday βπ) = β© ( bday β {π¦ β No β£ (πΏ <<s {π¦} β§ {π¦} <<s π )})))) | ||
Theorem | eqscut2 27315* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((πΏ <<s π β§ π β No ) β ((πΏ |s π ) = π β (πΏ <<s {π} β§ {π} <<s π β§ βπ¦ β No ((πΏ <<s {π¦} β§ {π¦} <<s π ) β ( bday βπ) β ( bday βπ¦))))) | ||
Theorem | sslttr 27316 | Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ π΅ <<s πΆ β§ π΅ β β ) β π΄ <<s πΆ) | ||
Theorem | ssltun1 27317 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s πΆ β§ π΅ <<s πΆ) β (π΄ βͺ π΅) <<s πΆ) | ||
Theorem | ssltun2 27318 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ π΄ <<s πΆ) β π΄ <<s (π΅ βͺ πΆ)) | ||
Theorem | scutun12 27319 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ ((π΄ <<s π΅ β§ πΆ <<s {(π΄ |s π΅)} β§ {(π΄ |s π΅)} <<s π·) β ((π΄ βͺ πΆ) |s (π΅ βͺ π·)) = (π΄ |s π΅)) | ||
Theorem | dmscut 27320 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
β’ dom |s = <<s | ||
Theorem | scutf 27321 | Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
β’ |s : <<s βΆ No | ||
Theorem | etasslt 27322* | A restatement of noeta 27253 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ π β On β§ ( bday β (π΄ βͺ π΅)) β π) β βπ₯ β No (π΄ <<s {π₯} β§ {π₯} <<s π΅ β§ ( bday βπ₯) β π)) | ||
Theorem | etasslt2 27323* | A version of etasslt 27322 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.) |
β’ (π΄ <<s π΅ β βπ₯ β No (π΄ <<s {π₯} β§ {π₯} <<s π΅ β§ ( bday βπ₯) β suc βͺ ( bday β (π΄ βͺ π΅)))) | ||
Theorem | scutbdaybnd 27324 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ π β On β§ ( bday β (π΄ βͺ π΅)) β π) β ( bday β(π΄ |s π΅)) β π) | ||
Theorem | scutbdaybnd2 27325 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
β’ (π΄ <<s π΅ β ( bday β(π΄ |s π΅)) β suc βͺ ( bday β (π΄ βͺ π΅))) | ||
Theorem | scutbdaybnd2lim 27326 | An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ((π΄ <<s π΅ β§ Lim ( bday β(π΄ |s π΅))) β ( bday β(π΄ |s π΅)) β βͺ ( bday β (π΄ βͺ π΅))) | ||
Theorem | scutbdaylt 27327 | If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ ((π β No β§ (π΄ <<s {π} β§ {π} <<s π΅) β§ π β (π΄ |s π΅)) β ( bday β(π΄ |s π΅)) β ( bday βπ)) | ||
Theorem | slerec 27328* | A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ (((π΄ <<s π΅ β§ πΆ <<s π·) β§ (π = (π΄ |s π΅) β§ π = (πΆ |s π·))) β (π β€s π β (βπ β π· π <s π β§ βπ β π΄ π <s π))) | ||
Theorem | sltrec 27329* | A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.) |
β’ (((π΄ <<s π΅ β§ πΆ <<s π·) β§ (π = (π΄ |s π΅) β§ π = (πΆ |s π·))) β (π <s π β (βπ β πΆ π β€s π β¨ βπ β π΅ π β€s π))) | ||
Theorem | ssltdisj 27330 | If π΄ preceeds π΅, then π΄ and π΅ are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.) |
β’ (π΄ <<s π΅ β (π΄ β© π΅) = β ) | ||
Syntax | c0s 27331 | Declare the class syntax for surreal zero. |
class 0s | ||
Syntax | c1s 27332 | Declare the class syntax for surreal one. |
class 1s | ||
Definition | df-0s 27333 | Define surreal zero. This is the simplest cut of surreal number sets. Definition from [Conway] p. 17. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s = (β |s β ) | ||
Definition | df-1s 27334 | Define surreal one. This is the simplest number greater than surreal zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 1s = ({ 0s } |s β ) | ||
Theorem | 0sno 27335 | Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s β No | ||
Theorem | 1sno 27336 | Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 1s β No | ||
Theorem | bday0s 27337 | Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( bday β 0s ) = β | ||
Theorem | 0slt1s 27338 | Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ 0s <s 1s | ||
Theorem | bday0b 27339 | The only surreal with birthday β is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π β No β (( bday βπ) = β β π = 0s )) | ||
Theorem | bday1s 27340 | The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ( bday β 1s ) = 1o | ||
Theorem | cuteq0 27341 | Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.) |
β’ (π β π΄ <<s { 0s }) & β’ (π β { 0s } <<s π΅) β β’ (π β (π΄ |s π΅) = 0s ) | ||
Theorem | cuteq1 27342 | Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ (π β 0s β π΄) & β’ (π β π΄ <<s { 1s }) & β’ (π β { 1s } <<s π΅) β β’ (π β (π΄ |s π΅) = 1s ) | ||
Theorem | sgt0ne0 27343 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ ( 0s <s π΄ β π΄ β 0s ) | ||
Theorem | sgt0ne0d 27344 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
β’ (π β 0s <s π΄) β β’ (π β π΄ β 0s ) | ||
Syntax | cmade 27345 | Declare the symbol for the made by function. |
class M | ||
Syntax | cold 27346 | Declare the symbol for the older than function. |
class O | ||
Syntax | cnew 27347 | Declare the symbol for the new on function. |
class N | ||
Syntax | cleft 27348 | Declare the symbol for the left option function. |
class L | ||
Syntax | cright 27349 | Declare the symbol for the right option function. |
class R | ||
Definition | df-made 27350 | Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ M = recs((π β V β¦ ( |s β (π« βͺ ran π Γ π« βͺ ran π)))) | ||
Definition | df-old 27351 | Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ O = (π₯ β On β¦ βͺ ( M β π₯)) | ||
Definition | df-new 27352 | Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ N = (π₯ β On β¦ (( M βπ₯) β ( O βπ₯))) | ||
Definition | df-left 27353* | Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ L = (π₯ β No β¦ {π¦ β ( O β( bday βπ₯)) β£ π¦ <s π₯}) | ||
Definition | df-right 27354* | Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ R = (π₯ β No β¦ {π¦ β ( O β( bday βπ₯)) β£ π₯ <s π¦}) | ||
Theorem | madeval 27355 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ (π΄ β On β ( M βπ΄) = ( |s β (π« βͺ ( M β π΄) Γ π« βͺ ( M β π΄)))) | ||
Theorem | madeval2 27356* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
β’ (π΄ β On β ( M βπ΄) = {π₯ β No β£ βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯)}) | ||
Theorem | oldval 27357 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ (π΄ β On β ( O βπ΄) = βͺ ( M β π΄)) | ||
Theorem | newval 27358 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( N βπ΄) = (( M βπ΄) β ( O βπ΄)) | ||
Theorem | madef 27359 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ M :OnβΆπ« No | ||
Theorem | oldf 27360 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ O :OnβΆπ« No | ||
Theorem | newf 27361 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ N :OnβΆπ« No | ||
Theorem | old0 27362 | No surreal is older than β . (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( O ββ ) = β | ||
Theorem | madessno 27363 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( M βπ΄) β No | ||
Theorem | oldssno 27364 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( O βπ΄) β No | ||
Theorem | newssno 27365 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( N βπ΄) β No | ||
Theorem | leftval 27366* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π₯ <s π΄} | ||
Theorem | rightval 27367* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π΄ <s π₯} | ||
Theorem | leftf 27368 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ L : No βΆπ« No | ||
Theorem | rightf 27369 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ R : No βΆπ« No | ||
Theorem | elmade 27370* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
β’ (π΄ β On β (π β ( M βπ΄) β βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π))) | ||
Theorem | elmade2 27371* | Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β On β (π β ( M βπ΄) β βπ β π« ( O βπ΄)βπ β π« ( O βπ΄)(π <<s π β§ (π |s π) = π))) | ||
Theorem | elold 27372* | Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β On β (π β ( O βπ΄) β βπ β π΄ π β ( M βπ))) | ||
Theorem | ssltleft 27373 | A surreal is greater than its left options. Theorem 0(ii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β No β ( L βπ΄) <<s {π΄}) | ||
Theorem | ssltright 27374 | A surreal is less than its right options. Theorem 0(i) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (π΄ β No β {π΄} <<s ( R βπ΄)) | ||
Theorem | lltropt 27375 | The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) (Revised by Scott Fenton, 21-Feb-2025.) |
β’ ( L βπ΄) <<s ( R βπ΄) | ||
Theorem | made0 27376 | The only surreal made on day β is 0s. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ ( M ββ ) = { 0s } | ||
Theorem | new0 27377 | The only surreal new on day β is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ( N ββ ) = { 0s } | ||
Theorem | old1 27378 | The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( O β1o) = { 0s } | ||
Theorem | madess 27379 | If π΄ is less than or equal to ordinal π΅, then the made set of π΄ is included in the made set of π΅. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ((π΅ β On β§ π΄ β π΅) β ( M βπ΄) β ( M βπ΅)) | ||
Theorem | oldssmade 27380 | The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( O βπ΄) β ( M βπ΄) | ||
Theorem | leftssold 27381 | The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ) β ( O β( bday βπ)) | ||
Theorem | rightssold 27382 | The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ) β ( O β( bday βπ)) | ||
Theorem | leftssno 27383 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( L βπ΄) β No | ||
Theorem | rightssno 27384 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( R βπ΄) β No | ||
Theorem | madecut 27385 | Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024.) |
β’ (((π΄ β On β§ πΏ <<s π ) β§ (πΏ β ( O βπ΄) β§ π β ( O βπ΄))) β (πΏ |s π ) β ( M βπ΄)) | ||
Theorem | madeun 27386 | The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ ( M βπ΄) = (( O βπ΄) βͺ ( N βπ΄)) | ||
Theorem | madeoldsuc 27387 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π΄ β On β ( M βπ΄) = ( O βsuc π΄)) | ||
Theorem | oldsuc 27388 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ (π΄ β On β ( O βsuc π΄) = (( O βπ΄) βͺ ( N βπ΄))) | ||
Theorem | oldlim 27389 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
β’ ((Lim π΄ β§ π΄ β π) β ( O βπ΄) = βͺ ( O β π΄)) | ||
Theorem | madebdayim 27390 | If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ (π β ( M βπ΄) β ( bday βπ) β π΄) | ||
Theorem | oldbdayim 27391 | If π is in the old set for π΄, then the birthday of π is less than π΄. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ (π β ( O βπ΄) β ( bday βπ) β π΄) | ||
Theorem | oldirr 27392 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
β’ Β¬ π β ( O β( bday βπ)) | ||
Theorem | leftirr 27393 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ Β¬ π β ( L βπ) | ||
Theorem | rightirr 27394 | No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ Β¬ π β ( R βπ) | ||
Theorem | left0s 27395 | The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ( L β 0s ) = β | ||
Theorem | right0s 27396 | The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ( R β 0s ) = β | ||
Theorem | left1s 27397 | The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( L β 1s ) = { 0s } | ||
Theorem | right1s 27398 | The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.) |
β’ ( R β 1s ) = β | ||
Theorem | lrold 27399 | The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ (( L βπ΄) βͺ ( R βπ΄)) = ( O β( bday βπ΄)) | ||
Theorem | madebdaylemold 27400* | Lemma for madebday 27402. If the inductive hypothesis of madebday 27402 is satisfied, the converse of oldbdayim 27391 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ ((π΄ β On β§ βπ β π΄ βπ¦ β No (( bday βπ¦) β π β π¦ β ( M βπ)) β§ π β No ) β (( bday βπ) β π΄ β π β ( O βπ΄))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |