![]() |
Metamath
Proof Explorer Theorem List (p. 423 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 | naddcnffn 42201 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
โข ((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โ ( โf +o โพ (๐ ร ๐)) Fn (๐ ร ๐)) | ||
Theorem | naddcnffo 42202 | 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 42203 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น โf +o ๐บ) โ ๐) | ||
Theorem | naddcnfcom 42204 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น โf +o ๐บ) = (๐บ โf +o ๐น)) | ||
Theorem | naddcnfid1 42205 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง ๐น โ ๐) โ (๐น โf +o (๐ ร {โ })) = ๐น) | ||
Theorem | naddcnfid2 42206 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
โข (((๐ โ On โง ๐ = dom (ฯ CNF ๐)) โง ๐น โ ๐) โ ((๐ ร {โ }) โf +o ๐น) = ๐น) | ||
Theorem | naddcnfass 42207 | 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 42208* | 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 42209 | 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 42210 | 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 42211 | 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 42212* | The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 42220. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ Ord {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)}) | ||
Theorem | oaun3lem2 42213* | The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 42220. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ (๐ด +o ๐ต)) | ||
Theorem | oaun3lem3 42214* | The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 42220. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ On) | ||
Theorem | oaun3lem4 42215* | The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 42220. (Contributed by RP, 12-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ {๐ฅ โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ฅ = (๐ +o ๐)} โ suc (๐ด +o ๐ต)) | ||
Theorem | rp-abid 42216* | Two ways to express a class. (Contributed by RP, 13-Feb-2025.) |
โข ๐ด = {๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐} | ||
Theorem | oadif1lem 42217* | 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 42218* | 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 42219* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +o ๐ต) = โช {{๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐}, {๐ฆ โฃ โ๐ โ ๐ต ๐ฆ = (๐ด +o ๐)}}) | ||
Theorem | oaun3 42220* | Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +o ๐ต) = โช {{๐ฅ โฃ โ๐ โ ๐ด ๐ฅ = ๐}, {๐ฆ โฃ โ๐ โ ๐ต ๐ฆ = (๐ด +o ๐)}, {๐ง โฃ โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ +o ๐)}}) | ||
Theorem | naddov4 42221* | Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +no ๐ต) = โฉ ({๐ฅ โ On โฃ โ๐ โ ๐ด (๐ +no ๐ต) โ ๐ฅ} โฉ {๐ฅ โ On โฃ โ๐ โ ๐ต (๐ด +no ๐) โ ๐ฅ})) | ||
Theorem | nadd2rabtr 42222* | 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 42223* | 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 42224* | 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 42225* | 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 42226* | 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 42227* | 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 42228* | 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 42229* | 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 42230 | Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.) |
โข (๐ด โ On โ (๐ด +no 1o) = suc ๐ด) | ||
Theorem | naddsuc2 42231 | Natural addition with successor. (Contributed by RP, 1-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด +no suc ๐ต) = suc (๐ด +no ๐ต)) | ||
Theorem | naddass1 42232 | 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 42233 | 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 42234 | 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 42235 | 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 42236 | 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 42237 | 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 42238* | 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 42239* | 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 8559. (Contributed by RP, 14-Feb-2025.) |
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) & โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) & โข (๐ โ ๐ถ โ ๐ท) & โข (๐ โ ๐ท โ On) & โข (๐ โ ๐ โ ฯ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ โ๐ฅ โ On (๐ด +o ๐ฅ) = ๐ต) | ||
Theorem | naddwordnexlem4 42240* | 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 42241 | 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 42173 for a biimplication when ๐ด is a set. (Contributed by RP, 3-Jan-2025.) |
โข ((Ord ๐ด โง Ord ๐ต) โ (๐ด โ suc ๐ต โ (๐ด โ ๐ต โจ ๐ด = suc ๐ต))) | ||
Theorem | insucid 42242 | The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โฉ suc ๐ด) = ๐ด | ||
Theorem | om2 42243 | Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โ On โ (๐ด +o ๐ด) = (๐ด ยทo 2o)) | ||
Theorem | oaltom 42244 | Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((1o โ ๐ด โง ๐ด โ ๐ต) โ (๐ต +o ๐ด) โ (๐ต ยทo ๐ด))) | ||
Theorem | oe2 42245 | Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.) |
โข (๐ด โ On โ (๐ด ยทo ๐ด) = (๐ด โo 2o)) | ||
Theorem | omltoe 42246 | Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.) |
โข ((๐ด โ On โง ๐ต โ On) โ ((1o โ ๐ด โง ๐ด โ ๐ต) โ (๐ต ยทo ๐ด) โ (๐ต โo ๐ด))) | ||
Theorem | abeqabi 42247 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
โข ๐ด = {๐ฅ โฃ ๐} โ โข ({๐ฅ โฃ ๐} = ๐ด โ โ๐ฅ(๐ โ ๐)) | ||
Theorem | abpr 42248* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
โข ({๐ฅ โฃ ๐} = {๐, ๐} โ โ๐ฅ(๐ โ (๐ฅ = ๐ โจ ๐ฅ = ๐))) | ||
Theorem | abtp 42249* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
โข ({๐ฅ โฃ ๐} = {๐, ๐, ๐} โ โ๐ฅ(๐ โ (๐ฅ = ๐ โจ ๐ฅ = ๐ โจ ๐ฅ = ๐))) | ||
Theorem | ralopabb 42250* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ๐} & โข (๐ = โจ๐ฅ, ๐ฆโฉ โ (๐ โ ๐)) โ โข (โ๐ โ ๐ ๐ โ โ๐ฅโ๐ฆ(๐ โ ๐)) | ||
Theorem | fpwfvss 42251 | 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 42252 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
โข (๐ต โบ ๐ด โ ๐ด โ โ ) | ||
Theorem | sdomne0d 42253 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
โข (๐ โ ๐ต โบ ๐ด) & โข (๐ โ ๐ต โ ๐) โ โข (๐ โ ๐ด โ โ ) | ||
Theorem | safesnsupfiss 42254 | 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 42255* | 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 42256 | 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 42257* | 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 42258 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
โข (๐ โ ๐น = ๐บ) & โข (๐ โ ๐ด = ๐ถ) & โข (๐ โ ๐ต = ๐ท) โ โข (๐ โ (๐น Isom ๐ , ๐ (๐ด, ๐ต) โ ๐บ Isom ๐ , ๐ (๐ถ, ๐ท))) | ||
Theorem | resisoeq45d 42259 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
โข (๐ โ ๐ด = ๐ถ) & โข (๐ โ ๐ต = ๐ท) โ โข (๐ โ ((๐น โพ ๐ด) Isom ๐ , ๐ (๐ด, ๐ต) โ (๐น โพ ๐ถ) Isom ๐ , ๐ (๐ถ, ๐ท))) | ||
Theorem | negslem1 42260 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
โข (๐ด = ๐ต โ ((๐น โพ ๐ด) Isom ๐ , โก๐ (๐ด, ๐ด) โ (๐น โพ ๐ต) Isom ๐ , โก๐ (๐ต, ๐ต))) | ||
Theorem | nvocnvb 42261* | 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 42262* | 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 27294. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
โข < = {โจ๐, ๐โฉ โฃ (๐ โ ๐ โง ๐ โ ๐ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ๐ ๐ฆ)} โ โข (๐ด < ๐ต โ ((๐ด โ V โง ๐ต โ V) โง (๐ด โ ๐ โง ๐ต โ ๐ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ๐ ๐ฆ))) | ||
Theorem | nla0002 42263* | 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 42264* | 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 42265* | 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 42266* |
๐ต
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 42267 | 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 42268 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ On โง ๐ต โ {1o, 2o}) โ (๐ด ร {๐ต}) โ No ) | ||
Theorem | onnobdayg 42269 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ On โง ๐ต โ {1o, 2o}) โ ( bday โ(๐ด ร {๐ต})) = ๐ด) | ||
Theorem | bdaybndex 42270 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
โข ((๐ด โ No โง ๐ต = ( bday โ๐ด) โง ๐ถ โ {1o, 2o}) โ (๐ต ร {๐ถ}) โ No ) | ||
Theorem | bdaybndbday 42271 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
โข ((๐ด โ No โง ๐ต = ( bday โ๐ด) โง ๐ถ โ {1o, 2o}) โ ( bday โ(๐ต ร {๐ถ})) = ( bday โ๐ด)) | ||
Theorem | onno 42272 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (๐ด โ On โ (๐ด ร {2o}) โ No ) | ||
Theorem | onnoi 42273 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข ๐ด โ On โ โข (๐ด ร {2o}) โ No | ||
Theorem | 0no 42274 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข โ โ No | ||
Theorem | 1no 42275 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (1o ร {2o}) โ No | ||
Theorem | 2no 42276 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (2o ร {2o}) โ No | ||
Theorem | 3no 42277 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (3o ร {2o}) โ No | ||
Theorem | 4no 42278 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
โข (4o ร {2o}) โ No | ||
Theorem | fnimafnex 42279 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
โข ๐น Fn ๐ต โ โข (๐น โ (๐บโ๐ด)) โ V | ||
Theorem | nlimsuc 42280 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข (๐ด โ On โ ยฌ Lim suc ๐ด) | ||
Theorem | nlim1NEW 42281 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
โข ยฌ Lim 1o | ||
Theorem | nlim2NEW 42282 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
โข ยฌ Lim 2o | ||
Theorem | nlim3 42283 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข ยฌ Lim 3o | ||
Theorem | nlim4 42284 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
โข ยฌ Lim 4o | ||
Theorem | oa1un 42285 | Given ๐ด โ On, let ๐ด +o 1o be defined to be the union of ๐ด and {๐ด}. Compare with oa1suc 8533. (Contributed by RP, 27-Sep-2023.) |
โข (๐ด โ On โ (๐ด +o 1o) = (๐ด โช {๐ด})) | ||
Theorem | oa1cl 42286 | ๐ด +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
โข (๐ด โ On โ (๐ด +o 1o) โ On) | ||
Theorem | 0finon 42287 | 0 is a finite ordinal. See peano1 7881. (Contributed by RP, 27-Sep-2023.) |
โข โ โ (On โฉ Fin) | ||
Theorem | 1finon 42288 | 1 is a finite ordinal. See 1onn 8641. (Contributed by RP, 27-Sep-2023.) |
โข 1o โ (On โฉ Fin) | ||
Theorem | 2finon 42289 | 2 is a finite ordinal. See 1onn 8641. (Contributed by RP, 27-Sep-2023.) |
โข 2o โ (On โฉ Fin) | ||
Theorem | 3finon 42290 | 3 is a finite ordinal. See 1onn 8641. (Contributed by RP, 27-Sep-2023.) |
โข 3o โ (On โฉ Fin) | ||
Theorem | 4finon 42291 | 4 is a finite ordinal. See 1onn 8641. (Contributed by RP, 27-Sep-2023.) |
โข 4o โ (On โฉ Fin) | ||
Theorem | finona1cl 42292 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
โข (๐ โ (On โฉ Fin) โ (๐ +o 1o) โ (On โฉ Fin)) | ||
Theorem | finonex 42293 | The finite ordinals are a set. See also onprc 7767 and fiprc 9047 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
โข (On โฉ Fin) โ V | ||
Theorem | fzunt 42294 | 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 42295 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โค ๐) & โข (๐ โ ๐ โค ๐) โ โข (๐ โ ((๐พ...๐) โช (๐...๐)) = (๐พ...๐)) | ||
Theorem | fzunt1d 42296 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ฟ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โค ๐) & โข (๐ โ ๐ โค ๐ฟ) & โข (๐ โ ๐ฟ โค ๐) โ โข (๐ โ ((๐พ...๐ฟ) โช (๐...๐)) = (๐พ...๐)) | ||
Theorem | fzuntgd 42297 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ฟ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โค ๐) & โข (๐ โ ๐ โค (๐ฟ + 1)) & โข (๐ โ ๐ฟ โค ๐) โ โข (๐ โ ((๐พ...๐ฟ) โช (๐...๐)) = (๐พ...๐)) | ||
Theorem | ifpan123g 42298 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
โข ((if-(๐, ๐, ๐) โง if-(๐, ๐, ๐)) โ (((ยฌ ๐ โจ ๐) โง (๐ โจ ๐)) โง ((ยฌ ๐ โจ ๐) โง (๐ โจ ๐)))) | ||
Theorem | ifpan23 42299 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
โข ((if-(๐, ๐, ๐) โง if-(๐, ๐, ๐)) โ if-(๐, (๐ โง ๐), (๐ โง ๐))) | ||
Theorem | ifpdfor2 42300 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
โข ((๐ โจ ๐) โ if-(๐, ๐, ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |