![]() |
Metamath
Proof Explorer Theorem List (p. 91 of 444) | < 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-28489) |
![]() (28490-30014) |
![]() (30015-44305) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | r1ord 9001 | 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 9002 | 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 9003 | 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 9004 | 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 9005 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) | ||
Theorem | r1sscl 9006 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵)) | ||
Theorem | r1val1 9007* | 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 9008* | Lemma for tz9.12 9011. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)}) ⇒ ⊢ (𝐹 “ 𝐴) ⊆ On | ||
Theorem | tz9.12lem2 9009* | Lemma for tz9.12 9011. (Contributed by NM, 22-Sep-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)}) ⇒ ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On | ||
Theorem | tz9.12lem3 9010* | Lemma for tz9.12 9011. (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 9011* | 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 9008 through tz9.12lem3 9010. (Contributed by NM, 22-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦)) | ||
Theorem | tz9.13 9012* | 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 9013* | Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9012 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥)) | ||
Theorem | rankwflemb 9014* | 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 9015 | 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 9016 | 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 9017 | 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 9018* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9037 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 9019 | One direction of rankr1a 9057. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵) | ||
Theorem | rankvaln 9020 | Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 9034, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.) |
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅) | ||
Theorem | rankidb 9021 | 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 9022 | A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ (rank‘𝐴) ∈ dom 𝑅1 | ||
Theorem | rankr1ag 9023 | A version of rankr1a 9057 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 9024 | A relationship between rank and 𝑅1. See rankr1ag 9023 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵)) | ||
Theorem | r1rankidb 9025 | 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 9026 | The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 9027 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 9027 | 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 9028 | 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 9029 | A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On)) | ||
Theorem | snwf 9030 | 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 9031 | 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 9032 | 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 9033 | 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 9034 | 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 9035 | 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 9036* | Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 9013 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥)) | ||
Theorem | rankval 9037* | 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 9038* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9037 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)}) | ||
Theorem | rankval2 9039* | 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 9040 | 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 9041 | Lemma for rankr1c 9042. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴))) | ||
Theorem | rankr1c 9042 | 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 9043 | 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 9044 | 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 9045 | 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 9046 | A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 8854. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | rankval3b 9047* | 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 9048 | 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 9049 | Lemma for rankonid 9050. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.) |
⊢ (𝐴 ∈ dom 𝑅1 → (𝐴 ∈ ∪ (𝑅1 “ On) ∧ (rank‘𝐴) = 𝐴)) | ||
Theorem | rankonid 9050 | 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 9051 | 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 9052 | 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 9053 | 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 9054 | 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 9055 | 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 9056 | 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 9057 | A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 9056 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 9085 for the subset version. (Contributed by Raph Levien, 29-May-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) | ||
Theorem | r1val2 9058* | 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 9059* | 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 9060 | 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 9061* | 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 9062* | 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 9063* | 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 9064 | 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 9065 | 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 9066 | A stronger property of 𝑅1 than rankpw 9064. 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 9067 | Alternate shorter proof of r1pw 9066 based on the additional axioms ax-reg 8849 and ax-inf2 8896. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc 𝐵))) | ||
Theorem | r1pwcl 9068 | 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 9069 | 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 9070 | 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 9071 | 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 9072 | 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 9073 | 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 9074* | 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 9075 | 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‘𝐴) | ||
Theorem | rankuni2 9076* | The rank of a union. Part of Theorem 15.17(iv) of [Monk1] p. 112. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) | ||
Theorem | rankun 9077 | The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by NM, 26-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)) | ||
Theorem | rankpr 9078 | The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (rank‘{𝐴, 𝐵}) = suc ((rank‘𝐴) ∪ (rank‘𝐵)) | ||
Theorem | rankop 9079 | The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 13-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (rank‘〈𝐴, 𝐵〉) = suc suc ((rank‘𝐴) ∪ (rank‘𝐵)) | ||
Theorem | r1rankid 9080 | Any set is a subset of the hierarchy of its rank. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (𝑅1‘(rank‘𝐴))) | ||
Theorem | rankeq0b 9081 | A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 = ∅ ↔ (rank‘𝐴) = ∅)) | ||
Theorem | rankeq0 9082 | A set is empty iff its rank is empty. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = ∅ ↔ (rank‘𝐴) = ∅) | ||
Theorem | rankr1id 9083 | The rank of the hierarchy of an ordinal number is itself. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ dom 𝑅1 ↔ (rank‘(𝑅1‘𝐴)) = 𝐴) | ||
Theorem | rankuni 9084 | The rank of a union. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (rank‘∪ 𝐴) = ∪ (rank‘𝐴) | ||
Theorem | rankr1b 9085 | A relationship between rank and 𝑅1. See rankr1a 9057 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵)) | ||
Theorem | ranksuc 9086 | The rank of a successor. (Contributed by NM, 18-Sep-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘suc 𝐴) = suc (rank‘𝐴) | ||
Theorem | rankuniss 9087 | Upper bound of the rank of a union. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 30-Nov-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘∪ 𝐴) ⊆ (rank‘𝐴) | ||
Theorem | rankval4 9088* | The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of [Jech] p. 72. Also a special case of Theorem 7V(b) of [Enderton] p. 204. (Contributed by NM, 12-Oct-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rank‘𝐴) = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) | ||
Theorem | rankbnd 9089* | The rank of a set is bounded by a bound for the successor of its members. (Contributed by NM, 18-Sep-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝐵 ↔ (rank‘𝐴) ⊆ 𝐵) | ||
Theorem | rankbnd2 9090* | The rank of a set is bounded by the successor of a bound for its members. (Contributed by NM, 15-Sep-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ On → (∀𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ 𝐵 ↔ (rank‘𝐴) ⊆ suc 𝐵)) | ||
Theorem | rankc1 9091* | A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ (rank‘∪ 𝐴) ↔ (rank‘𝐴) = (rank‘∪ 𝐴)) | ||
Theorem | rankc2 9092* | A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘∪ 𝐴) → (rank‘𝐴) = suc (rank‘∪ 𝐴)) | ||
Theorem | rankelun 9093 | Rank membership is inherited by union. (Contributed by NM, 18-Sep-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐶 ∪ 𝐷))) | ||
Theorem | rankelpr 9094 | Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘{𝐴, 𝐵}) ∈ (rank‘{𝐶, 𝐷})) | ||
Theorem | rankelop 9095 | Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (((rank‘𝐴) ∈ (rank‘𝐶) ∧ (rank‘𝐵) ∈ (rank‘𝐷)) → (rank‘〈𝐴, 𝐵〉) ∈ (rank‘〈𝐶, 𝐷〉)) | ||
Theorem | rankxpl 9096 | A lower bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) | ||
Theorem | rankxpu 9097 | An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵)) | ||
Theorem | rankfu 9098 | An upper bound on the rank of a function. (Contributed by Gérard Lang, 5-Aug-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 → (rank‘𝐹) ⊆ suc suc (rank‘(𝐴 ∪ 𝐵))) | ||
Theorem | rankmapu 9099 | An upper bound on the rank of set exponentiation. (Contributed by Gérard Lang, 5-Aug-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (rank‘(𝐴 ↑𝑚 𝐵)) ⊆ suc suc suc (rank‘(𝐴 ∪ 𝐵)) | ||
Theorem | rankxplim 9100 | The rank of a Cartesian product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 9103 for the successor case. (Contributed by NM, 19-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Lim (rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |