Home | Metamath
Proof Explorer Theorem List (p. 76 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssonuni 7501 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On)) | ||
Theorem | ssonunii 7502 | The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On) | ||
Theorem | ordeleqon 7503 | A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse. (Contributed by NM, 1-Jun-2003.) |
⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) | ||
Theorem | ordsson 7504 | Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ On) | ||
Theorem | onss 7505 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | ||
Theorem | predon 7506 | The predecessor of an ordinal under E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | ssonprc 7507 | Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On)) | ||
Theorem | onuni 7508 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On) | ||
Theorem | orduni 7509 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → Ord ∪ 𝐴) | ||
Theorem | onint 7510 | The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴) | ||
Theorem | onint0 7511 | The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴)) | ||
Theorem | onssmin 7512* | A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) | ||
Theorem | onminesb 7513 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 29-Sep-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 → [∩ {𝑥 ∈ On ∣ 𝜑} / 𝑥]𝜑) | ||
Theorem | onminsb 7514 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ∩ {𝑥 ∈ On ∣ 𝜑} → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → 𝜓) | ||
Theorem | oninton 7515 | The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ On) | ||
Theorem | onintrab 7516 | The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∩ {𝑥 ∈ On ∣ 𝜑} ∈ V ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onintrab2 7517 | An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onnmin 7518 | No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴) | ||
Theorem | onnminsb 7519* | An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. 𝜓 is the wff resulting from the substitution of 𝐴 for 𝑥 in wff 𝜑. (Contributed by NM, 9-Nov-2003.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝐴 ∈ ∩ {𝑥 ∈ On ∣ 𝜑} → ¬ 𝜓)) | ||
Theorem | oneqmin 7520* | A way to show that an ordinal number equals the minimum of a nonempty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.) |
⊢ ((𝐵 ⊆ On ∧ 𝐵 ≠ ∅) → (𝐴 = ∩ 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵))) | ||
Theorem | uniordint 7521* | The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
Theorem | onminex 7522* | If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Mario Carneiro, 20-Nov-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → ∃𝑥 ∈ On (𝜑 ∧ ∀𝑦 ∈ 𝑥 ¬ 𝜓)) | ||
Theorem | sucon 7523 | The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.) |
⊢ suc On = On | ||
Theorem | sucexb 7524 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | ||
Theorem | sucexg 7525 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | sucex 7526 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Theorem | onmindif2 7527 | The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ ∩ (𝐴 ∖ {∩ 𝐴})) | ||
Theorem | suceloni 7528 | The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) | ||
Theorem | ordsuc 7529 | The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.) |
⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | ||
Theorem | ordpwsuc 7530 | The collection of ordinals in the power class of an ordinal is its successor. (Contributed by NM, 30-Jan-2005.) |
⊢ (Ord 𝐴 → (𝒫 𝐴 ∩ On) = suc 𝐴) | ||
Theorem | onpwsuc 7531 | The collection of ordinal numbers in the power set of an ordinal number is its successor. (Contributed by NM, 19-Oct-2004.) |
⊢ (𝐴 ∈ On → (𝒫 𝐴 ∩ On) = suc 𝐴) | ||
Theorem | sucelon 7532 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) | ||
Theorem | ordsucss 7533 | The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) | ||
Theorem | onpsssuc 7534 | An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ On → 𝐴 ⊊ suc 𝐴) | ||
Theorem | ordelsuc 7535 | A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.) |
⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵)) | ||
Theorem | onsucmin 7536* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
⊢ (𝐴 ∈ On → suc 𝐴 = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | ordsucelsuc 7537 | Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42. (Contributed by NM, 22-Jun-1998.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) | ||
Theorem | ordsucsssuc 7538 | The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) | ||
Theorem | ordsucuniel 7539 | Given an element 𝐴 of the union of an ordinal 𝐵, suc 𝐴 is an element of 𝐵 itself. (Contributed by Scott Fenton, 28-Mar-2012.) (Proof shortened by Mario Carneiro, 29-May-2015.) |
⊢ (Ord 𝐵 → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) | ||
Theorem | ordsucun 7540 | The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) | ||
Theorem | ordunpr 7541 | The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∪ 𝐶) ∈ {𝐵, 𝐶}) | ||
Theorem | ordunel 7542 | The maximum of two ordinals belongs to a third if each of them do. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | onsucuni 7543 | A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of [TakeutiZaring] p. 41. (Contributed by NM, 19-Sep-2003.) |
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) | ||
Theorem | ordsucuni 7544 | An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ suc ∪ 𝐴) | ||
Theorem | orduniorsuc 7545 | An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) | ||
Theorem | unon 7546 | The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.) |
⊢ ∪ On = On | ||
Theorem | ordunisuc 7547 | An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (Ord 𝐴 → ∪ suc 𝐴 = 𝐴) | ||
Theorem | orduniss2 7548* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.) |
⊢ (Ord 𝐴 → ∪ {𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | onsucuni2 7549 | A successor ordinal is the successor of its union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪ 𝐴 = 𝐴) | ||
Theorem | 0elsuc 7550 | The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.) |
⊢ (Ord 𝐴 → ∅ ∈ suc 𝐴) | ||
Theorem | limon 7551 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
⊢ Lim On | ||
Theorem | onssi 7552 | An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ 𝐴 ⊆ On | ||
Theorem | onsuci 7553 | The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ On | ||
Theorem | onuniorsuci 7554 | An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴) | ||
Theorem | onuninsuci 7555* | A limit ordinal is not a successor ordinal. (Contributed by NM, 18-Feb-2004.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥) | ||
Theorem | onsucssi 7556 | A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵) | ||
Theorem | nlimsucg 7557 | A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → ¬ Lim suc 𝐴) | ||
Theorem | orduninsuc 7558* | An ordinal equal to its union is not a successor. (Contributed by NM, 18-Feb-2004.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) | ||
Theorem | ordunisuc2 7559* | An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | ordzsl 7560* | An ordinal is zero, a successor ordinal, or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) | ||
Theorem | onzsl 7561* | An ordinal number is zero, a successor ordinal, or a limit ordinal number. (Contributed by NM, 1-Oct-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) | ||
Theorem | dflim3 7562* | An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) | ||
Theorem | dflim4 7563* | An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | limsuc 7564 | The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.) |
⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) | ||
Theorem | limsssuc 7565 | A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | nlimon 7566* | Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of [TakeutiZaring] p. 42, who use the symbol KI for this class. (Contributed by NM, 1-Nov-2004.) |
⊢ {𝑥 ∈ On ∣ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)} = {𝑥 ∈ On ∣ ¬ Lim 𝑥} | ||
Theorem | limuni3 7567* | The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪ 𝐴) | ||
Theorem | tfi 7568* |
The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring]
p. 39. This principle states that if 𝐴 is a class of ordinal
numbers with the property that every ordinal number included in 𝐴
also belongs to 𝐴, then every ordinal number is in
𝐴.
See theorem tfindes 7577 or tfinds 7574 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On) | ||
Theorem | tfis 7569* | Transfinite Induction Schema. If all ordinal numbers less than a given number 𝑥 have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 20-Nov-2016.) |
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis2f 7570* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis2 7571* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfis3 7572* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ On → 𝜒) | ||
Theorem | tfisi 7573* | A transfinite induction scheme in "implicit" form where the induction is done on an object derived from the object of interest. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ On) & ⊢ ((𝜑 ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀𝑦(𝑆 ∈ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | tfinds 7574* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ On → (𝜒 → 𝜃)) & ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)) ⇒ ⊢ (𝐴 ∈ On → 𝜏) | ||
Theorem | tfindsg 7575* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal 𝐵 instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ On → 𝜓) & ⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃)) & ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑)) ⇒ ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏) | ||
Theorem | tfindsg2 7576* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal suc 𝐵 instead of zero. (Contributed by NM, 5-Jan-2005.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = suc 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝐵 ∈ On → 𝜓) & ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ 𝑦) → (𝜒 → 𝜃)) & ⊢ ((Lim 𝑥 ∧ 𝐵 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝜏) | ||
Theorem | tfindes 7577* | Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.) |
⊢ [∅ / 𝑥]𝜑 & ⊢ (𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) & ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 𝜑 → [𝑦 / 𝑥]𝜑)) ⇒ ⊢ (𝑥 ∈ On → 𝜑) | ||
Theorem | tfinds2 7578* | Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff 𝜏 is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝜏 → 𝜓) & ⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃))) & ⊢ (Lim 𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) ⇒ ⊢ (𝑥 ∈ On → (𝜏 → 𝜑)) | ||
Theorem | tfinds3 7579* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝜂 → 𝜓) & ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃))) & ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑))) ⇒ ⊢ (𝐴 ∈ On → (𝜂 → 𝜏)) | ||
Syntax | com 7580 | Extend class notation to include the class of natural numbers. |
class ω | ||
Definition | df-om 7581* |
Define the class of natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e., all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7582 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 9106, and ω can
then be defined per dfom3 9110 (the smallest inductive set) and dfom4 9112.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 6195. They are completely different from the natural numbers ℕ (df-nn 11639) that are a subset of the complex numbers defined much later in our development, although the two sets have analogous properties and operations defined on them. (Contributed by NM, 15-May-1994.) |
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom2 7582 | An alternate definition of the set of natural numbers ω. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the inner class builder of non-limit ordinal numbers (see nlimon 7566). (Contributed by NM, 1-Nov-2004.) |
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} | ||
Theorem | elom 7583* | Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9111. (Contributed by NM, 15-May-1994.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))) | ||
Theorem | omsson 7584 | Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ On | ||
Theorem | limomss 7585 | The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) |
⊢ (Lim 𝐴 → ω ⊆ 𝐴) | ||
Theorem | nnon 7586 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | ||
Theorem | nnoni 7587 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
⊢ 𝐴 ∈ ω ⇒ ⊢ 𝐴 ∈ On | ||
Theorem | nnord 7588 | A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
⊢ (𝐴 ∈ ω → Ord 𝐴) | ||
Theorem | ordom 7589 | Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ord ω | ||
Theorem | elnn 7590 | A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) | ||
Theorem | omon 7591 | The class of natural numbers ω is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43. (Contributed by NM, 10-May-1998.) |
⊢ (ω ∈ On ∨ ω = On) | ||
Theorem | omelon2 7592 | Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.) |
⊢ (ω ∈ V → ω ∈ On) | ||
Theorem | nnlim 7593 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴) | ||
Theorem | omssnlim 7594 | The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ω ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} | ||
Theorem | limom 7595 | Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
⊢ Lim ω | ||
Theorem | peano2b 7596 | A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.) |
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | ||
Theorem | nnsuc 7597* | A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.) |
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) | ||
Theorem | omsucne 7598 | A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.) |
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴) | ||
Theorem | ssnlim 7599* | An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) |
⊢ ((Ord 𝐴 ∧ 𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω) | ||
Theorem | omsinds 7600* | Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |