![]() |
Metamath
Proof Explorer Theorem List (p. 422 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 | tfsconcatrnsson 42101* | The concatenation of transfinite sequences yields ordinals iff both sequences yield ordinals. Theorem 4 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 (๐ด + ๐ต) โ On โ (ran ๐ด โ On โง ran ๐ต โ On))) | ||
Theorem | tfsnfin 42102 | A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 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, 1-Mar-2025.) |
โข ((๐ด Fn ๐ต โง ๐ต โ On) โ (ยฌ ๐ด โ Fin โ ฯ โ ๐ต)) | ||
Theorem | rp-tfslim 42103* | The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.) |
โข (๐ด Fn ๐ต โ โช ๐ฅ โ ๐ต (๐ดโ๐ฅ) = โช ran ๐ด) | ||
Theorem | ofoafg 42104* | 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 42105 | 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 42106 | 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 42107 | 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 42108 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
โข (((๐ด โ ๐ โง ๐ต โ On) โง ๐น โ (๐ต โm ๐ด)) โ (๐น โf +o (๐ด ร {โ })) = ๐น) | ||
Theorem | ofoaid2 42109 | Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.) |
โข (((๐ด โ ๐ โง ๐ต โ On) โง ๐น โ (๐ต โm ๐ด)) โ ((๐ด ร {โ }) โf +o ๐น) = ๐น) | ||
Theorem | ofoaass 42110 | 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 42111 | Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.) |
โข ((๐ด โ ๐ โง (๐น โ (ฯ โm ๐ด) โง ๐บ โ (ฯ โm ๐ด))) โ (๐น โf +o ๐บ) = (๐บ โf +o ๐น)) | ||
Theorem | naddcnff 42112 | 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 42113 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
โข ((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โ ( โf +o โพ (๐ ร ๐)) Fn (๐ ร ๐)) | ||
Theorem | naddcnffo 42114 | 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 42115 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น โf +o ๐บ) โ ๐) | ||
Theorem | naddcnfcom 42116 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น โf +o ๐บ) = (๐บ โf +o ๐น)) | ||
Theorem | naddcnfid1 42117 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง ๐น โ ๐) โ (๐น โf +o (๐ ร {โ })) = ๐น) | ||
Theorem | naddcnfid2 42118 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง ๐น โ ๐) โ ((๐ ร {โ }) โf +o ๐น) = ๐น) | ||
Theorem | naddcnfass 42119 | 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 | onsucunifi 42120* | The successor to the union of any non-empty, finite subset of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
โข ((๐ด โ On โง ๐ด โ Fin โง ๐ด โ โ ) โ suc โช ๐ด = โช ๐ฅ โ ๐ด suc ๐ฅ) | ||
Theorem | sucunisn 42121 | The successor to the union of any singleton of a set is the successor of the set. (Contributed by RP, 11-Feb-2025.) |
โข (๐ด โ ๐ โ suc โช {๐ด} = suc ๐ด) | ||
Theorem | onsucunipr 42122 | The successor to the union of any pair of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ suc โช {๐ด, ๐ต} = โช {suc ๐ด, suc ๐ต}) | ||
Theorem | onsucunitp 42123 | The successor to the union of any triple of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ suc โช {๐ด, ๐ต, ๐ถ} = โช {suc ๐ด, suc ๐ต, suc ๐ถ}) | ||
Theorem | oaun3lem1 42124* | The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 42132. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ Ord {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)}) | ||
Theorem | oaun3lem2 42125* | The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 42132. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ (๐ด +o ๐ต)) | ||
Theorem | oaun3lem3 42126* | The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 42132. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ On) | ||
Theorem | oaun3lem4 42127* | The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 42132. (Contributed by RP, 12-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ suc (๐ด +o ๐ต)) | ||
Theorem | rp-abid 42128* | Two ways to express a class. (Contributed by RP, 13-Feb-2025.) |
โข ๐ด = {๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐} | ||
Theorem | oadif1lem 42129* | Express the set difference of a continuous sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โ ๐ต) โ On) & โข ((๐ด โ On โง ๐ โ On) โ (๐ด โ ๐) โ On) & โข (((๐ด โ On โง ๐ต โ On) โง (๐ด โ ๐ฆ โง ๐ฆ โ (๐ด โ ๐ต))) โ โ๐ โ ๐ต (๐ด โ ๐) = ๐ฆ) & โข ((๐ด โ On โง ๐ต โ On) โ (๐ โ ๐ต โ (๐ด โ ๐) โ (๐ด โ ๐ต))) & โข ((๐ด โ On โง ๐ โ On) โ ๐ด โ (๐ด โ ๐)) โ โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ ๐ต) โ ๐ด) = {๐ฅ โฃ โ๐ โ ๐ต ๐ฅ = (๐ด โ ๐)}) | ||
Theorem | oadif1 42130* | Express the set difference of an ordinal sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด +o ๐ต) โ ๐ด) = {๐ฅ โฃ โ๐ โ ๐ต ๐ฅ = (๐ด +o ๐)}) | ||
Theorem | oaun2 42131* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +o ๐ต) = โช {{๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐}, {๐ฆ โฃ โ๐ โ ๐ต ๐ฆ = (๐ด +o ๐)}}) | ||
Theorem | oaun3 42132* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +o ๐ต) = โช {{๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐}, {๐ฆ โฃ โ๐ โ ๐ต ๐ฆ = (๐ด +o ๐)}, {๐ง โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ +o ๐)}}) | ||
Theorem | naddov4 42133* | Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +no ๐ต) = โฉ ({๐ฅ โ On โฃ โ๐ โ ๐ด (๐ +no ๐ต) โ ๐ฅ} โฉ {๐ฅ โ On โฃ โ๐ โ ๐ต (๐ด +no ๐) โ ๐ฅ})) | ||
Theorem | nadd2rabtr 42134* | The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ Tr {๐ฅ โ ๐ด โฃ (๐ต +no ๐ฅ) โ ๐ถ}) | ||
Theorem | nadd2rabord 42135* | The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ Ord {๐ฅ โ ๐ด โฃ (๐ต +no ๐ฅ) โ ๐ถ}) | ||
Theorem | nadd2rabex 42136* | The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ {๐ฅ โ ๐ด โฃ (๐ต +no ๐ฅ) โ ๐ถ} โ V) | ||
Theorem | nadd2rabon 42137* | The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ {๐ฅ โ ๐ด โฃ (๐ต +no ๐ฅ) โ ๐ถ} โ On) | ||
Theorem | nadd1rabtr 42138* | The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ Tr {๐ฅ โ ๐ด โฃ (๐ฅ +no ๐ต) โ ๐ถ}) | ||
Theorem | nadd1rabord 42139* | The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ Ord {๐ฅ โ ๐ด โฃ (๐ฅ +no ๐ต) โ ๐ถ}) | ||
Theorem | nadd1rabex 42140* | The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ {๐ฅ โ ๐ด โฃ (๐ฅ +no ๐ต) โ ๐ถ} โ V) | ||
Theorem | nadd1rabon 42141* | The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.) |
โข ((Ord ๐ด โง ๐ต โ On โง ๐ถ โ On) โ {๐ฅ โ ๐ด โฃ (๐ฅ +no ๐ต) โ ๐ถ} โ On) | ||
Theorem | nadd1suc 42142 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
โข (๐ด โ On โ (๐ด +no 1o) = suc ๐ด) | ||
Theorem | naddsuc2 42143 | Natural addition with successor. (Contributed by RP, 1-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +no suc ๐ต) = suc (๐ด +no ๐ต)) | ||
Theorem | naddass1 42144 | Natural addition of ordinal numbers is associative when the third element is 1. (Contributed by RP, 1-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด +no ๐ต) +no 1o) = (๐ด +no (๐ต +no 1o))) | ||
Theorem | naddgeoa 42145 | Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +o ๐ต) โ (๐ด +no ๐ต)) | ||
Theorem | naddonnn 42146 | Natural addition with a natural number on the right results in a value equal to that of ordinal addition. (Contributed by RP, 1-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ ฯ) โ (๐ด +o ๐ต) = (๐ด +no ๐ต)) | ||
Theorem | naddwordnexlem0 42147 | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, (ฯ ยทo suc ๐ถ) lies between ๐ด and ๐ต. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ (๐ด โ (ฯ ยทo suc ๐ถ) โง (ฯ ยทo suc ๐ถ) โ ๐ต)) | ||
Theorem | naddwordnexlem1 42148 | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, ๐ต is equal to or larger than ๐ด. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | naddwordnexlem2 42149 | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, ๐ต is larger than ๐ด. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | naddwordnexlem3 42150* | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, every natural sum of ๐ด with a natural number is less that ๐ต. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ โ๐ฅ โ ฯ (๐ด +no ๐ฅ) โ ๐ต) | ||
Theorem | oawordex3 42151* | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, some ordinal sum of ๐ด is equal to ๐ต. This is a specialization of oawordex 8557. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ โ๐ฅ โ On (๐ด +o ๐ฅ) = ๐ต) | ||
Theorem | naddwordnexlem4 42152* | When ๐ด is the sum of a limit ordinal (or zero) and a natural number and ๐ต is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with ๐ด is less than or equal to ๐ต while the natural sum is larger than ๐ต. (Contributed by RP, 15-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) & โข ๐ = {๐ฆ โ On โฃ ๐ท โ (๐ถ +o ๐ฆ)} โ โข (๐ โ โ๐ฅ โ (On โ 1o)((๐ถ +o ๐ฅ) = ๐ท โง (๐ด +o (ฯ ยทo ๐ฅ)) โ ๐ต โง ๐ต โ (๐ด +no (ฯ ยทo ๐ฅ)))) | ||
Theorem | ordsssucim 42153 | If an ordinal is less than or equal to the successor of another, then the first is either less than or equal to the second or the first is equal to the successor of the second. Theorem 1 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 See also ordsssucb 42085 for a biimplication when ๐ด is a set. (Contributed by RP, 3-Jan-2025.) |
โข ((Ord ๐ด โง Ord ๐ต) โ (๐ด โ suc ๐ต โ (๐ด โ ๐ต โจ ๐ด = suc ๐ต))) | ||
Theorem | insucid 42154 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โฉ suc ๐ด) = ๐ด | ||
Theorem | om2 42155 | Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โ On โ (๐ด +o ๐ด) = (๐ด ยทo 2o)) | ||
Theorem | oaltom 42156 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((1o โ ๐ด โง ๐ด โ ๐ต) โ (๐ต +o ๐ด) โ (๐ต ยทo ๐ด))) | ||
Theorem | oe2 42157 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โ On โ (๐ด ยทo ๐ด) = (๐ด โo 2o)) | ||
Theorem | omltoe 42158 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((1o โ ๐ด โง ๐ด โ ๐ต) โ (๐ต ยทo ๐ด) โ (๐ต โo ๐ด))) | ||
Theorem | abeqabi 42159 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
โข ๐ด = {๐ฅ โฃ ๐} โ โข ({๐ฅ โฃ ๐} = ๐ด โ โ๐ฅ(๐ โ ๐)) | ||
Theorem | abpr 42160* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
โข ({๐ฅ โฃ ๐} = {๐, ๐} โ โ๐ฅ(๐ โ (๐ฅ = ๐ โจ ๐ฅ = ๐))) | ||
Theorem | abtp 42161* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
โข ({๐ฅ โฃ ๐} = {๐, ๐, ๐} โ โ๐ฅ(๐ โ (๐ฅ = ๐ โจ ๐ฅ = ๐ โจ ๐ฅ = ๐))) | ||
Theorem | ralopabb 42162* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ๐} & โข (๐ = โจ๐ฅ, ๐ฆโฉ โ (๐ โ ๐)) โ โข (โ๐ โ ๐ ๐ โ โ๐ฅโ๐ฆ(๐ โ ๐)) | ||
Theorem | fpwfvss 42163 | 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 42164 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
โข (๐ต โบ ๐ด โ ๐ด โ โ ) | ||
Theorem | sdomne0d 42165 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
โข (๐ โ ๐ต โบ ๐ด) & โข (๐ โ ๐ต โ ๐) โ โข (๐ โ ๐ด โ โ ) | ||
Theorem | safesnsupfiss 42166 | 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 42167* | 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 42168 | 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 42169* | 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 42170 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
โข (๐ โ ๐น = ๐บ) & โข (๐ โ ๐ด = ๐ถ) & โข (๐ โ ๐ต = ๐ท) โ โข (๐ โ (๐น Isom ๐ , ๐ (๐ด, ๐ต) โ ๐บ Isom ๐ , ๐ (๐ถ, ๐ท))) | ||
Theorem | resisoeq45d 42171 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
โข (๐ โ ๐ด = ๐ถ) & โข (๐ โ ๐ต = ๐ท) โ โข (๐ โ ((๐น โพ ๐ด) Isom ๐ , ๐ (๐ด, ๐ต) โ (๐น โพ ๐ถ) Isom ๐ , ๐ (๐ถ, ๐ท))) | ||
Theorem | negslem1 42172 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
โข (๐ด = ๐ต โ ((๐น โพ ๐ด) Isom ๐ , โก๐ (๐ด, ๐ด) โ (๐น โพ ๐ต) Isom ๐ , โก๐ (๐ต, ๐ต))) | ||
Theorem | nvocnvb 42173* | 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 42174* | 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 27287. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
โข < = {โจ๐, ๐โฉ โฃ (๐ โ ๐ โง ๐ โ ๐ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ๐ ๐ฆ)} โ โข (๐ด < ๐ต โ ((๐ด โ V โง ๐ต โ V) โง (๐ด โ ๐ โง ๐ต โ ๐ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ๐ ๐ฆ))) | ||
Theorem | nla0002 42175* | 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 42176* | 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 42177* | 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 42178* |
๐ต
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 42179 | 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 42180 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ On โง ๐ต โ {1o, 2o}) โ (๐ด ร {๐ต}) โ No ) | ||
Theorem | onnobdayg 42181 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ On โง ๐ต โ {1o, 2o}) โ ( bday โ(๐ด ร {๐ต})) = ๐ด) | ||
Theorem | bdaybndex 42182 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ No โง ๐ต = ( bday โ๐ด) โง ๐ถ โ {1o, 2o}) โ (๐ต ร {๐ถ}) โ No ) | ||
Theorem | bdaybndbday 42183 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
โข ((๐ด โ No โง ๐ต = ( bday โ๐ด) โง ๐ถ โ {1o, 2o}) โ ( bday โ(๐ต ร {๐ถ})) = ( bday โ๐ด)) | ||
Theorem | onno 42184 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (๐ด โ On โ (๐ด ร {2o}) โ No ) | ||
Theorem | onnoi 42185 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข ๐ด โ On โ โข (๐ด ร {2o}) โ No | ||
Theorem | 0no 42186 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข โ โ No | ||
Theorem | 1no 42187 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (1o ร {2o}) โ No | ||
Theorem | 2no 42188 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (2o ร {2o}) โ No | ||
Theorem | 3no 42189 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (3o ร {2o}) โ No | ||
Theorem | 4no 42190 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (4o ร {2o}) โ No | ||
Theorem | fnimafnex 42191 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
โข ๐น Fn ๐ต โ โข (๐น โ (๐บโ๐ด)) โ V | ||
Theorem | nlimsuc 42192 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข (๐ด โ On โ ยฌ Lim suc ๐ด) | ||
Theorem | nlim1NEW 42193 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
โข ยฌ Lim 1o | ||
Theorem | nlim2NEW 42194 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
โข ยฌ Lim 2o | ||
Theorem | nlim3 42195 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข ยฌ Lim 3o | ||
Theorem | nlim4 42196 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข ยฌ Lim 4o | ||
Theorem | oa1un 42197 | Given ๐ด โ On, let ๐ด +o 1o be defined to be the union of ๐ด and {๐ด}. Compare with oa1suc 8531. (Contributed by RP, 27-Sep-2023.) |
โข (๐ด โ On โ (๐ด +o 1o) = (๐ด โช {๐ด})) | ||
Theorem | oa1cl 42198 | ๐ด +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
โข (๐ด โ On โ (๐ด +o 1o) โ On) | ||
Theorem | 0finon 42199 | 0 is a finite ordinal. See peano1 7879. (Contributed by RP, 27-Sep-2023.) |
โข โ โ (On โฉ Fin) | ||
Theorem | 1finon 42200 | 1 is a finite ordinal. See 1onn 8639. (Contributed by RP, 27-Sep-2023.) |
โข 1o โ (On โฉ Fin) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |