Home | Metamath
Proof Explorer Theorem List (p. 58 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | setlikespec 5701 | If is set-like in , then all predecessors classes of elements of exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Se | ||
Theorem | predidm 5702 | Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.) |
Theorem | predin 5703 | Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
Theorem | predun 5704 | Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
Theorem | preddif 5705 | Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.) |
Theorem | predep 5706 | The predecessor under the epsilon relationship is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | preddowncl 5707* | A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) |
Theorem | predpoirr 5708 | Given a partial ordering, is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) |
Theorem | predfrirr 5709 | Given a well-founded relationship, is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.) |
Theorem | pred0 5710 | The predecessor class over is always . (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.) |
Theorem | tz6.26 5711* | All nonempty (possibly proper) subclasses of , which has a well-founded relation , have -minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Se | ||
Theorem | tz6.26i 5712* | All nonempty (possibly proper) subclasses of , which has a well-founded relation , have -minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Se | ||
Theorem | wfi 5713* | The Principle of Well-Founded Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if is a subclass of a well-ordered class with the property that every element of whose inital segment is included in is itself equal to . (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Se | ||
Theorem | wfii 5714* | The Principle of Well-Founded Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if is a subclass of a well-ordered class with the property that every element of whose inital segment is included in is itself equal to . (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Se | ||
Theorem | wfisg 5715* | Well-Founded Induction Schema. If a property passes from all elements less than of a well-founded class to itself (induction hypothesis), then the property holds for all elements of . (Contributed by Scott Fenton, 11-Feb-2011.) |
Se | ||
Theorem | wfis 5716* | Well-Founded Induction Schema. If all elements less than a given set of the well-founded class have a property (induction hypothesis), then all elements of have that property. (Contributed by Scott Fenton, 29-Jan-2011.) |
Se | ||
Theorem | wfis2fg 5717* | Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
Se | ||
Theorem | wfis2f 5718* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
Se | ||
Theorem | wfis2g 5719* | Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
Se | ||
Theorem | wfis2 5720* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
Se | ||
Theorem | wfis3 5721* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
Se | ||
Syntax | word 5722 | Extend the definition of a wff to include the ordinal predicate. |
Syntax | con0 5723 | Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.) |
Syntax | wlim 5724 | Extend the definition of a wff to include the limit ordinal predicate. |
Syntax | csuc 5725 | Extend class notation to include the successor function. |
Definition | df-ord 5726 | Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the epsilon relation. Variant of definition of [BellMachover] p. 468. (Contributed by NM, 17-Sep-1993.) |
Definition | df-on 5727 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
Definition | df-lim 5728 | Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 5781, dflim3 7047, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.) |
Definition | df-suc 5729 | Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 7611). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 5800), so that the successor of any ordinal class is still an ordinal class (ordsuc 7014), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.) |
Theorem | ordeq 5730 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | elong 5731 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
Theorem | elon 5732 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
Theorem | eloni 5733 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
Theorem | elon2 5734 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
Theorem | limeq 5735 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordwe 5736 | Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) |
Theorem | ordtr 5737 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
Theorem | ordfr 5738 | Epsilon is well-founded on an ordinal class. (Contributed by NM, 22-Apr-1994.) |
Theorem | ordelss 5739 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
Theorem | trssord 5740 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
Theorem | ordirr 5741 | Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.) |
Theorem | nordeq 5742 | A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.) |
Theorem | ordn2lp 5743 | An ordinal class cannot be an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469. (Contributed by NM, 3-Apr-1994.) |
Theorem | tz7.5 5744* | A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36. (Contributed by NM, 18-Feb-2004.) (Revised by David Abernethy, 16-Mar-2011.) |
Theorem | ordelord 5745 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.) |
Theorem | tron 5746 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
Theorem | ordelon 5747 | An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
Theorem | onelon 5748 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.) |
Theorem | tz7.7 5749 | A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of [TakeutiZaring] p. 37. (Contributed by NM, 5-May-1994.) |
Theorem | ordelssne 5750 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 25-Nov-1995.) |
Theorem | ordelpss 5751 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 17-Jun-1998.) |
Theorem | ordsseleq 5752 | For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordin 5753 | The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.) |
Theorem | onin 5754 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
Theorem | ordtri3or 5755 | A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordtri1 5756 | A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ontri1 5757 | A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.) |
Theorem | ordtri2 5758 | A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.) |
Theorem | ordtri3 5759 | A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by JJ, 24-Sep-2021.) |
Theorem | ordtri3OLD 5760 | Obsolete proof of ordtri3 5759 as of 24-Sep-2021. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | ordtri4 5761 | A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | orddisj 5762 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
Theorem | onfr 5763 | The ordinal class is well-founded. This lemma is needed for ordon 6982 in order to eliminate the need for the Axiom of Regularity. (Contributed by NM, 17-May-1994.) |
Theorem | onelpss 5764 | Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
Theorem | onsseleq 5765 | Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
Theorem | onelss 5766 | 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.) |
Theorem | ordtr1 5767 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
Theorem | ordtr2 5768 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordtr3 5769 | Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.) |
Theorem | ordtr3OLD 5770 | Obsolete proof of ordtr3 5769 as of 24-Sep-2021. (Contributed by Mario Carneiro, 30-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | ontr1 5771 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.) |
Theorem | ontr2 5772 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
Theorem | ordunidif 5773 | 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.) |
Theorem | ordintdif 5774 | 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.) |
Theorem | onintss 5775* | 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.) |
Theorem | oneqmini 5776* | 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.) |
Theorem | ord0 5777 | The empty set is an ordinal class. (Contributed by NM, 11-May-1994.) |
Theorem | 0elon 5778 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
Theorem | ord0eln0 5779 | A nonempty ordinal contains the empty set. (Contributed by NM, 25-Nov-1995.) |
Theorem | on0eln0 5780 | An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
Theorem | dflim2 5781 | An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.) |
Theorem | inton 5782 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
Theorem | nlim0 5783 | The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | limord 5784 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
Theorem | limuni 5785 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
Theorem | limuni2 5786 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
Theorem | 0ellim 5787 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
Theorem | limelon 5788 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
Theorem | onn0 5789 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
Theorem | suceq 5790 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | elsuci 5791 | Membership in a successor. This one-way implication does not require that either or be sets. (Contributed by NM, 6-Jun-1994.) |
Theorem | elsucg 5792 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
Theorem | elsuc2g 5793 | Variant of membership in a successor, requiring that rather than be a set. (Contributed by NM, 28-Oct-2003.) |
Theorem | elsuc 5794 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
Theorem | elsuc2 5795 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
Theorem | nfsuc 5796 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
Theorem | elelsuc 5797 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
Theorem | sucel 5798* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
Theorem | suc0 5799 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
Theorem | sucprc 5800 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |