Home | Metamath
Proof Explorer Theorem List (p. 380 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cononrel2 37901 | 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 37902* | 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 37903 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
Theorem | elinlem 37904 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
Theorem | elcnvcnvlem 37905 | 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 37906* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
Theorem | elcnvlem 37907 | 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 37908* | 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 37909* | Value of the converse of the intersection of a non-empty class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
Theorem | undmrnresiss 37910* | 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 37911. (Contributed by RP, 26-Sep-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
Theorem | reflexg 37911* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
Theorem | cnvssco 37912* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
Theorem | refimssco 37913 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
Theorem | cleq2lem 37914 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | cbvcllem 37915* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
Theorem | intabssd 37916* | 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 37917* | 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 37918* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
Theorem | dfid7 37919* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | mptrcllem 37920* | 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 37921 | 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 37922* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexlem 37923 | 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 37924* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
Theorem | trclubgNEW 37925* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclubNEW 37926* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclexi 37927* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexi 37928* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
Theorem | clrellem 37929* | 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 37930* | 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 37931* | The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | cnvrcl0 37932* | 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 37933* | The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}) | ||
Theorem | dmtrcl 37934* | 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 37935* | 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 37936* | Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) | ||
Theorem | trcleq2lemRP 37937 | Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | al3im 37938 | Version of ax-4 1737 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 37939* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 37940* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | csbcog 37941 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | cnviun 37942* | Converse of indexed union. (Contributed by RP, 20-Jun-2020.) |
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵 | ||
Theorem | imaiun1 37943* | The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶) | ||
Theorem | coiun1 37944* | Composition with an indexed union. Proof analgous to that of coiun 5645. (Contributed by RP, 20-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | elintima 37945* | Element of intersection of images. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | intimass 37946* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | intimass2 37947* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵) | ||
Theorem | intimag 37948* | 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 37949* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ {𝐵})}) | ||
Theorem | intimasn2 37950* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ 𝑥 ∈ 𝐴 (𝑥 “ {𝐵})) | ||
Theorem | ss2iundf 37951* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝑌 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑦𝐺 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | ss2iundv 37952* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | cbviuneq12df 37953* | 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 37954* | 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 37955 | Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | conrel2d 37956 | Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅) | ||
Theorem | trrelind 37957 | The intersection of transitive relations is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) & ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆)) ⇒ ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇) | ||
Theorem | xpintrreld 37958 | The intersection of a transitive relation with a cross product is a transitve relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵))) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | restrreld 37959 | The restriction of a transitive relation is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | trrelsuperreldg 37960 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Theorem | trficl 37961* | 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 37962 | The converse of a transitive relation is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.) |
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆) | ||
Theorem | trrelsuperrel2dg 37963 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.) |
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Syntax | crcl 37964 | Extend class notation with reflexive closure. |
class r* | ||
Definition | df-rcl 37965* | 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 37966 | Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | ||
Theorem | dfrcl3 37967 | Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1))) | ||
Theorem | dfrcl4 37968* | 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 37969 | 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 37970 | 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 37971* | 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 13797. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | eltrclrec 37972* | 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 37973* | 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 37974* | 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 37975* | 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 13797. (Contributed by RP, 21-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) ⇒ ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvmptiunrelexplb0d 37976* | 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 37977* | 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 37978* | 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 37979 | 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 37980 | 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 37975. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | fvilbd 37981 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | fvilbdRP 37982 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | brfvrcld 37983 | If two elements are connected by the reflexive closure of a relation, then they are connected via zero or one instances the relation. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ (𝐴(𝑅↑𝑟0)𝐵 ∨ 𝐴(𝑅↑𝑟1)𝐵))) | ||
Theorem | brfvrcld2 37984 | If two elements are connected by the reflexive closure of a relation, then they are equal or related by relation. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵))) | ||
Theorem | fvrcllb0d 37985 | A restriction of the identity relation is a subset of the reflexive closure of a set. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (r*‘𝑅)) | ||
Theorem | fvrcllb0da 37986 | A restriction of the identity relation is a subset of the reflexive closure of a relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (r*‘𝑅)) | ||
Theorem | fvrcllb1d 37987 | A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (r*‘𝑅)) | ||
Theorem | brtrclrec 37988* | Two classes related by the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ 𝑋(𝑅↑𝑟𝑛)𝑌)) | ||
Theorem | brrtrclrec 37989* | Two classes related by 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 two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ0 𝑋(𝑅↑𝑟𝑛)𝑌)) | ||
Theorem | briunov2uz 37990* | 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. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌)) | ||
Theorem | eliunov2uz 37991* | 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. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | ov2ssiunov2 37992* | Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 13798 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝑅 ↑ 𝑀) ⊆ (𝐶‘𝑅)) | ||
Theorem | relexp0eq 37993 | The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) → ((dom 𝐴 ∪ ran 𝐴) = (dom 𝐵 ∪ ran 𝐵) ↔ (𝐴↑𝑟0) = (𝐵↑𝑟0))) | ||
Theorem | iunrelexp0 37994* | Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ({0, 1} ∩ 𝑍) ≠ ∅) → (∪ 𝑥 ∈ 𝑍 (𝑅↑𝑟𝑥)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexpxpnnidm 37995 | Any positive power of a cross product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝑁) = (𝐴 × 𝐵))) | ||
Theorem | relexpiidm 37996 | Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) | ||
Theorem | relexpss1d 37997 | The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑟𝑁) ⊆ (𝐵↑𝑟𝑁)) | ||
Theorem | comptiunov2i 37998* | The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.) |
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) & ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) & ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) & ⊢ 𝐼 ∈ V & ⊢ 𝐽 ∈ V & ⊢ 𝐾 = (𝐼 ∪ 𝐽) & ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⇒ ⊢ (𝑋 ∘ 𝑌) = 𝑍 | ||
Theorem | corclrcl 37999 | The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ r*) = r* | ||
Theorem | iunrelexpmin1 38000* | The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∀𝑠((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |