Home | Intuitionistic Logic Explorer Theorem List (p. 62 of 114) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rdgexg 6101 | The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 Fn V ⇒ ⊢ (𝐵 ∈ 𝑉 → (rec(𝐹, 𝐴)‘𝐵) ∈ V) | ||
Syntax | cfrec 6102 | Extend class notation with the finite recursive definition generator, with characteristic function 𝐹 and initial value 𝐼. |
class frec(𝐹, 𝐼) | ||
Definition | df-frec 6103* |
Define a recursive definition generator on ω (the
class of finite
ordinals) with characteristic function 𝐹 and initial value 𝐼.
This rather amazing operation allows us to define, with compact direct
definitions, functions that are usually defined in textbooks only with
indirect self-referencing recursive definitions. A recursive definition
requires advanced metalogic to justify - in particular, eliminating a
recursive definition is very difficult and often not even shown in
textbooks. On the other hand, the elimination of a direct definition is
a matter of simple mechanical substitution. The price paid is the
daunting complexity of our frec operation
(especially when df-recs 6017
that it is built on is also eliminated). But once we get past this
hurdle, definitions that would otherwise be recursive become relatively
simple; see frec0g 6109 and frecsuc 6119.
Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4390. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6120, this definition and df-irdg 6082 restricted to ω produce the same result. Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.) |
⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω) | ||
Theorem | freceq1 6104 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝐹 = 𝐺 → frec(𝐹, 𝐴) = frec(𝐺, 𝐴)) | ||
Theorem | freceq2 6105 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝐴 = 𝐵 → frec(𝐹, 𝐴) = frec(𝐹, 𝐵)) | ||
Theorem | frecex 6106 | Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.) |
⊢ frec(𝐹, 𝐴) ∈ V | ||
Theorem | frecfun 6107 | Finite recursion produces a function. See also frecfnom 6113 which also states that the domain of that function is ω but which puts conditions on 𝐴 and 𝐹. (Contributed by Jim Kingdon, 13-Feb-2022.) |
⊢ Fun frec(𝐹, 𝐴) | ||
Theorem | nffrec 6108 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥frec(𝐹, 𝐴) | ||
Theorem | frec0g 6109 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | frecabex 6110* | The class abstraction from df-frec 6103 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦(𝐹‘𝑦) ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V) | ||
Theorem | frecabcl 6111* | The class abstraction from df-frec 6103 exists. Unlike frecabex 6110 the function 𝐹 only needs to be defined on 𝑆, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.) |
⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝐺:𝑁⟶𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) | ||
Theorem | frectfr 6112* |
Lemma to connect transfinite recursion theorems with finite recursion.
That is, given the conditions 𝐹 Fn V and 𝐴 ∈ 𝑉 on
frec(𝐹, 𝐴), we want to be able to apply tfri1d 6047 or tfri2d 6048,
and this lemma lets us satisfy hypotheses of those theorems.
(Contributed by Jim Kingdon, 15-Aug-2019.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺‘𝑦) ∈ V)) | ||
Theorem | frecfnom 6113* | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω) | ||
Theorem | freccllem 6114* | Lemma for freccl 6115. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) & ⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | freccl 6115* | Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | frecfcllem 6116* | Lemma for frecfcl 6117. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecfcl 6117* | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecsuclem 6118* | Lemma for frecsuc 6119. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecsuc 6119* | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecrdg 6120* |
Transfinite recursion restricted to omega.
Given a suitable characteristic function, df-frec 6103 produces the same results as df-irdg 6082 restricted to ω. Presumably the theorem would also hold if 𝐹 Fn V were changed to ∀𝑧(𝐹‘𝑧) ∈ V. (Contributed by Jim Kingdon, 29-Aug-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω)) | ||
Syntax | c1o 6121 | Extend the definition of a class to include the ordinal number 1. |
class 1_{𝑜} | ||
Syntax | c2o 6122 | Extend the definition of a class to include the ordinal number 2. |
class 2_{𝑜} | ||
Syntax | c3o 6123 | Extend the definition of a class to include the ordinal number 3. |
class 3_{𝑜} | ||
Syntax | c4o 6124 | Extend the definition of a class to include the ordinal number 4. |
class 4_{𝑜} | ||
Syntax | coa 6125 | Extend the definition of a class to include the ordinal addition operation. |
class +_{𝑜} | ||
Syntax | comu 6126 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·_{𝑜} | ||
Syntax | coei 6127 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑_{𝑜} | ||
Definition | df-1o 6128 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1_{𝑜} = suc ∅ | ||
Definition | df-2o 6129 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2_{𝑜} = suc 1_{𝑜} | ||
Definition | df-3o 6130 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3_{𝑜} = suc 2_{𝑜} | ||
Definition | df-4o 6131 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4_{𝑜} = suc 3_{𝑜} | ||
Definition | df-oadd 6132* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +_{𝑜} = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 6133* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·_{𝑜} = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +_{𝑜} 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexpi 6134* |
Define the ordinal exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑_{𝑜} 𝐴 to be 1_{𝑜} for all 𝐴 ∈ On, in order to avoid having different cases for whether the base is ∅ or not. (Contributed by Mario Carneiro, 4-Jul-2019.) |
⊢ ↑_{𝑜} = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·_{𝑜} 𝑥)), 1_{𝑜})‘𝑦)) | ||
Theorem | 1on 6135 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1_{𝑜} ∈ On | ||
Theorem | 1oex 6136 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
⊢ 1_{𝑜} ∈ V | ||
Theorem | 2on 6137 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2_{𝑜} ∈ On | ||
Theorem | 2on0 6138 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2_{𝑜} ≠ ∅ | ||
Theorem | 3on 6139 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3_{𝑜} ∈ On | ||
Theorem | 4on 6140 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4_{𝑜} ∈ On | ||
Theorem | df1o2 6141 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1_{𝑜} = {∅} | ||
Theorem | df2o3 6142 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2_{𝑜} = {∅, 1_{𝑜}} | ||
Theorem | df2o2 6143 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2_{𝑜} = {∅, {∅}} | ||
Theorem | 1n0 6144 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1_{𝑜} ≠ ∅ | ||
Theorem | xp01disj 6145 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1_{𝑜}})) = ∅ | ||
Theorem | ordgt0ge1 6146 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1_{𝑜} ⊆ 𝐴)) | ||
Theorem | ordge1n0im 6147 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
⊢ (Ord 𝐴 → (1_{𝑜} ⊆ 𝐴 → 𝐴 ≠ ∅)) | ||
Theorem | el1o 6148 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1_{𝑜} ↔ 𝐴 = ∅) | ||
Theorem | dif1o 6149 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1_{𝑜}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | 2oconcl 6150 | Closure of the pair swapping function on 2_{𝑜}. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2_{𝑜} → (1_{𝑜} ∖ 𝐴) ∈ 2_{𝑜}) | ||
Theorem | 0lt1o 6151 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1_{𝑜} | ||
Theorem | oafnex 6152 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ (𝑥 ∈ V ↦ suc 𝑥) Fn V | ||
Theorem | sucinc 6153* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ∀𝑥 𝑥 ⊆ (𝐹‘𝑥) | ||
Theorem | sucinc2 6154* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | fnoa 6155 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.) |
⊢ +_{𝑜} Fn (On × On) | ||
Theorem | oaexg 6156 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +_{𝑜} 𝐵) ∈ V) | ||
Theorem | omfnex 6157* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ V ↦ (𝑥 +_{𝑜} 𝐴)) Fn V) | ||
Theorem | fnom 6158 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ·_{𝑜} Fn (On × On) | ||
Theorem | omexg 6159 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ·_{𝑜} 𝐵) ∈ V) | ||
Theorem | fnoei 6160 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ↑_{𝑜} Fn (On × On) | ||
Theorem | oeiexg 6161 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑_{𝑜} 𝐵) ∈ V) | ||
Theorem | oav 6162* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +_{𝑜} 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | ||
Theorem | omv 6163* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·_{𝑜} 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +_{𝑜} 𝐴)), ∅)‘𝐵)) | ||
Theorem | oeiv 6164* | Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑_{𝑜} 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·_{𝑜} 𝐴)), 1_{𝑜})‘𝐵)) | ||
Theorem | oa0 6165 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 +_{𝑜} ∅) = 𝐴) | ||
Theorem | om0 6166 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ·_{𝑜} ∅) = ∅) | ||
Theorem | oei0 6167 | 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 → (𝐴 ↑_{𝑜} ∅) = 1_{𝑜}) | ||
Theorem | oacl 6168 | Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +_{𝑜} 𝐵) ∈ On) | ||
Theorem | omcl 6169 | Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Constructive proof by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·_{𝑜} 𝐵) ∈ On) | ||
Theorem | oeicl 6170 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑_{𝑜} 𝐵) ∈ On) | ||
Theorem | oav2 6171* | Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +_{𝑜} 𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +_{𝑜} 𝑥))) | ||
Theorem | oasuc 6172 | 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) → (𝐴 +_{𝑜} suc 𝐵) = suc (𝐴 +_{𝑜} 𝐵)) | ||
Theorem | omv2 6173* | Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·_{𝑜} 𝐵) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·_{𝑜} 𝑥) +_{𝑜} 𝐴)) | ||
Theorem | onasuc 6174 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +_{𝑜} suc 𝐵) = suc (𝐴 +_{𝑜} 𝐵)) | ||
Theorem | oa1suc 6175 | 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 → (𝐴 +_{𝑜} 1_{𝑜}) = suc 𝐴) | ||
Theorem | o1p1e2 6176 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
⊢ (1_{𝑜} +_{𝑜} 1_{𝑜}) = 2_{𝑜} | ||
Theorem | oawordi 6177 | Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 +_{𝑜} 𝐴) ⊆ (𝐶 +_{𝑜} 𝐵))) | ||
Theorem | oawordriexmid 6178* | A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6177. (Contributed by Jim Kingdon, 15-May-2022.) |
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑎 ⊆ 𝑏 → (𝑎 +_{𝑜} 𝑐) ⊆ (𝑏 +_{𝑜} 𝑐))) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | oaword1 6179 | An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +_{𝑜} 𝐵)) | ||
Theorem | omsuc 6180 | 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) → (𝐴 ·_{𝑜} suc 𝐵) = ((𝐴 ·_{𝑜} 𝐵) +_{𝑜} 𝐴)) | ||
Theorem | onmsuc 6181 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·_{𝑜} suc 𝐵) = ((𝐴 ·_{𝑜} 𝐵) +_{𝑜} 𝐴)) | ||
Theorem | nna0 6182 | Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 +_{𝑜} ∅) = 𝐴) | ||
Theorem | nnm0 6183 | Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) |
⊢ (𝐴 ∈ ω → (𝐴 ·_{𝑜} ∅) = ∅) | ||
Theorem | nnasuc 6184 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +_{𝑜} suc 𝐵) = suc (𝐴 +_{𝑜} 𝐵)) | ||
Theorem | nnmsuc 6185 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·_{𝑜} suc 𝐵) = ((𝐴 ·_{𝑜} 𝐵) +_{𝑜} 𝐴)) | ||
Theorem | nna0r 6186 | Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ (𝐴 ∈ ω → (∅ +_{𝑜} 𝐴) = 𝐴) | ||
Theorem | nnm0r 6187 | Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ (𝐴 ∈ ω → (∅ ·_{𝑜} 𝐴) = ∅) | ||
Theorem | nnacl 6188 | Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +_{𝑜} 𝐵) ∈ ω) | ||
Theorem | nnmcl 6189 | Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·_{𝑜} 𝐵) ∈ ω) | ||
Theorem | nnacli 6190 | ω is closed under addition. Inference form of nnacl 6188. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 +_{𝑜} 𝐵) ∈ ω | ||
Theorem | nnmcli 6191 | ω is closed under multiplication. Inference form of nnmcl 6189. (Contributed by Scott Fenton, 20-Apr-2012.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω ⇒ ⊢ (𝐴 ·_{𝑜} 𝐵) ∈ ω | ||
Theorem | nnacom 6192 | Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +_{𝑜} 𝐵) = (𝐵 +_{𝑜} 𝐴)) | ||
Theorem | nnaass 6193 | Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +_{𝑜} 𝐵) +_{𝑜} 𝐶) = (𝐴 +_{𝑜} (𝐵 +_{𝑜} 𝐶))) | ||
Theorem | nndi 6194 | Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ·_{𝑜} (𝐵 +_{𝑜} 𝐶)) = ((𝐴 ·_{𝑜} 𝐵) +_{𝑜} (𝐴 ·_{𝑜} 𝐶))) | ||
Theorem | nnmass 6195 | Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·_{𝑜} 𝐵) ·_{𝑜} 𝐶) = (𝐴 ·_{𝑜} (𝐵 ·_{𝑜} 𝐶))) | ||
Theorem | nnmsucr 6196 | Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ·_{𝑜} 𝐵) = ((𝐴 ·_{𝑜} 𝐵) +_{𝑜} 𝐵)) | ||
Theorem | nnmcom 6197 | Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·_{𝑜} 𝐵) = (𝐵 ·_{𝑜} 𝐴)) | ||
Theorem | nndir 6198 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +_{𝑜} 𝐵) ·_{𝑜} 𝐶) = ((𝐴 ·_{𝑜} 𝐶) +_{𝑜} (𝐵 ·_{𝑜} 𝐶))) | ||
Theorem | nnsucelsuc 6199 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4296, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4317. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) | ||
Theorem | nnsucsssuc 6200 | Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4297, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4314. (Contributed by Jim Kingdon, 25-Aug-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |