Home | Metamath
Proof Explorer Theorem List (p. 58 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | limord 5701 | A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → Ord 𝐴) | ||
Theorem | limuni 5702 | A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.) |
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | ||
Theorem | limuni2 5703 | The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.) |
⊢ (Lim 𝐴 → Lim ∪ 𝐴) | ||
Theorem | 0ellim 5704 | A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
⊢ (Lim 𝐴 → ∅ ∈ 𝐴) | ||
Theorem | limelon 5705 | A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) | ||
Theorem | onn0 5706 | The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.) |
⊢ On ≠ ∅ | ||
Theorem | suceq 5707 | Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) | ||
Theorem | elsuci 5708 | 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 5709 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc2g 5710 | Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | elsuc 5711 | Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | elsuc2 5712 | Membership in a successor. (Contributed by NM, 15-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) | ||
Theorem | nfsuc 5713 | Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 suc 𝐴 | ||
Theorem | elelsuc 5714 | Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | sucel 5715* | Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))) | ||
Theorem | suc0 5716 | The successor of the empty set. (Contributed by NM, 1-Feb-2005.) |
⊢ suc ∅ = {∅} | ||
Theorem | sucprc 5717 | A proper class is its own successor. (Contributed by NM, 3-Apr-1995.) |
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | ||
Theorem | unisuc 5718 | 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 5719 | 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 5720 | 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 5721 | 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 5722 | No successor is empty. (Contributed by NM, 3-Apr-1995.) |
⊢ suc 𝐴 ≠ ∅ | ||
Theorem | eqelsuc 5723 | A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵) | ||
Theorem | iunsuc 5724* | 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 5725 | 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 | suctrOLD 5726 | Obsolete proof of suctr 5725 as of 24-Sep-2021. (Contributed by Alan Sare, 11-Apr-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
Theorem | trsuc 5727 | 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 5728 | A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.) |
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | ordsssuc 5729 | A subset of an ordinal belongs to its successor. (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | onsssuc 5730 | A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | ||
Theorem | ordsssuc2 5731 | 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 5732 | 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 5733 | 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 | ordnbtwnOLD 5734 | Obsolete proof of ordnbtwn 5733 as of 24-Sep-2021. (Contributed by NM, 21-Jun-1998.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | ||
Theorem | onnbtwn 5735 | 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 5736 | 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 5737 | Ordinal derived from its successor. (Contributed by NM, 20-May-1998.) |
⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) | ||
Theorem | orduniss 5738 | An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.) |
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | ordtri2or 5739 | A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or2 5740 | A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtri2or3 5741 | A consequence of total ordering for ordinal classes. Similar to ordtri2or2 5740. (Contributed by David Moews, 1-May-2017.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) | ||
Theorem | ordelinel 5742 | 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 | ordelinelOLD 5743 | Obsolete proof of ordelinel 5742 as of 24-Sep-2021. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) | ||
Theorem | ordssun 5744 | Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.) |
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶))) | ||
Theorem | ordequn 5745 | 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 5746 | 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 5747 | A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) | ||
Theorem | suc11 5748 | 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 5749 | An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Ord 𝐴 | ||
Theorem | ontrci 5750 | An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ Tr 𝐴 | ||
Theorem | onirri 5751 | 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 5752 | 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 5753 | A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴) | ||
Theorem | onssneli 5754 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | onssnel2i 5755 | An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | onelini 5756 | An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴)) | ||
Theorem | oneluni 5757 | An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴) | ||
Theorem | onunisuci 5758 | An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐴 ∈ On ⇒ ⊢ ∪ suc 𝐴 = 𝐴 | ||
Theorem | onsseli 5759 | Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | onun2i 5760 | The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) |
⊢ 𝐴 ∈ On & ⊢ 𝐵 ∈ On ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ On | ||
Theorem | unizlim 5761 | An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | ||
Theorem | on0eqel 5762 | An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.) |
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) | ||
Theorem | snsn0non 5763 | The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 6961). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 5764. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ ¬ {{∅}} ∈ On | ||
Theorem | onxpdisj 5764 | 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 5763. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (On ∩ (V × V)) = ∅ | ||
Theorem | onnev 5765 | 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 5766 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩𝑥𝜑) | ||
Theorem | iotajust 5767* | Soundness justification theorem for df-iota 5768. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-iota 5768* |
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 5779);
otherwise, it evaluates to the empty set (see iotanul 5783). 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 6524 (or iotacl 5791 for unbounded iota), as demonstrated in the proof of supub 8248. This can be easier than applying riotasbc 6526 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 5769* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | nfiota1 5770 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥𝜑) | ||
Theorem | nfiotad 5771 | Deduction version of nfiota 5772. (Contributed by NM, 18-Feb-2013.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓)) | ||
Theorem | nfiota 5772 | Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥(℩𝑦𝜑) | ||
Theorem | cbviota 5773 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | cbviotav 5774* | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) | ||
Theorem | sb8iota 5775 | Variable substitution in description binder. Compare sb8eu 2491. (Contributed by NM, 18-Mar-2013.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | iotaeq 5776 | Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑)) | ||
Theorem | iotabi 5777 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | ||
Theorem | uniabio 5778* | 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 5779* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) | ||
Theorem | iotauni 5780 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑}) | ||
Theorem | iotaint 5781 | Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | iota1 5782 | Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥)) | ||
Theorem | iotanul 5783 | Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅) | ||
Theorem | iotassuni 5784 | The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑} | ||
Theorem | iotaex 5785 | Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (℩𝑥𝜑) ∈ V | ||
Theorem | iota4 5786 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) | ||
Theorem | iota4an 5787 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑) | ||
Theorem | iota5 5788* | A method for computing iota. (Contributed by NM, 17-Sep-2013.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴) | ||
Theorem | iotabidv 5789* | Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) | ||
Theorem | iotabii 5790 | Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) | ||
Theorem | iotacl 5791 |
Membership law for descriptions.
This can useful for expanding an unbounded iota-based definition (see df-iota 5768). If you have a bounded iota-based definition, riotacl2 6524 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑}) | ||
Theorem | iota2df 5792 | A condition that allows us to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
Theorem | iota2d 5793* | A condition that allows us to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → ∃!𝑥𝜓) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵)) | ||
Theorem | iota2 5794* | The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴)) | ||
Theorem | sniota 5795 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)}) | ||
Theorem | dfiota4 5796 | The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) |
⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅) | ||
Theorem | csbiota 5797* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦𝜑) = (℩𝑦[𝐴 / 𝑥]𝜑) | ||
Syntax | wfun 5798 | Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.) |
wff Fun 𝐴 | ||
Syntax | wfn 5799 | Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.) |
wff 𝐴 Fn 𝐵 | ||
Syntax | wf 5800 | Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.) |
wff 𝐹:𝐴⟶𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |