HomeTheorem List (p. 439 of 501)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 439 of 501) | < 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-30976) |
Hilbert Space Explorer
(30977-32499) |
Users' Mathboxes
(32500-50086) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | snen1g 43801 | A singleton is equinumerous to ordinal one iff its content is a set. (Contributed by RP, 8-Oct-2023.) |
| ⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ V) | ||
| Theorem | snen1el 43802 | A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023.) |
| ⊢ ({𝐴} ≈ 1o ↔ 𝐴 ∈ {𝐴}) | ||
| Theorem | sn1dom 43803 | A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023.) |
| ⊢ {𝐴} ≼ 1o | ||
| Theorem | pr2dom 43804 | An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023.) |
| ⊢ {𝐴, 𝐵} ≼ 2o | ||
| Theorem | tr3dom 43805 | An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.) |
| ⊢ {𝐴, 𝐵, 𝐶} ≼ 3o | ||
| Theorem | ensucne0 43806 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.) |
| ⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
| Theorem | ensucne0OLD 43807 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
| Theorem | dfom6 43808 | Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
| ⊢ ω = ∪ (On ∩ Fin) | ||
| Theorem | infordmin 43809 | ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
| ⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥 | ||
| Theorem | iscard4 43810 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
| ⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card) | ||
| Theorem | minregex 43811* | Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which is greater to or equal to 𝐴. This proof uses AC. (Contributed by RP, 23-Nov-2023.) |
| ⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ⊆ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))}) | ||
| Theorem | minregex2 43812* | Given any cardinal number 𝐴, there exists an argument 𝑥, which yields the least regular uncountable value of ℵ which dominates 𝐴. This proof uses AC. (Contributed by RP, 24-Nov-2023.) |
| ⊢ (𝐴 ∈ (ran card ∖ ω) → ∃𝑥 ∈ On 𝑥 = ∩ {𝑦 ∈ On ∣ (∅ ∈ 𝑦 ∧ 𝐴 ≼ (ℵ‘𝑦) ∧ (cf‘(ℵ‘𝑦)) = (ℵ‘𝑦))}) | ||
| Theorem | iscard5 43813* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
| ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
| Theorem | elrncard 43814* | Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.) |
| ⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
| Theorem | harval3 43815* | (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
| ⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
| Theorem | harval3on 43816* | For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
| ⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
| Theorem | omssrncard 43817 | All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023.) |
| ⊢ ω ⊆ ran card | ||
| Theorem | 0iscard 43818 | 0 is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
| ⊢ ∅ ∈ ran card | ||
| Theorem | 1iscard 43819 | 1 is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
| ⊢ 1o ∈ ran card | ||
| Theorem | omiscard 43820 | ω is a cardinal number. (Contributed by RP, 1-Oct-2023.) |
| ⊢ ω ∈ ran card | ||
| Theorem | sucomisnotcard 43821 | ω +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023.) |
| ⊢ ¬ (ω +o 1o) ∈ ran card | ||
| Theorem | nna1iscard 43822 | For any natural number, the add one operation is results in a cardinal number. (Contributed by RP, 1-Oct-2023.) |
| ⊢ (𝑁 ∈ ω → (𝑁 +o 1o) ∈ ran card) | ||
| Theorem | har2o 43823 | The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023.) |
| ⊢ (har‘2o) = 3o | ||
| Theorem | en2pr 43824* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
| ⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦)) | ||
| Theorem | pr2cv 43825 | If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
| Theorem | pr2el1 43826 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵}) | ||
| Theorem | pr2cv1 43827 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V) | ||
| Theorem | pr2el2 43828 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵}) | ||
| Theorem | pr2cv2 43829 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V) | ||
| Theorem | pren2 43830 | An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵)) | ||
| Theorem | pr2eldif1 43831 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ ({𝐴, 𝐵} ∖ {𝐵})) | ||
| Theorem | pr2eldif2 43832 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
| ⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ ({𝐴, 𝐵} ∖ {𝐴})) | ||
| Theorem | pren2d 43833 | A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
| Theorem | aleph1min 43834 | (ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.) |
| ⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥} | ||
| Theorem | alephiso2 43835 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
| ⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}) | ||
| Theorem | alephiso3 43836 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
| ⊢ ℵ Isom E , ≺ (On, (ran card ∖ ω)) | ||
| Theorem | pwelg 43837* | The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.) |
| ⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵)) | ||
| Theorem | pwinfig 43838* | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.) |
| ⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin))) | ||
| Theorem | pwinfi2 43839 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.) |
| ⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin))) | ||
| Theorem | pwinfi3 43840 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.) |
| ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin))) | ||
| Theorem | pwinfi 43841 | The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.) |
| ⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin)) | ||
While there is not yet a definition, the finite intersection property of a class is introduced by fiint 9231 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6349, ordelinel 6421), chains of sets ordered by the proper subset relation (sorpssin 7678), various sets in the field of topology (inopn 22847, incld 22991, innei 23073, ... ) and "universal" classes like weak universes (wunin 10628, tskin 10674) and the class of all sets (inex1g 5265). | ||
| Theorem | fipjust 43842* | A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020.) |
| ⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) | ||
| Theorem | cllem0 43843* | The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by RP, 3-Jan-2020.) |
| ⊢ 𝑉 = {𝑧 ∣ 𝜑} & ⊢ 𝑅 ∈ 𝑈 & ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 | ||
| Theorem | superficl 43844* | The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
| Theorem | superuncl 43845* | The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
| Theorem | ssficl 43846* | The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
| Theorem | ssuncl 43847* | The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
| Theorem | ssdifcl 43848* | The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴 | ||
| Theorem | sssymdifcl 43849* | The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.) |
| ⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴 | ||
| Theorem | fiinfi 43850* | If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶) | ||
| Theorem | rababg 43851 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
| ⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | ||
| Theorem | elinintab 43852* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
| ⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
| Theorem | elmapintrab 43853* | Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.) |
| ⊢ 𝐶 ∈ V & ⊢ 𝐶 ⊆ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶)))) | ||
| Theorem | elinintrab 43854* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = (𝐵 ∩ 𝑥) ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))) | ||
| Theorem | inintabss 43855* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
| ⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)} | ||
| Theorem | inintabd 43856* | Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)}) | ||
| Theorem | xpinintabd 43857* | Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)}) | ||
| Theorem | relintabex 43858 | If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.) |
| ⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) | ||
| Theorem | elcnvcnvintab 43859* | Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
| ⊢ (𝐴 ∈ ◡◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
| Theorem | relintab 43860* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
| ⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) | ||
| Theorem | nonrel 43861 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
| ⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V)) | ||
| Theorem | elnonrel 43862 | Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.) |
| ⊢ (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ ◡◡𝐴) ↔ (∅ ∈ 𝐴 ∧ ¬ (𝑋 ∈ V ∧ 𝑌 ∈ V))) | ||
| Theorem | cnvssb 43863 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
| ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵)) | ||
| Theorem | relnonrel 43864 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅) | ||
| Theorem | cnvnonrel 43865 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
| ⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅ | ||
| Theorem | brnonrel 43866 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
| ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌) | ||
| Theorem | dmnonrel 43867 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅ | ||
| Theorem | rnnonrel 43868 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅ | ||
| Theorem | resnonrel 43869 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅ | ||
| Theorem | imanonrel 43870 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅ | ||
| Theorem | cononrel1 43871 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅ | ||
| Theorem | cononrel2 43872 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
| ⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅ | ||
See also idssxp 6009 by Thierry Arnoux. | ||
| Theorem | elmapintab 43873* | Two ways to say a set is an element of mapped intersection of a class. Here 𝐹 maps elements of 𝐶 to elements of ∩ {𝑥 ∣ 𝜑} or 𝑥. (Contributed by RP, 19-Aug-2020.) |
| ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ ∩ {𝑥 ∣ 𝜑})) & ⊢ (𝐴 ∈ 𝐸 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐸))) | ||
| Theorem | fvnonrel 43874 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
| ⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
| Theorem | elinlem 43875 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
| ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
| Theorem | elcnvcnvlem 43876 | Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.) |
| ⊢ (𝐴 ∈ ◡◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ ( I ‘𝐴) ∈ 𝐵)) | ||
Original probably needs new subsection for Relation-related existence theorems. | ||
| Theorem | cnvcnvintabd 43877* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
| Theorem | elcnvlem 43878 | Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ (V × V) ↦ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩) ⇒ ⊢ (𝐴 ∈ ◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ (𝐹‘𝐴) ∈ 𝐵)) | ||
| Theorem | elcnvintab 43879* | Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.) |
| ⊢ (𝐴 ∈ ◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ ◡𝑥))) | ||
| Theorem | cnvintabd 43880* | Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.) |
| ⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
| Theorem | undmrnresiss 43881* | Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 43882. (Contributed by RP, 26-Sep-2020.) |
| ⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
| Theorem | reflexg 43882* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
| ⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
| Theorem | cnvssco 43883* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
| ⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
| Theorem | refimssco 43884 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
| ⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
| Theorem | cleq2lem 43885 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
| ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
| Theorem | cbvcllem 43886* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
| Theorem | clublem 43887* | If a superset 𝑌 of 𝑋 possesses the property parameterized in 𝑥 in 𝜓, then 𝑌 is a superset of the closure of that property for the set 𝑋. (Contributed by RP, 23-Jul-2020.) |
| ⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝑥 = 𝑌 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ 𝑌) | ||
| Theorem | clss2lem 43888* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
| ⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
| Theorem | dfid7 43889* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
| ⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
| Theorem | mptrcllem 43890* | Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020.) |
| ⊢ (𝑥 ∈ 𝑉 → ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∈ V) & ⊢ (𝑥 ∈ 𝑉 → ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} ∈ V) & ⊢ (𝑥 ∈ 𝑉 → 𝜒) & ⊢ (𝑥 ∈ 𝑉 → 𝜃) & ⊢ (𝑥 ∈ 𝑉 → 𝜏) & ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ 𝜃)) & ⊢ (𝑧 = ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝑥 ∈ 𝑉 ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) = (𝑥 ∈ 𝑉 ↦ ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)}) | ||
| Theorem | cotrintab 43891 | The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020.) |
| ⊢ (𝜑 → (𝑥 ∘ 𝑥) ⊆ 𝑥) ⇒ ⊢ (∩ {𝑥 ∣ 𝜑} ∘ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑥 ∣ 𝜑} | ||
| Theorem | rclexi 43892* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
| ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
| Theorem | rtrclexlem 43893 | Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 1-Nov-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ ((dom 𝑅 ∪ ran 𝑅) × (dom 𝑅 ∪ ran 𝑅))) ∈ V) | ||
| Theorem | rtrclex 43894* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
| ⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
| Theorem | trclubgNEW 43895* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
| ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
| Theorem | trclubNEW 43896* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
| ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
| Theorem | trclexi 43897* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
| ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
| Theorem | rtrclexi 43898* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
| ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
| Theorem | clrellem 43899* | When the property 𝜓 holds for a relation substituted for 𝑥, then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020.) |
| ⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝜑 → Rel 𝑋) & ⊢ (𝑥 = ◡◡𝑌 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → Rel ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)}) | ||
| Theorem | clcnvlem 43900* | When 𝐴, an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓)) & ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |