Home | Metamath
Proof Explorer Theorem List (p. 399 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pwinfi2 39801 | 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 39802 | 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 39803 | 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 8784 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6216, ordelinel 6283), chains of sets ordered by the proper subset relation (sorpssin 7446), various sets in the field of topology (inopn 21437, incld 21581, innei 21663, ... ) and "universal" classes like weak universes (wunin 10124, tskin 10170) and the class of all sets (inex1g 5215). | ||
Theorem | fipjust 39804* | 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 39805* | 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 39806* | 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 39807* | The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssficl 39808* | 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 39809* | The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssdifcl 39810* | The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴 | ||
Theorem | sssymdifcl 39811* | The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴 | ||
Theorem | fiinfi 39812* | If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶) | ||
Theorem | rababg 39813 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | ||
Theorem | elintabg 39814* | Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | elinintab 39815* | 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 39816* | 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 39817* | 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 39818* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)} | ||
Theorem | inintabd 39819* | Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | xpinintabd 39820* | Value of the intersection of cross-product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | relintabex 39821 | If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) | ||
Theorem | elcnvcnvintab 39822* | 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 39823* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) | ||
Theorem | nonrel 39824 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V)) | ||
Theorem | elnonrel 39825 | 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 39826 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵)) | ||
Theorem | relnonrel 39827 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅) | ||
Theorem | cnvnonrel 39828 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | brnonrel 39829 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌) | ||
Theorem | dmnonrel 39830 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | rnnonrel 39831 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | resnonrel 39832 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅ | ||
Theorem | imanonrel 39833 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅ | ||
Theorem | cononrel1 39834 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅ | ||
Theorem | cononrel2 39835 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅ | ||
See also idssxp 5910 by Thierry Arnoux. | ||
Theorem | elmapintab 39836* | 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 39837 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
Theorem | elinlem 39838 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
Theorem | elcnvcnvlem 39839 | 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 39840* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
Theorem | elcnvlem 39841 | 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 39842* | 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 39843* | Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
Theorem | undmrnresiss 39844* | 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 39845. (Contributed by RP, 26-Sep-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
Theorem | reflexg 39845* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
Theorem | cnvssco 39846* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
Theorem | refimssco 39847 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
Theorem | cleq2lem 39848 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | cbvcllem 39849* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
Theorem | clublem 39850* | 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 39851* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
Theorem | dfid7 39852* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | mptrcllem 39853* | 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 39854 | 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 39855* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexlem 39856 | 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 39857* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
Theorem | trclubgNEW 39858* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclubNEW 39859* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclexi 39860* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexi 39861* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
Theorem | clrellem 39862* | 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 39863* | 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 39864* | The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | cnvrcl0 39865* | 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 39866* | The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}) | ||
Theorem | dmtrcl 39867* | 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 39868* | 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 39869* | Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) | ||
Theorem | trcleq2lemRP 39870 | Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | al3im 39871 | Version of ax-4 1801 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 39872* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 39873* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | csbcog 39874 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | cnviun 39875* | Converse of indexed union. (Contributed by RP, 20-Jun-2020.) |
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵 | ||
Theorem | imaiun1 39876* | The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶) | ||
Theorem | coiun1 39877* | Composition with an indexed union. Proof analgous to that of coiun 6103. (Contributed by RP, 20-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | elintima 39878* | Element of intersection of images. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | intimass 39879* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | intimass2 39880* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵) | ||
Theorem | intimag 39881* | Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑦(∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎 → ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) → (∩ 𝐴 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}) | ||
Theorem | intimasn 39882* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ {𝐵})}) | ||
Theorem | intimasn2 39883* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ 𝑥 ∈ 𝐴 (𝑥 “ {𝐵})) | ||
Theorem | ss2iundf 39884* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝑌 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑦𝐺 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | ss2iundv 39885* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | cbviuneq12df 39886* | Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑦𝑌 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐺 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐺) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐷 = 𝐹) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | cbviuneq12dv 39887* | Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐺) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐷 = 𝐹) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | conrel1d 39888 | Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | conrel2d 39889 | Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅) | ||
Theorem | trrelind 39890 | The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) & ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆)) ⇒ ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇) | ||
Theorem | xpintrreld 39891 | The intersection of a transitive relation with a cross product is a transitve relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵))) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | restrreld 39892 | The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | trrelsuperreldg 39893 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Theorem | trficl 39894* | The class of all transitive relations has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ (𝑧 ∘ 𝑧) ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | cnvtrrel 39895 | The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆) | ||
Theorem | trrelsuperrel2dg 39896 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.) |
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Syntax | crcl 39897 | Extend class notation with reflexive closure. |
class r* | ||
Definition | df-rcl 39898* | Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) | ||
Theorem | dfrcl2 39899 | Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | ||
Theorem | dfrcl3 39900 | Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |