Home | Metamath
Proof Explorer Theorem List (p. 82 of 449) | < 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-28687) |
Hilbert Space Explorer
(28688-30210) |
Users' Mathboxes
(30211-44897) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1on 8101 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o ∈ On | ||
Theorem | 1oex 8102 | Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) |
⊢ 1o ∈ V | ||
Theorem | 2on 8103 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2o ∈ On | ||
Theorem | 2oex 8104 | 2o is a set. (Contributed by BJ, 6-Apr-2019.) |
⊢ 2o ∈ V | ||
Theorem | 2on0 8105 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2o ≠ ∅ | ||
Theorem | 3on 8106 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3o ∈ On | ||
Theorem | 4on 8107 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4o ∈ On | ||
Theorem | df1o2 8108 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1o = {∅} | ||
Theorem | df2o3 8109 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2o = {∅, 1o} | ||
Theorem | df2o2 8110 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2o = {∅, {∅}} | ||
Theorem | 1n0 8111 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1o ≠ ∅ | ||
Theorem | xp01disj 8112 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅ | ||
Theorem | xp01disjl 8113 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ | ||
Theorem | ordgt0ge1 8114 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) | ||
Theorem | ordge1n0 8115 | An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | el1o 8116 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) | ||
Theorem | dif1o 8117 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | ondif1 8118 | Two ways to say that 𝐴 is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) | ||
Theorem | ondif2 8119 | Two ways to say that 𝐴 is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴)) | ||
Theorem | 2oconcl 8120 | Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o) | ||
Theorem | 0lt1o 8121 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1o | ||
Theorem | dif20el 8122 | An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴) | ||
Theorem | 0we1 8123 | The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ ∅ We 1o | ||
Theorem | brwitnlem 8124 | 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 8125 | 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 8126 | 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 8127 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ↑o Fn (On × On) | ||
Theorem | oav 8128* | 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 8129* | 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 8130 | A helper lemma for oe0 8139 and others. (Contributed by NM, 6-Jan-2005.) |
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝜓) & ⊢ (((𝐴 ∈ On ∧ 𝜑) ∧ ∅ ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝜑) → 𝜓) | ||
Theorem | oev 8131* | 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 8132* | Value of ordinal exponentiation at a nonzero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) | ||
Theorem | oa0 8133 | 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 8134 | Ordinal multiplication with zero. Definition 8.15(a) of [TakeutiZaring] p. 62. See om0x 8136 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 8135 | Ordinal exponentiation with zero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (∅ ↑o 𝐴) = (1o ∖ 𝐴)) | ||
Theorem | om0x 8136 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 8134, 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 8137 | Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) |
⊢ (∅ ↑o ∅) = 1o | ||
Theorem | oe0m1 8138 | Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67 and its converse. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ (∅ ↑o 𝐴) = ∅)) | ||
Theorem | oe0 8139 | 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 8140* | Alternate value of ordinal exponentiation. Compare oev 8131. (Contributed by NM, 2-Jan-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵) ∩ ((V ∖ ∩ 𝐴) ∪ ∩ 𝐵))) | ||
Theorem | oasuc 8141 | 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 8142* | Lemma for oesuc 8144. (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 8143 | 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 8144 | 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 8145 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 8141 does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) | ||
Theorem | onmsuc 8146 | 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 8147 | 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 8148 | 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 8149* | 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 8150* | 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 8151* | Ordinal exponentiation with a limit exponent and nonzero mantissa. 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 8152 | Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) | ||
Theorem | omcl 8153 | 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 8154 | 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 8155 | Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) |
⊢ (𝐴 ∈ On → (∅ +o 𝐴) = 𝐴) | ||
Theorem | om0r 8156 | Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.) |
⊢ (𝐴 ∈ On → (∅ ·o 𝐴) = ∅) | ||
Theorem | o1p1e2 8157 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
⊢ (1o +o 1o) = 2o | ||
Theorem | o2p2e4 8158 | 2 + 2 = 4 for ordinal numbers. Ordinal numbers are modeled as Von Neumann ordinals; see df-suc 6190. For the usual proof using complex numbers, see 2p2e4 11764. (Contributed by NM, 18-Aug-2021.) Avoid ax-rep 5181, from a comment by Sophie. (Revised by SN, 23-Mar-2024.) |
⊢ (2o +o 2o) = 4o | ||
Theorem | o2p2e4OLD 8159 | 2 + 2 = 4 for ordinal numbers. (Contributed by NM, 18-Aug-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (2o +o 2o) = 4o | ||
Theorem | om1 8160 | Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 29-Oct-1995.) |
⊢ (𝐴 ∈ On → (𝐴 ·o 1o) = 𝐴) | ||
Theorem | om1r 8161 | Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.) |
⊢ (𝐴 ∈ On → (1o ·o 𝐴) = 𝐴) | ||
Theorem | oe1 8162 | Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005.) |
⊢ (𝐴 ∈ On → (𝐴 ↑o 1o) = 𝐴) | ||
Theorem | oe1m 8163 | Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67. (Contributed by NM, 2-Jan-2005.) |
⊢ (𝐴 ∈ On → (1o ↑o 𝐴) = 1o) | ||
Theorem | oaordi 8164 | Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.) |
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) | ||
Theorem | oaord 8165 | 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 8166 | 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 8167 | 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 8168 | 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 8169 | 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 8170 | 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 8169.) (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +o 𝐵)) | ||
Theorem | oaword2 8171 | 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 8172* | Lemma for oawordex 8175. (Contributed by NM, 11-Dec-2004.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On & ⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐵 ⊆ (𝐴 +o 𝑦)} ⇒ ⊢ (𝐴 ⊆ 𝐵 → ∃!𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) | ||
Theorem | oawordeu 8173* | 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 8174* | Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵) → 𝐴 ⊆ 𝐵) | ||
Theorem | oawordex 8175* | Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 8173 for uniqueness. (Contributed by NM, 12-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)) | ||
Theorem | oaordex 8176* | 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 8177 | An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) | ||
Theorem | oalimcl 8178 | 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 8179 | 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 8180* | 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 8181* | 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 8182* | Lemma for oacomf1o 8183. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐵 +o 𝑥)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹:𝐴–1-1-onto→ran 𝐹 ∧ (ran 𝐹 ∩ 𝐵) = ∅)) | ||
Theorem | oacomf1o 8183* | Define a bijection from 𝐴 +o 𝐵 to 𝐵 +o 𝐴. Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g., oancom 9106). (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = ((𝑥 ∈ 𝐴 ↦ (𝐵 +o 𝑥)) ∪ ◡(𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐴 +o 𝐵)–1-1-onto→(𝐵 +o 𝐴)) | ||
Theorem | omordi 8184 | 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 8185 | Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) | ||
Theorem | omord 8186 | 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 8187 | 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 8188 | Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) | ||
Theorem | omwordi 8189 | Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) | ||
Theorem | omwordri 8190 | 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 8191 | An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → 𝐴 ⊆ (𝐴 ·o 𝐵)) | ||
Theorem | omword2 8192 | An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → 𝐴 ⊆ (𝐵 ·o 𝐴)) | ||
Theorem | om00 8193 | 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 8194 | The product of two nonzero ordinal numbers is nonzero. (Contributed by NM, 28-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ (𝐴 ·o 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))) | ||
Theorem | omordlim 8195* | 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 8196 | 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 8197 | 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 8198 | 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 8199 | 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 8200* | Lemma for omeu 8203: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) = 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |