Home | Metamath
Proof Explorer Theorem List (p. 63 of 463) | < 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-29023) |
Hilbert Space Explorer
(29024-30546) |
Users' Mathboxes
(30547-46209) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | setlikespec 6201 | If 𝑅 is set-like in 𝐴, then all predecessor classes of elements of 𝐴 exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V) | ||
Theorem | predidm 6202 | Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋) | ||
Theorem | predin 6203 | Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predun 6204 | Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | preddif 6205 | Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.) |
⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predep 6206 | The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝑋 ∈ 𝐵 → Pred( E , 𝐴, 𝑋) = (𝐴 ∩ 𝑋)) | ||
Theorem | trpred 6207 | The class of predecessors of an element of a transitive class for the membership relation is that element. (Contributed by BJ, 12-Oct-2024.) |
⊢ ((Tr 𝐴 ∧ 𝑋 ∈ 𝐴) → Pred( E , 𝐴, 𝑋) = 𝑋) | ||
Theorem | preddowncl 6208* | A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | predpoirr 6209 | Given a partial ordering, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) |
⊢ (𝑅 Po 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋)) | ||
Theorem | predfrirr 6210 | Given a well-founded relation, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.) |
⊢ (𝑅 Fr 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋)) | ||
Theorem | pred0 6211 | The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.) |
⊢ Pred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | frpomin 6212* | Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9390 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | frpomin2 6213* | Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9390 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) | ||
Theorem | frpoind 6214* | The principle of well-founded induction over a partial order. This theorem is a version of frind 9391 that does not require the axiom of infinity and can be used to prove wfi 6221 and tfi 7651. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frpoinsg 6215* | Well-Founded Induction Schema (variant). If a property passes from all elements less than 𝑦 of a well-founded set-like partial order class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑦 ∈ 𝐴) → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins2fg 6216* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins2g 6217* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins3g 6218* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑥)𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒) | ||
Theorem | tz6.26 6219* | All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | tz6.26i 6220* | All nonempty subclasses of a class having a well-ordered set-like 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.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | wfi 6221* | The Principle of Well-Ordered 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.) |
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | wfii 6222* | The Principle of Well-Ordered 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.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵)) → 𝐴 = 𝐵) | ||
Theorem | wfisg 6223* | Well-Ordered Induction Schema. If a property passes from all elements less than 𝑦 of a well-ordered class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis 6224* | Well-Ordered Induction Schema. If all elements less than a given set 𝑥 of the well-ordered class 𝐴 have a property (induction hypothesis), then all elements of 𝐴 have that property. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | wfis2fg 6225* | Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis2f 6226* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | wfis2g 6227* | Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis2 6228* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | wfis3 6229* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝜒) | ||
Syntax | word 6230 | Extend the definition of a wff to include the ordinal predicate. |
wff Ord 𝐴 | ||
Syntax | con0 6231 | 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.) |
class On | ||
Syntax | wlim 6232 | Extend the definition of a wff to include the limit ordinal predicate. |
wff Lim 𝐴 | ||
Syntax | csuc 6233 | Extend class notation to include the successor function. |
class suc 𝐴 | ||
Definition | df-ord 6234 |
Define the ordinal predicate, which is true for a class that is transitive
and is well-ordered by the membership relation. Variant of definition of
[BellMachover] p. 468.
Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively. (Contributed by NM, 17-Sep-1993.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | ||
Definition | df-on 6235 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
⊢ On = {𝑥 ∣ Ord 𝑥} | ||
Definition | df-lim 6236 | 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 6287, dflim3 7645, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | ||
Definition | df-suc 6237 | Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8279). 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 6306), so that the successor of any ordinal class is still an ordinal class (ordsuc 7612), 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.) |
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | ||
Theorem | ordeq 6238 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | ||
Theorem | elong 6239 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) | ||
Theorem | elon 6240 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) | ||
Theorem | eloni 6241 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → Ord 𝐴) | ||
Theorem | elon2 6242 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | limeq 6243 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) | ||
Theorem | ordwe 6244 | Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → E We 𝐴) | ||
Theorem | ordtr 6245 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → Tr 𝐴) | ||
Theorem | ordfr 6246 | Membership is well-founded on an ordinal class. In other words, an ordinal class is well-founded. (Contributed by NM, 22-Apr-1994.) |
⊢ (Ord 𝐴 → E Fr 𝐴) | ||
Theorem | ordelss 6247 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | ||
Theorem | trssord 6248 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) | ||
Theorem | ordirr 6249 | No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. 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.) |
⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | nordeq 6250 | A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ 𝐵) | ||
Theorem | ordn2lp 6251 | 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.) |
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)) | ||
Theorem | tz7.5 6252* | 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.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) | ||
Theorem | ordelord 6253 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
Theorem | tron 6254 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
⊢ Tr On | ||
Theorem | ordelon 6255 | An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
Theorem | onelon 6256 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
Theorem | tz7.7 6257 | 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.) |
⊢ ((Ord 𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))) | ||
Theorem | ordelssne 6258 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 25-Nov-1995.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
Theorem | ordelpss 6259 | For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 17-Jun-1998.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | ordsseleq 6260 | For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | ordin 6261 | The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) | ||
Theorem | onin 6262 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On) | ||
Theorem | ordtri3or 6263 | 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.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
Theorem | ordtri1 6264 | A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) | ||
Theorem | ontri1 6265 | A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) | ||
Theorem | ordtri2 6266 | A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
Theorem | ordtri3 6267 | 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.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴))) | ||
Theorem | ordtri4 6268 | A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵))) | ||
Theorem | orddisj 6269 | An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) | ||
Theorem | onfr 6270 | The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7580 (through epweon 7579) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.) |
⊢ E Fr On | ||
Theorem | onelpss 6271 | Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))) | ||
Theorem | onsseleq 6272 | Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | onelss 6273 | 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 6274 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr2 6275 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordtr3 6276 | Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | ||
Theorem | ontr1 6277 | Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ontr2 6278 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | ||
Theorem | ordunidif 6279 | 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 6280 | 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 6281* | 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 6282* | 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 6283 | The empty set is an ordinal class. (Contributed by NM, 11-May-1994.) |
⊢ Ord ∅ | ||
Theorem | 0elon 6284 | The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.) |
⊢ ∅ ∈ On | ||
Theorem | ord0eln0 6285 | A nonempty ordinal contains the empty set. (Contributed by NM, 25-Nov-1995.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | on0eln0 6286 | An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | dflim2 6287 | An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Theorem | inton 6288 | The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.) |
⊢ ∩ On = ∅ | ||
Theorem | nlim0 6289 | 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 6290 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → Ord 𝐴) | ||
Theorem | limuni 6291 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
Theorem | limuni2 6292 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
Theorem | 0ellim 6293 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
Theorem | limelon 6294 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
Theorem | onn0 6295 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
⊢ On ≠ ∅ | ||
Theorem | suceq 6296 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
Theorem | elsuci 6297 | 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 6298 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc2g 6299 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc 6300 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |