![]() |
Metamath
Proof Explorer Theorem List (p. 420 of 473) | < 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: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqrtcvallem4 41901 | Equivalent to saying that the square of the real component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval 41903. See resqrtval 41905. (Contributed by RP, 11-May-2024.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)) | ||
Theorem | sqrtcvallem5 41902 | Equivalent to saying that the real component of the square root of a complex number is a real number. Lemma for resqrtval 41905 and imsqrtval 41906. (Contributed by RP, 11-May-2024.) |
⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ) | ||
Theorem | sqrtcval 41903 | Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei 15077 and crimi 15078. This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) | ||
Theorem | sqrtcval2 41904 | Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right side is slightly more compact than sqrtcval 41903. (Contributed by RP, 18-May-2024.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (if((ℑ‘𝐴) < 0, -i, i) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) | ||
Theorem | resqrtval 41905 | Real part of the complex square root. (Contributed by RP, 18-May-2024.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(√‘𝐴)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) | ||
Theorem | imsqrtval 41906 | Imaginary part of the complex square root. (Contributed by RP, 18-May-2024.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘(√‘𝐴)) = (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) | ||
Theorem | resqrtvalex 41907 | Example for resqrtval 41905. (Contributed by RP, 21-May-2024.) |
⊢ (ℜ‘(√‘(;15 + (i · 8)))) = 4 | ||
Theorem | imsqrtvalex 41908 | Example for imsqrtval 41906. (Contributed by RP, 21-May-2024.) |
⊢ (ℑ‘(√‘(;15 + (i · 8)))) = 1 | ||
Theorem | al3im 41909 | Version of ax-4 1811 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 41910* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 41911* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | cnviun 41912* | Converse of indexed union. (Contributed by RP, 20-Jun-2020.) |
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵 | ||
Theorem | imaiun1 41913* | The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶) | ||
Theorem | coiun1 41914* | Composition with an indexed union. Proof analgous to that of coiun 6208. (Contributed by RP, 20-Jun-2020.) |
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | elintima 41915* | Element of intersection of images. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | intimass 41916* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | intimass2 41917* | The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.) |
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵) | ||
Theorem | intimag 41918* | 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 41919* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ {𝐵})}) | ||
Theorem | intimasn2 41920* | Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ 𝑥 ∈ 𝐴 (𝑥 “ {𝐵})) | ||
Theorem | ss2iundf 41921* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝑌 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑦𝐺 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | ss2iundv 41922* | Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷) | ||
Theorem | cbviuneq12df 41923* | 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 41924* | 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 41925 | Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | conrel2d 41926 | Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅) | ||
Theorem | trrelind 41927 | The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) & ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆)) ⇒ ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇) | ||
Theorem | xpintrreld 41928 | The intersection of a transitive relation with a Cartesian product is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵))) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | restrreld 41929 | The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | trrelsuperreldg 41930 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Theorem | trficl 41931* | 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 41932 | The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆) | ||
Theorem | trrelsuperrel2dg 41933 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.) |
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Syntax | crcl 41934 | Extend class notation with reflexive closure. |
class r* | ||
Definition | df-rcl 41935* | 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 41936 | Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | ||
Theorem | dfrcl3 41937 | Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1))) | ||
Theorem | dfrcl4 41938* | 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 41939 | 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 41940 | 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 41941* | 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 element is a member of that operator value. Generalized from dfrtrclrec2 14943. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | eltrclrec 41942* | 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 41943* | 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 41944* | 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 two classes are related by that operator value. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌)) | ||
Theorem | brmptiunrelexpd 41945* | 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 14943. (Contributed by RP, 21-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) ⇒ ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvmptiunrelexplb0d 41946* | 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 41947* | 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 41948* | 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 41949 | 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 41950 | 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 41945. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | fvilbd 41951 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | fvilbdRP 41952 | 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 41953 | 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 41954 | 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 41955 | 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 41956 | 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 41957 | A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (r*‘𝑅)) | ||
Theorem | brtrclrec 41958* | 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 41959* | 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 41960* | 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 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 41961* | 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 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 41962* | Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 14942 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝑅 ↑ 𝑀) ⊆ (𝐶‘𝑅)) | ||
Theorem | relexp0eq 41963 | 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 41964* | Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ({0, 1} ∩ 𝑍) ≠ ∅) → (∪ 𝑥 ∈ 𝑍 (𝑅↑𝑟𝑥)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexpxpnnidm 41965 | Any positive power of a Cartesian product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝑁) = (𝐴 × 𝐵))) | ||
Theorem | relexpiidm 41966 | Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) | ||
Theorem | relexpss1d 41967 | The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑟𝑁) ⊆ (𝐵↑𝑟𝑁)) | ||
Theorem | comptiunov2i 41968* | The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.) |
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) & ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) & ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) & ⊢ 𝐼 ∈ V & ⊢ 𝐽 ∈ V & ⊢ 𝐾 = (𝐼 ∪ 𝐽) & ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⇒ ⊢ (𝑋 ∘ 𝑌) = 𝑍 | ||
Theorem | corclrcl 41969 | The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ r*) = r* | ||
Theorem | iunrelexpmin1 41970* | 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 ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∀𝑠((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) | ||
Theorem | relexpmulnn 41971 | With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | relexpmulg 41972 | With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | trclrelexplem 41973* | The union of relational powers to positive multiples of 𝑁 is a subset to the transitive closure raised to the power of 𝑁. (Contributed by RP, 15-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ∪ 𝑘 ∈ ℕ ((𝐷↑𝑟𝑘)↑𝑟𝑁) ⊆ (∪ 𝑗 ∈ ℕ (𝐷↑𝑟𝑗)↑𝑟𝑁)) | ||
Theorem | iunrelexpmin2 41974* | The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0) → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) | ||
Theorem | relexp01min 41975 | With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | relexp1idm 41976 | Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1)↑𝑟1) = (𝑅↑𝑟1)) | ||
Theorem | relexp0idm 41977 | Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟0)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexp0a 41978 | Absorption law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0)) | ||
Theorem | relexpxpmin 41979 | The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)) | ||
Theorem | relexpaddss 41980 | The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where 𝑅 is a relation as shown by relexpaddd 14939 or when the sum of the powers isn't 1 as shown by relexpaddg 14938. (Contributed by RP, 3-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ⊆ (𝑅↑𝑟(𝑁 + 𝑀))) | ||
Theorem | iunrelexpuztr 41981* | The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 14945. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = (ℤ≥‘𝑀) ∧ 𝑀 ∈ ℕ0) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅)) | ||
Theorem | dftrcl3 41982* | Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.) |
⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) | ||
Theorem | brfvtrcld 41983* | If two elements are connected by the transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some counting number 𝑛. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvtrcllb1d 41984 | A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t+‘𝑅)) | ||
Theorem | trclfvcom 41985 | The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (𝑅 ∘ (t+‘𝑅))) | ||
Theorem | cnvtrclfv 41986 | The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ◡(t+‘𝑅) = (t+‘◡𝑅)) | ||
Theorem | cotrcltrcl 41987 | The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.) |
⊢ (t+ ∘ t+) = t+ | ||
Theorem | trclimalb2 41988 | Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 “ (𝐴 ∪ 𝐵)) ⊆ 𝐵) → ((t+‘𝑅) “ 𝐴) ⊆ 𝐵) | ||
Theorem | brtrclfv2 41989* | Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋(t+‘𝑅)𝑌 ↔ 𝑌 ∈ ∩ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})) | ||
Theorem | trclfvdecomr 41990 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅))) | ||
Theorem | trclfvdecoml 41991 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ (𝑅 ∘ (t+‘𝑅)))) | ||
Theorem | dmtrclfvRP 41992 | The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅) | ||
Theorem | rntrclfvRP 41993 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
Theorem | rntrclfv 41994 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
Theorem | dfrtrcl3 41995* | Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 14947. (Contributed by RP, 5-Jun-2020.) |
⊢ t* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) | ||
Theorem | brfvrtrcld 41996* | If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some natural number 𝑛. Similar of dfrtrclrec2 14943. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t*‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvrtrcllb0d 41997 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*‘𝑅)) | ||
Theorem | fvrtrcllb0da 41998 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*‘𝑅)) | ||
Theorem | fvrtrcllb1d 41999 | A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t*‘𝑅)) | ||
Theorem | dfrtrcl4 42000 | Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.) |
⊢ t* = (𝑟 ∈ V ↦ ((𝑟↑𝑟0) ∪ (t+‘𝑟))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |