Home | Metamath
Proof Explorer Theorem List (p. 85 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2oexOLD 8401 | Obsolete version of 2oex 8391 as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 2o ∈ V | ||
Theorem | 1n0 8402 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1o ≠ ∅ | ||
Theorem | nlim1 8403 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ ¬ Lim 1o | ||
Theorem | nlim2 8404 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ ¬ Lim 2o | ||
Theorem | xp01disj 8405 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅ | ||
Theorem | xp01disjl 8406 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ | ||
Theorem | ordgt0ge1 8407 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) | ||
Theorem | ordge1n0 8408 | An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | el1o 8409 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) | ||
Theorem | ord1eln01 8410 | An ordinal that is not 0 or 1 contains 1. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ (Ord 𝐴 → (1o ∈ 𝐴 ↔ (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o))) | ||
Theorem | ord2eln012 8411 | An ordinal that is not 0, 1, or 2 contains 2. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ (Ord 𝐴 → (2o ∈ 𝐴 ↔ (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o))) | ||
Theorem | 1ellim 8412 | A limit ordinal contains 1. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ (Lim 𝐴 → 1o ∈ 𝐴) | ||
Theorem | 2ellim 8413 | A limit ordinal contains 2. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ (Lim 𝐴 → 2o ∈ 𝐴) | ||
Theorem | dif1o 8414 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | ondif1 8415 | Two ways to say that 𝐴 is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) | ||
Theorem | ondif2 8416 | Two ways to say that 𝐴 is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴)) | ||
Theorem | 2oconcl 8417 | Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o) | ||
Theorem | 0lt1o 8418 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1o | ||
Theorem | dif20el 8419 | An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴) | ||
Theorem | 0we1 8420 | The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ ∅ We 1o | ||
Theorem | brwitnlem 8421 | Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ 𝑅 = (◡𝑂 “ (V ∖ 1o)) & ⊢ 𝑂 Fn 𝑋 ⇒ ⊢ (𝐴𝑅𝐵 ↔ (𝐴𝑂𝐵) ≠ ∅) | ||
Theorem | fnoa 8422 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ +o Fn (On × On) | ||
Theorem | fnom 8423 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ·o Fn (On × On) | ||
Theorem | fnoe 8424 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ↑o Fn (On × On) | ||
Theorem | oav 8425* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | ||
Theorem | omv 8426* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +o 𝐴)), ∅)‘𝐵)) | ||
Theorem | oe0lem 8427 | A helper lemma for oe0 8436 and others. (Contributed by NM, 6-Jan-2005.) |
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝜓) & ⊢ (((𝐴 ∈ On ∧ 𝜑) ∧ ∅ ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝜑) → 𝜓) | ||
Theorem | oev 8428* | Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = if(𝐴 = ∅, (1o ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) | ||
Theorem | oevn0 8429* | Value of ordinal exponentiation at a nonzero base. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) | ||
Theorem | oa0 8430 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = 𝐴) | ||
Theorem | om0 8431 | Ordinal multiplication with zero. Definition 8.15(a) of [TakeutiZaring] p. 62. See om0x 8433 for a way to remove the antecedent 𝐴 ∈ On. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) = ∅) | ||
Theorem | oe0m 8432 | Value of zero raised to an ordinal. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (∅ ↑o 𝐴) = (1o ∖ 𝐴)) | ||
Theorem | om0x 8433 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 8431, this version works whether or not 𝐴 is an ordinal. However, since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐴 ·o ∅) = ∅ | ||
Theorem | oe0m0 8434 | Ordinal exponentiation with zero base and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) |
⊢ (∅ ↑o ∅) = 1o | ||
Theorem | oe0m1 8435 | Ordinal exponentiation with zero base and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67 and its converse. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ (∅ ↑o 𝐴) = ∅)) | ||
Theorem | oe0 8436 | Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) = 1o) | ||
Theorem | oev2 8437* | Alternate value of ordinal exponentiation. Compare oev 8428. (Contributed by NM, 2-Jan-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴) ∪ ∩ 𝐵))) | ||
Theorem | oasuc 8438 | Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | oesuclem 8439* | Lemma for oesuc 8441. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ Lim 𝑋 & ⊢ (𝐵 ∈ 𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) | ||
Theorem | omsuc 8440 | Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) | ||
Theorem | oesuc 8441 | Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) | ||
Theorem | onasuc 8442 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 8438 does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | onmsuc 8443 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) | ||
Theorem | onesuc 8444 | Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) | ||
Theorem | oa1suc 8445 | Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = suc 𝐴) | ||
Theorem | oalim 8446* | Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 +o 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 +o 𝑥)) | ||
Theorem | omlim 8447* | Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ·o 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ·o 𝑥)) | ||
Theorem | oelim 8448* | Ordinal exponentiation with a limit exponent and nonzero base. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 1-Jan-2005.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥)) | ||
Theorem | oacl 8449 | Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) | ||
Theorem | omcl 8450 | Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) | ||
Theorem | oecl 8451 | Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) | ||
Theorem | oa0r 8452 | Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) |
⊢ (𝐴 ∈ On → (∅ +o 𝐴) = 𝐴) | ||
Theorem | om0r 8453 | Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.) |
⊢ (𝐴 ∈ On → (∅ ·o 𝐴) = ∅) | ||
Theorem | o1p1e2 8454 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
⊢ (1o +o 1o) = 2o | ||
Theorem | o2p2e4 8455 | 2 + 2 = 4 for ordinal numbers. Ordinal numbers are modeled as Von Neumann ordinals; see df-suc 6320. For the usual proof using complex numbers, see 2p2e4 12222. (Contributed by NM, 18-Aug-2021.) Avoid ax-rep 5241, from a comment by Sophie. (Revised by SN, 23-Mar-2024.) |
⊢ (2o +o 2o) = 4o | ||
Theorem | o2p2e4OLD 8456 | Obsolete version of o2p2e4 8455 as of 23-Mar-2024. (Contributed by NM, 18-Aug-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (2o +o 2o) = 4o | ||
Theorem | om1 8457 | Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 29-Oct-1995.) |
⊢ (𝐴 ∈ On → (𝐴 ·o 1o) = 𝐴) | ||
Theorem | om1r 8458 | Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.) |
⊢ (𝐴 ∈ On → (1o ·o 𝐴) = 𝐴) | ||
Theorem | oe1 8459 | Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005.) |
⊢ (𝐴 ∈ On → (𝐴 ↑o 1o) = 𝐴) | ||
Theorem | oe1m 8460 | Ordinal exponentiation with a base of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67. (Contributed by NM, 2-Jan-2005.) |
⊢ (𝐴 ∈ On → (1o ↑o 𝐴) = 1o) | ||
Theorem | oaordi 8461 | Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.) |
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) | ||
Theorem | oaord 8462 | Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58 and its converse. (Contributed by NM, 5-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) | ||
Theorem | oacan 8463 | Left cancellation law for ordinal addition. Corollary 8.5 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | oaword 8464 | Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) | ||
Theorem | oawordri 8465 | Weak ordering property of ordinal addition. Proposition 8.7 of [TakeutiZaring] p. 59. (Contributed by NM, 7-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +o 𝐶) ⊆ (𝐵 +o 𝐶))) | ||
Theorem | oaord1 8466 | An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of [Suppes] p. 209 and its converse. (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ 𝐵 ↔ 𝐴 ∈ (𝐴 +o 𝐵))) | ||
Theorem | oaword1 8467 | An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (For the other part see oaord1 8466.) (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +o 𝐵)) | ||
Theorem | oaword2 8468 | An ordinal is less than or equal to its sum with another. Theorem 21 of [Suppes] p. 209. (Contributed by NM, 7-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐵 +o 𝐴)) | ||
Theorem | oawordeulem 8469* | Lemma for oawordex 8472. (Contributed by NM, 11-Dec-2004.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On & ⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⇒ ⊢ (𝐴 ⊆ 𝐵 → ∃!𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | oawordeu 8470* | Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59. (Contributed by NM, 11-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ∃!𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | oawordexr 8471* | Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) → 𝐴 ⊆ 𝐵) | ||
Theorem | oawordex 8472* | Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 8470 for uniqueness. (Contributed by NM, 12-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)) | ||
Theorem | oaordex 8473* | Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of [Mendelson] p. 266 and its converse. (Contributed by NM, 12-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) | ||
Theorem | oa00 8474 | An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) | ||
Theorem | oalimcl 8475 | The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60. (Contributed by NM, 8-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Lim (𝐴 +o 𝐵)) | ||
Theorem | oaass 8476 | Ordinal addition is associative. Theorem 25 of [Suppes] p. 211. (Contributed by NM, 10-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) | ||
Theorem | oarec 8477* | Recursive definition of ordinal addition. Exercise 25 of [Enderton] p. 240. (Contributed by NM, 26-Dec-2004.) (Revised by Mario Carneiro, 30-May-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥)))) | ||
Theorem | oaf1o 8478* | Left addition by a constant is a bijection from ordinals to ordinals greater than the constant. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝐴 ∈ On → (𝑥 ∈ On ↦ (𝐴 +o 𝑥)):On–1-1-onto→(On ∖ 𝐴)) | ||
Theorem | oacomf1olem 8479* | Lemma for oacomf1o 8480. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐵 +o 𝑥)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹:𝐴–1-1-onto→ran 𝐹 ∧ (ran 𝐹 ∩ 𝐵) = ∅)) | ||
Theorem | oacomf1o 8480* | Define a bijection from 𝐴 +o 𝐵 to 𝐵 +o 𝐴. Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g., oancom 9521). (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = ((𝑥 ∈ 𝐴 ↦ (𝐵 +o 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐴 +o 𝐵)–1-1-onto→(𝐵 +o 𝐴)) | ||
Theorem | omordi 8481 | Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.) |
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) | ||
Theorem | omord2 8482 | Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) | ||
Theorem | omord 8483 | Ordering property of ordinal multiplication. Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) | ||
Theorem | omcan 8484 | Left cancellation law for ordinal multiplication. Proposition 8.20 of [TakeutiZaring] p. 63 and its converse. (Contributed by NM, 14-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | omword 8485 | Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) | ||
Theorem | omwordi 8486 | Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) | ||
Theorem | omwordri 8487 | Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 ·o 𝐶) ⊆ (𝐵 ·o 𝐶))) | ||
Theorem | omword1 8488 | An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → 𝐴 ⊆ (𝐴 ·o 𝐵)) | ||
Theorem | omword2 8489 | An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → 𝐴 ⊆ (𝐵 ·o 𝐴)) | ||
Theorem | om00 8490 | The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of [TakeutiZaring] p. 64. (Contributed by NM, 21-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) | ||
Theorem | om00el 8491 | The product of two nonzero ordinal numbers is nonzero. (Contributed by NM, 28-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ (𝐴 ·o 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))) | ||
Theorem | omordlim 8492* | Ordering involving the product of a limit ordinal. Proposition 8.23 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐷 ∧ Lim 𝐵)) ∧ 𝐶 ∈ (𝐴 ·o 𝐵)) → ∃𝑥 ∈ 𝐵 𝐶 ∈ (𝐴 ·o 𝑥)) | ||
Theorem | omlimcl 8493 | The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝐵)) | ||
Theorem | odi 8494 | Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | ||
Theorem | omass 8495 | Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65. (Contributed by NM, 28-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) ·o 𝐶) = (𝐴 ·o (𝐵 ·o 𝐶))) | ||
Theorem | oneo 8496 | If an ordinal number is even, its successor is odd. (Contributed by NM, 26-Jan-2006.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2o ·o 𝐴)) → ¬ suc 𝐶 = (2o ·o 𝐵)) | ||
Theorem | omeulem1 8497* | Lemma for omeu 8500: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) | ||
Theorem | omeulem2 8498 | Lemma for omeu 8500: uniqueness part. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 29-May-2015.) |
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐵 ∈ 𝐷 ∨ (𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸)) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) | ||
Theorem | omopth2 8499 | An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (((𝐴 ·o 𝐵) +o 𝐶) = ((𝐴 ·o 𝐷) +o 𝐸) ↔ (𝐵 = 𝐷 ∧ 𝐶 = 𝐸))) | ||
Theorem | omeu 8500* | The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃!𝑧∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |