Home | Metamath
Proof Explorer Theorem List (p. 400 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tr3dom 39901 | An unordered triple is dominated by ordinal three. (Contributed by RP, 29-Oct-2023.) |
⊢ {𝐴, 𝐵, 𝐶} ≼ 3o | ||
Theorem | ensucne0 39902 | 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 39903 | 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 | nndomog 39904 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 8714 when both are natural numbers. (Originally by NM, 17-Jun-1998.) (Contributed by RP, 5-Nov-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | dfom6 39905 | Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
⊢ ω = ∪ (On ∩ Fin) | ||
Theorem | infordmin 39906 | ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥 | ||
Theorem | iscard4 39907 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card) | ||
Theorem | iscard5 39908* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | elrncard 39909* | 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 | harsucnn 39910 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴) | ||
Theorem | harval3 39911* | (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | harval3on 39912* | 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 | en2pr 39913* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | pr2cv 39914 | 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 39915 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv1 39916 | 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 39917 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv2 39918 | 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 39919 | 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 39920 | 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 39921 | 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 39922 | A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | aleph1min 39923 | (ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.) |
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥} | ||
Theorem | alephiso2 39924 | ℵ 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 39925 | ℵ 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 39926* | 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 39927* | 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 39928 | 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 39929 | 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 39930 | 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 8797 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6224, ordelinel 6291), chains of sets ordered by the proper subset relation (sorpssin 7459), various sets in the field of topology (inopn 21509, incld 21653, innei 21735, ... ) and "universal" classes like weak universes (wunin 10137, tskin 10183) and the class of all sets (inex1g 5225). | ||
Theorem | fipjust 39931* | 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 39932* | 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 39933* | 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 39934* | The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssficl 39935* | 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 39936* | The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssdifcl 39937* | The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴 | ||
Theorem | sssymdifcl 39938* | The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴 | ||
Theorem | fiinfi 39939* | If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶) | ||
Theorem | rababg 39940 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | ||
Theorem | elintabg 39941* | Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | elinintab 39942* | 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 39943* | 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 39944* | 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 39945* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)} | ||
Theorem | inintabd 39946* | Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | xpinintabd 39947* | Value of the intersection of cross-product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | relintabex 39948 | If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) | ||
Theorem | elcnvcnvintab 39949* | 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 39950* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) | ||
Theorem | nonrel 39951 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V)) | ||
Theorem | elnonrel 39952 | 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 39953 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵)) | ||
Theorem | relnonrel 39954 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅) | ||
Theorem | cnvnonrel 39955 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | brnonrel 39956 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌) | ||
Theorem | dmnonrel 39957 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | rnnonrel 39958 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | resnonrel 39959 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅ | ||
Theorem | imanonrel 39960 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅ | ||
Theorem | cononrel1 39961 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅ | ||
Theorem | cononrel2 39962 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅ | ||
See also idssxp 5918 by Thierry Arnoux. | ||
Theorem | elmapintab 39963* | 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 39964 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
Theorem | elinlem 39965 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
Theorem | elcnvcnvlem 39966 | 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 39967* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
Theorem | elcnvlem 39968 | 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 39969* | 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 39970* | Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
Theorem | undmrnresiss 39971* | 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 39972. (Contributed by RP, 26-Sep-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
Theorem | reflexg 39972* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
Theorem | cnvssco 39973* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
Theorem | refimssco 39974 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
Theorem | cleq2lem 39975 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | cbvcllem 39976* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
Theorem | clublem 39977* | 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 39978* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
Theorem | dfid7 39979* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | mptrcllem 39980* | 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 39981 | 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 39982* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexlem 39983 | 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 39984* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
Theorem | trclubgNEW 39985* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclubNEW 39986* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclexi 39987* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexi 39988* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
Theorem | clrellem 39989* | 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 39990* | 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) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) | ||
Theorem | cnvtrucl0 39991* | The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | cnvrcl0 39992* | The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)}) | ||
Theorem | cnvtrcl0 39993* | The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}) | ||
Theorem | dmtrcl 39994* | The domain of the transitive closure is equal to the domain of its base relation. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝑋 ∈ 𝑉 → dom ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = dom 𝑋) | ||
Theorem | rntrcl 39995* | The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝑋 ∈ 𝑉 → ran ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ran 𝑋) | ||
Theorem | dfrtrcl5 39996* | Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) | ||
Theorem | trcleq2lemRP 39997 | Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | al3im 39998 | Version of ax-4 1810 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 39999* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 40000* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |