Home | Metamath
Proof Explorer Theorem List (p. 370 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 | elmapintrab 36901* | 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 36902* | 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 36903* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)} | ||
Theorem | inintabd 36904* | Value of the intersection of class with the intersection of a non-empty class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | xpinintabd 36905* | Value of the intersection of cross-product with the intersection of a non-empty class. (Contributed by RP, 12-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | relintabex 36906 | If the intersection of a class is a relation, then the class is non-empty. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) | ||
Theorem | elcnvcnvintab 36907* | 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 36908* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) | ||
Theorem | nonrel 36909 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V)) | ||
Theorem | elnonrel 36910 | 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 36911 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵)) | ||
Theorem | relnonrel 36912 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅) | ||
Theorem | cnvnonrel 36913 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | brnonrel 36914 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌) | ||
Theorem | dmnonrel 36915 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | rnnonrel 36916 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | resnonrel 36917 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅ | ||
Theorem | imanonrel 36918 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅ | ||
Theorem | cononrel1 36919 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅ | ||
Theorem | cononrel2 36920 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅ | ||
See also idssxp 28811 by Thierry Arnoux. | ||
Theorem | elmapintab 36921* | 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 36922 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
Theorem | elinlem 36923 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
Theorem | elcnvcnvlem 36924 | 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 36925* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
Theorem | elcnvlem 36926 | 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 36927* | 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 36928* | Value of the converse of the intersection of a non-empty class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
Theorem | undmrnresiss 36929* | 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 36930. (Contributed by RP, 26-Sep-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
Theorem | reflexg 36930* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
Theorem | cnvssco 36931* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
Theorem | refimssco 36932 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
Theorem | cleq2lem 36933 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | cbvcllem 36934* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
Theorem | intabssd 36935* | When for each element 𝑦 there is a subset 𝐴 which may substituted for 𝑥 such that 𝑦 satisfying 𝜒 implies 𝑥 satisfies 𝜓 then the intersection of all 𝑥 that satisfy 𝜓 is a subclass the intersection of all 𝑦 that satisfy 𝜒. (Contributed by RP, 17-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑦) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ 𝜓} ⊆ ∩ {𝑦 ∣ 𝜒}) | ||
Theorem | clublem 36936* | 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 36937* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
Theorem | dfid7 36938* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | mptrcllem 36939* | 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 36940 | 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 36941* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexlem 36942 | 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 36943* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
Theorem | trclubgNEW 36944* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclubNEW 36945* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclexi 36946* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexi 36947* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
Theorem | clrellem 36948* | 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 36949* | 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 36950* | The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | cnvrcl0 36951* | 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 36952* | The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}) | ||
Theorem | dmtrcl 36953* | 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 36954* | 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 36955* | Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) | ||
Theorem | trcleq2lemRP 36956 | Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | al3im 36957 | Version of ax-4 1728 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 36958* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 36959* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | csbcog 36960 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | cnviun 36961* | Converse of indexed union. (Contributed by RP, 20-Jun-2020.) |
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵 | ||
Theorem | imaiun1 36962* | The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶) | ||
Theorem | coiun1 36963* | Composition with an indexed union. Proof analgous to that of coiun 5562. (Contributed by RP, 20-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | elintima 36964* | Element of intersection of images. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | intimass 36965* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | intimass2 36966* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵) | ||
Theorem | intimag 36967* | 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 36968* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ {𝐵})}) | ||
Theorem | intimasn2 36969* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ 𝑥 ∈ 𝐴 (𝑥 “ {𝐵})) | ||
Theorem | ss2iundf 36970* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝑌 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑦𝐺 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | ss2iundv 36971* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | cbviuneq12df 36972* | 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 36973* | 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 36974 | Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | conrel2d 36975 | Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅) | ||
Theorem | trrelind 36976 | The intersection of transitive relations is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) & ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆)) ⇒ ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇) | ||
Theorem | xpintrreld 36977 | The intersection of a transitive relation with a cross product is a transitve relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵))) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | restrreld 36978 | The restriction of a transitive relation is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | trrelsuperreldg 36979 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Theorem | trficl 36980* | The class of all transitive relations has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ (𝑧 ∘ 𝑧) ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | cnvtrrel 36981 | The converse of a transitive relation is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.) |
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆) | ||
Theorem | trrelsuperrel2dg 36982 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.) |
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Syntax | crcl 36983 | Extend class notation with reflexive closure. |
class r* | ||
Definition | df-rcl 36984* | 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 36985 | Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | ||
Theorem | dfrcl3 36986 | Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1))) | ||
Theorem | dfrcl4 36987* | Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020.) |
⊢ r* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ {0, 1} (𝑟↑𝑟𝑛)) | ||
In order for theorems on the transitive closure of a relation to be grouped together before the concept of continuity, we really need an analogue of ↑𝑟 that works on finite ordinals or finite sets instead of natural numbers. | ||
Theorem | relexp2 36988 | A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟2) = (𝑅 ∘ 𝑅)) | ||
Theorem | relexpnul 36989 | If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ Rel 𝑅) ∧ (𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)) → ((dom (𝑅↑𝑟𝑁) ∩ ran (𝑅↑𝑟𝑀)) = ∅ ↔ (𝑅↑𝑟(𝑁 + 𝑀)) = ∅)) | ||
Theorem | eliunov2 36990* | Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the the element is a member of that operator value. Generalized from dfrtrclrec2 13645. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | eltrclrec 36991* | Membership in the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ 𝑋 ∈ (𝑅↑𝑟𝑛))) | ||
Theorem | elrtrclrec 36992* | Membership in the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ0 𝑋 ∈ (𝑅↑𝑟𝑛))) | ||
Theorem | briunov2 36993* | Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌)) | ||
Theorem | brmptiunrelexpd 36994* | If two elements are connected by an indexed union of relational powers, then they are connected via 𝑛 instances the relation, for some 𝑛. Generalization of dfrtrclrec2 13645. (Contributed by RP, 21-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) ⇒ ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvmptiunrelexplb0d 36995* | If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → 0 ∈ 𝑁) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (𝐶‘𝑅)) | ||
Theorem | fvmptiunrelexplb0da 36996* | If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 0 ∈ 𝑁) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (𝐶‘𝑅)) | ||
Theorem | fvmptiunrelexplb1d 36997* | If the indexed union ranges over the first power of the relation, then the relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → 1 ∈ 𝑁) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (𝐶‘𝑅)) | ||
Theorem | brfvid 36998 | If two elements are connected by a value of the identity relation, then they are connected via the argument. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | brfvidRP 36999 | If two elements are connected by a value of the identity relation, then they are connected via the argument. This is an example which uses brmptiunrelexpd 36994. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | fvilbd 37000 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |