Home | Metamath
Proof Explorer Theorem List (p. 86 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 | tc2 8501* | A variant of the definition of the transitive closure function, using instead the smallest transitive set containing 𝐴 as a member, gives almost the same set, except that 𝐴 itself must be added because it is not usually a member of (TC‘𝐴) (and it is never a member if 𝐴 is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((TC‘𝐴) ∪ {𝐴}) = ∩ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} | ||
Theorem | tcsni 8502 | The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (TC‘{𝐴}) = ((TC‘𝐴) ∪ {𝐴}) | ||
Theorem | tcss 8503 | The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ⊆ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcel 8504 | The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcidm 8505 | The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (TC‘(TC‘𝐴)) = (TC‘𝐴) | ||
Theorem | tc0 8506 | The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (TC‘∅) = ∅ | ||
Theorem | tc00 8507 | The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Syntax | cr1 8508 | Extend class definition to include the cumulative hierarchy of sets function. |
class 𝑅1 | ||
Syntax | crnk 8509 | Extend class definition to include rank function. |
class rank | ||
Definition | df-r1 8510 | Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 8537). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 8514, r1suc 8516, and r1lim 8518. Theorem r1val1 8532 shows a recursive definition that works for all values, and theorems r1val2 8583 and r1val3 8584 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95). (Contributed by NM, 2-Sep-2003.) |
⊢ 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅) | ||
Definition | df-rank 8511* | Define the rank function. See rankval 8562, rankval2 8564, rankval3 8586, or rankval4 8613 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 8579 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8582. (Contributed by NM, 11-Oct-2003.) |
⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) | ||
Theorem | r1funlim 8512 | The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 8513 avoids ax-rep 4699.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1) | ||
Theorem | r1fnon 8513 | The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ 𝑅1 Fn On | ||
Theorem | r10 8514 | Value of the cumulative hierarchy of sets function at ∅. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ (𝑅1‘∅) = ∅ | ||
Theorem | r1sucg 8515 | Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴)) | ||
Theorem | r1suc 8516 | Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴)) | ||
Theorem | r1limg 8517* | Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥)) | ||
Theorem | r1lim 8518* | Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥)) | ||
Theorem | r1fin 8519 | The first ω levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.) |
⊢ (𝐴 ∈ ω → (𝑅1‘𝐴) ∈ Fin) | ||
Theorem | r1sdom 8520 | Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺ (𝑅1‘𝐴)) | ||
Theorem | r111 8521 | The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.) |
⊢ 𝑅1:On–1-1→V | ||
Theorem | r1tr 8522 | The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ Tr (𝑅1‘𝐴) | ||
Theorem | r1tr2 8523 | The union of a cumulative hierarchy of sets at ordinal 𝐴 is a subset of the hierarchy at 𝐴. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011.) |
⊢ ∪ (𝑅1‘𝐴) ⊆ (𝑅1‘𝐴) | ||
Theorem | r1ordg 8524 | Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) |
⊢ (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵))) | ||
Theorem | r1ord3g 8525 | Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.) |
⊢ ((𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵))) | ||
Theorem | r1ord 8526 | Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵))) | ||
Theorem | r1ord2 8527 | Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 22-Sep-2003.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵))) | ||
Theorem | r1ord3 8528 | Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵))) | ||
Theorem | r1sssuc 8529 | The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.) |
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴)) | ||
Theorem | r1pwss 8530 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) | ||
Theorem | r1sscl 8531 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵)) | ||
Theorem | r1val1 8532* | The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 (𝑅1‘𝑥)) | ||
Theorem | tz9.12lem1 8533* | Lemma for tz9.12 8536. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)}) ⇒ ⊢ (𝐹 “ 𝐴) ⊆ On | ||
Theorem | tz9.12lem2 8534* | Lemma for tz9.12 8536. (Contributed by NM, 22-Sep-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)}) ⇒ ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On | ||
Theorem | tz9.12lem3 8535* | Lemma for tz9.12 8536. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)}) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝐴 ∈ (𝑅1‘suc suc ∪ (𝐹 “ 𝐴))) | ||
Theorem | tz9.12 8536* | A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 8533 through tz9.12lem3 8535. (Contributed by NM, 22-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦)) | ||
Theorem | tz9.13 8537* | Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥) | ||
Theorem | tz9.13g 8538* | Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 8537 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥)) | ||
Theorem | rankwflemb 8539* | Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥)) | ||
Theorem | rankf 8540 | The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.) |
⊢ rank:∪ (𝑅1 “ On)⟶On | ||
Theorem | rankon 8541 | The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.) |
⊢ (rank‘𝐴) ∈ On | ||
Theorem | r1elwf 8542 | Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐴 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | rankvalb 8543* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8562 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)}) | ||
Theorem | rankr1ai 8544 | One direction of rankr1a 8582. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵) | ||
Theorem | rankvaln 8545 | Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 8559, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅) | ||
Theorem | rankidb 8546 | Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ (𝑅1‘suc (rank‘𝐴))) | ||
Theorem | rankdmr1 8547 | A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ (rank‘𝐴) ∈ dom 𝑅1 | ||
Theorem | rankr1ag 8548 | A version of rankr1a 8582 that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) | ||
Theorem | rankr1bg 8549 | A relationship between rank and 𝑅1. See rankr1ag 8548 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵)) | ||
Theorem | r1rankidb 8550 | Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴))) | ||
Theorem | r1elssi 8551 | The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 8552 that doesn't need 𝐴 to be a set. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) | ||
Theorem | r1elss 8552 | The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝐴 ⊆ ∪ (𝑅1 “ On)) | ||
Theorem | pwwf 8553 | A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫 𝐴 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | sswf 8554 | A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | snwf 8555 | A singleton is well-founded if its element is. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝐴} ∈ ∪ (𝑅1 “ On)) | ||
Theorem | unwf 8556 | A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) ↔ (𝐴 ∪ 𝐵) ∈ ∪ (𝑅1 “ On)) | ||
Theorem | prwf 8557 | An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → {𝐴, 𝐵} ∈ ∪ (𝑅1 “ On)) | ||
Theorem | opwf 8558 | An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → 〈𝐴, 𝐵〉 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | unir1 8559 | The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 8-Jun-2013.) |
⊢ ∪ (𝑅1 “ On) = V | ||
Theorem | jech9.3 8560 | Every set belongs to some value of the cumulative hierarchy of sets function 𝑅1, i.e. the indexed union of all values of 𝑅1 is the universe. Lemma 9.3 of [Jech] p. 71. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 8-Jun-2013.) |
⊢ ∪ 𝑥 ∈ On (𝑅1‘𝑥) = V | ||
Theorem | rankwflem 8561* | Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 8538 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥)) | ||
Theorem | rankval 8562* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). (Contributed by NM, 24-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)} | ||
Theorem | rankvalg 8563* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8562 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)}) | ||
Theorem | rankval2 8564* | Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478. (Contributed by NM, 8-Oct-2003.) |
⊢ (𝐴 ∈ 𝐵 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (𝑅1‘𝑥)}) | ||
Theorem | uniwf 8565 | A union is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝐴 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | rankr1clem 8566 | Lemma for rankr1c 8567. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴))) | ||
Theorem | rankr1c 8567 | A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)))) | ||
Theorem | rankidn 8568 | A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ (𝑅1‘(rank‘𝐴))) | ||
Theorem | rankpwi 8569 | The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 3-Jun-2013.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝒫 𝐴) = suc (rank‘𝐴)) | ||
Theorem | rankelb 8570 | The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝐴 ∈ 𝐵 → (rank‘𝐴) ∈ (rank‘𝐵))) | ||
Theorem | wfelirr 8571 | A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 8388. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | rankval3b 8572* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥}) | ||
Theorem | ranksnb 8573 | The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘{𝐴}) = suc (rank‘𝐴)) | ||
Theorem | rankonidlem 8574 | Lemma for rankonid 8575. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.) |
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴)) | ||
Theorem | rankonid 8575 | The rank of an ordinal number is itself. Proposition 9.18 of [TakeutiZaring] p. 79 and its converse. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ dom 𝑅1 ↔ (rank‘𝐴) = 𝐴) | ||
Theorem | onwf 8576 | The ordinals are all well-founded. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ On ⊆ ∪ (𝑅1 “ On) | ||
Theorem | onssr1 8577 | Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) | ||
Theorem | rankr1g 8578 | A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵)))) | ||
Theorem | rankid 8579 | Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ (𝑅1‘suc (rank‘𝐴)) | ||
Theorem | rankr1 8580 | A relationship between the rank function and the cumulative hierarchy of sets function 𝑅1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc 𝐵))) | ||
Theorem | ssrankr1 8581 | A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets 𝑅1. Proposition 9.15(3) of [TakeutiZaring] p. 79. (Contributed by NM, 8-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ On → (𝐵 ⊆ (rank‘𝐴) ↔ ¬ 𝐴 ∈ (𝑅1‘𝐵))) | ||
Theorem | rankr1a 8582 | A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 8581 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 8610 for the subset version. (Contributed by Raph Levien, 29-May-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) | ||
Theorem | r1val2 8583* | The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.) |
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) = {𝑥 ∣ (rank‘𝑥) ∈ 𝐴}) | ||
Theorem | r1val3 8584* | The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 {𝑦 ∣ (rank‘𝑦) ∈ 𝑥}) | ||
Theorem | rankel 8585 | The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 → (rank‘𝐴) ∈ (rank‘𝐵)) | ||
Theorem | rankval3 8586* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥} | ||
Theorem | bndrank 8587* | Any class whose elements have bounded rank is a set. Proposition 9.19 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.) |
⊢ (∃𝑥 ∈ On ∀𝑦 ∈ 𝐴 (rank‘𝑦) ⊆ 𝑥 → 𝐴 ∈ V) | ||
Theorem | unbndrank 8588* | The elements of a proper class have unbounded rank. Exercise 2 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.) |
⊢ (¬ 𝐴 ∈ V → ∀𝑥 ∈ On ∃𝑦 ∈ 𝐴 𝑥 ∈ (rank‘𝑦)) | ||
Theorem | rankpw 8589 | The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 22-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘𝒫 𝐴) = suc (rank‘𝐴) | ||
Theorem | ranklim 8590 | The rank of a set belongs to a limit ordinal iff the rank of its power set does. (Contributed by NM, 18-Sep-2006.) |
⊢ (Lim 𝐵 → ((rank‘𝐴) ∈ 𝐵 ↔ (rank‘𝒫 𝐴) ∈ 𝐵)) | ||
Theorem | r1pw 8591 | A stronger property of 𝑅1 than rankpw 8589. The latter merely proves that 𝑅1 of the successor is a power set, but here we prove that if 𝐴 is in the cumulative hierarchy, then 𝒫 𝐴 is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵))) | ||
Theorem | r1pwALT 8592 | Alternate shorter proof of r1pw 8591 based on the additional axioms ax-reg 8380 and ax-inf2 8421. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵))) | ||
Theorem | r1pwcl 8593 | The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
⊢ (Lim 𝐵 → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘𝐵))) | ||
Theorem | rankssb 8594 | The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝐴 ⊆ 𝐵 → (rank‘𝐴) ⊆ (rank‘𝐵))) | ||
Theorem | rankss 8595 | The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 → (rank‘𝐴) ⊆ (rank‘𝐵)) | ||
Theorem | rankunb 8596 | The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))) | ||
Theorem | rankprb 8597 | The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘{𝐴, 𝐵}) = suc ((rank‘𝐴) ∪ (rank‘𝐵))) | ||
Theorem | rankopb 8598 | The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘〈𝐴, 𝐵〉) = suc suc ((rank‘𝐴) ∪ (rank‘𝐵))) | ||
Theorem | rankuni2b 8599* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) | ||
Theorem | ranksn 8600 | The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘{𝐴}) = suc (rank‘𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |