P. 420 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41901-42000   *Has distinct variable group(s)

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
21.32.5  Additional statements on relations and subclasses
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.)
⊢ (𝜑 → ◡𝐴 = ∅)    ⇒   ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅)
21.32.5.1  Transitive relations (not to be confused with transitive classes).
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 𝑅)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆))
21.32.5.2  Reflexive closures
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} (𝑟↑𝑟𝑛))
21.32.5.3  Finite relationship composition. 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) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅))
21.32.5.4  Transitive closure of a relation
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+‘𝑟)))