![]() |
Metamath
Proof Explorer Theorem List (p. 61 of 435) | < 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-28331) |
![]() (28332-29856) |
![]() (29857-43448) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ordtri4 6001 | A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵))) | ||
Theorem | orddisj 6002 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) | ||
Theorem | onfr 6003 | The ordinal class is well-founded. This lemma is needed for ordon 7245 in order to eliminate the need for the Axiom of Regularity. (Contributed by NM, 17-May-1994.) |
⊢ E Fr On | ||
Theorem | onelpss 6004 | Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
Theorem | onsseleq 6005 | Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | onelss 6006 | An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtr1 6007 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr2 6008 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr3 6009 | Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | ||
Theorem | ontr1 6010 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ontr2 6011 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordunidif 6012 | The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) | ||
Theorem | ordintdif 6013 | If 𝐵 is smaller than 𝐴, then it equals the intersection of the difference. Exercise 11 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 = ∩ (𝐴 ∖ 𝐵)) | ||
Theorem | onintss 6014* | If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴)) | ||
Theorem | oneqmini 6015* | A way to show that an ordinal number equals the minimum of a 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 | ord0 6016 | The empty set is an ordinal class. (Contributed by NM, 11-May-1994.) |
⊢ Ord ∅ | ||
Theorem | 0elon 6017 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
⊢ ∅ ∈ On | ||
Theorem | ord0eln0 6018 | A nonempty ordinal contains the empty set. (Contributed by NM, 25-Nov-1995.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | on0eln0 6019 | An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | dflim2 6020 | An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Theorem | inton 6021 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
⊢ ∩ On = ∅ | ||
Theorem | nlim0 6022 | The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ¬ Lim ∅ | ||
Theorem | limord 6023 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → Ord 𝐴) | ||
Theorem | limuni 6024 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
Theorem | limuni2 6025 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
Theorem | 0ellim 6026 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
Theorem | limelon 6027 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
Theorem | onn0 6028 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
⊢ On ≠ ∅ | ||
Theorem | suceq 6029 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
Theorem | elsuci 6030 | Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsucg 6031 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc2g 6032 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc 6033 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsuc2 6034 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) | ||
Theorem | nfsuc 6035 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 suc 𝐴 | ||
Theorem | elelsuc 6036 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | sucel 6037* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) | ||
Theorem | suc0 6038 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
⊢ suc ∅ = {∅} | ||
Theorem | sucprc 6039 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | ||
Theorem | unisuc 6040 | A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴) | ||
Theorem | sssucid 6041 | A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.) |
⊢ 𝐴 ⊆ suc 𝐴 | ||
Theorem | sucidg 6042 | Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) | ||
Theorem | sucid 6043 | A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ suc 𝐴 | ||
Theorem | nsuceq0 6044 | No successor is empty. (Contributed by NM, 3-Apr-1995.) |
⊢ suc 𝐴 ≠ ∅ | ||
Theorem | eqelsuc 6045 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | iunsuc 6046* | Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ suc 𝐴𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶) | ||
Theorem | suctr 6047 | The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
Theorem | trsuc 6048 | A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴) | ||
Theorem | trsucss 6049 | A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.) |
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | ordsssuc 6050 | A subset of an ordinal belongs to its successor. (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | onsssuc 6051 | A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | ordsssuc2 6052 | An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | onmindif 6053 | When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ On) → 𝐵 ∈ ∩ (𝐴 ∖ suc 𝐵)) | ||
Theorem | ordnbtwn 6054 | There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41. (Contributed by NM, 21-Jun-1998.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | ||
Theorem | onnbtwn 6055 | There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41. (Contributed by NM, 9-Jun-1994.) |
⊢ (𝐴 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | ||
Theorem | sucssel 6056 | A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵)) | ||
Theorem | orddif 6057 | Ordinal derived from its successor. (Contributed by NM, 20-May-1998.) |
⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) | ||
Theorem | orduniss 6058 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | ordtri2or 6059 | A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or2 6060 | A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or3 6061 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 6060. (Contributed by David Moews, 1-May-2017.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) | ||
Theorem | ordelinel 6062 | The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) | ||
Theorem | ordssun 6063 | Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶))) | ||
Theorem | ordequn 6064 | The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 = (𝐵 ∪ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | ordun 6065 | The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∪ 𝐵)) | ||
Theorem | ordunisssuc 6066 | A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | suc11 6067 | The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194. (Contributed by NM, 3-Sep-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onordi 6068 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Ord 𝐴 | ||
Theorem | ontrci 6069 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Tr 𝐴 | ||
Theorem | onirri 6070 | An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ¬ 𝐴 ∈ 𝐴 | ||
Theorem | oneli 6071 | A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ On) | ||
Theorem | onelssi 6072 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
Theorem | onssneli 6073 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | onssnel2i 6074 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | onelini 6075 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
Theorem | oneluni 6076 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
Theorem | onunisuci 6077 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
Theorem | onsseli 6078 | Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | onun2i 6079 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
Theorem | unizlim 6080 | An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | ||
Theorem | on0eqel 6081 | An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.) |
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) | ||
Theorem | snsn0non 6082 | The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7331). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6083. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ¬ {{∅}} ∈ On | ||
Theorem | onxpdisj 6083 | Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non 6082. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (On ∩ (V × V)) = ∅ | ||
Theorem | onnev 6084 | The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.) |
⊢ On ≠ V | ||
Syntax | cio 6085 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩𝑥𝜑) | ||
Theorem | iotajust 6086* | Soundness justification theorem for df-iota 6087. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-iota 6087* |
Define Russell's definition description binder, which can be read as
"the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains
𝑥 as a free variable. Our definition
is meaningful only when there
is exactly one 𝑥 such that 𝜑 is true (see iotaval 6098);
otherwise, it evaluates to the empty set (see iotanul 6102). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use riotacl2 6880 (or iotacl 6110 for unbounded iota), as demonstrated in the proof of supub 8635. This can be easier than applying riotasbc 6882 or a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfiota2 6088* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | nfiota1 6089 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥𝜑) | ||
Theorem | nfiotad 6090 | Deduction version of nfiota 6091. (Contributed by NM, 18-Feb-2013.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
Theorem | nfiota 6091 | Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
Theorem | cbviota 6092 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | cbviotav 6093* | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | sb8iota 6094 | Variable substitution in description binder. Compare sb8eu 2689. (Contributed by NM, 18-Mar-2013.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | iotaeq 6095 | Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑)) | ||
Theorem | iotabi 6096 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | ||
Theorem | uniabio 6097* | Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∪ {𝑥 ∣ 𝜑} = 𝑦) | ||
Theorem | iotaval 6098* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) | ||
Theorem | iotauni 6099 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑}) | ||
Theorem | iotaint 6100 | Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |