P. 437 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43601-43700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnvnonrel 43601	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅
Theorem	brnonrel 43602	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌)
Theorem	dmnonrel 43603	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	rnnonrel 43604	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	resnonrel 43605	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅
Theorem	imanonrel 43606	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅
Theorem	cononrel1 43607	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅
Theorem	cononrel2 43608	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅
21.36.4.11  RP ADDTO: Functions See also idssxp 6067 by Thierry Arnoux.
Theorem	elmapintab 43609*	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 43610	The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅
Theorem	elinlem 43611	Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶))
Theorem	elcnvcnvlem 43612	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 ‘𝐴) ∈ 𝐵))
21.36.4.12  RP ADDTO: Finite induction (for finite ordinals) Original probably needs new subsection for Relation-related existence theorems.
Theorem	cnvcnvintabd 43613*	Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)})
21.36.4.13  RP ADDTO: First and second members of an ordered pair
Theorem	elcnvlem 43614	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 43615*	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 43616*	Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)})
21.36.4.14  RP ADDTO: The reflexive and transitive properties of relations
Theorem	undmrnresiss 43617*	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 43618. (Contributed by RP, 26-Sep-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
Theorem	reflexg 43618*	Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦)))
Theorem	cnvssco 43619*	A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.)
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)))
Theorem	refimssco 43620	Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴))
21.36.4.15  RP ADDTO: Basic properties of closures
Theorem	cleq2lem 43621	Equality implies bijection. (Contributed by RP, 24-Jul-2020.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓)))
Theorem	cbvcllem 43622*	Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)}
Theorem	clublem 43623*	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 43624*	The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)})
Theorem	dfid7 43625*	Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.)
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)})
Theorem	mptrcllem 43626*	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 43627	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 43628*	The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V
Theorem	rtrclexlem 43629	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 43630*	The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.)
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
Theorem	trclubgNEW 43631*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclubNEW 43632*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅))
Theorem	trclexi 43633*	The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V
Theorem	rtrclexi 43634*	The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V
Theorem	clrellem 43635*	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 43636*	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 43637*	The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)})
Theorem	cnvrcl0 43638*	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 43639*	The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)})
Theorem	dmtrcl 43640*	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 43641*	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 43642*	Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.)
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))})
21.36.4.16  RP REPLACE: Definitions and basic properties of transitive closures
Theorem	trcleq2lemRP 43643	Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
21.36.4.17  Additions for square root; absolute value This is based on the observation that the real and imaginary parts of a complex number can be calculated from the number's absolute and real part and the sign of its imaginary part. Formalization of the formula in sqrtcval 43654 was motivated by a short Michael Penn video.
Theorem	sqrtcvallem1 43644	Two ways of saying a complex number does not lie on the positive real axis. Lemma for sqrtcval 43654. (Contributed by RP, 17-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ ¬ 𝐴 ∈ ℝ+))
Theorem	reabsifneg 43645	Alternate expression for the absolute value of a real number. Lemma for sqrtcval 43654. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 < 0, -𝐴, 𝐴))
Theorem	reabsifnpos 43646	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 ≤ 0, -𝐴, 𝐴))
Theorem	reabsifpos 43647	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(0 < 𝐴, 𝐴, -𝐴))
Theorem	reabsifnneg 43648	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(0 ≤ 𝐴, 𝐴, -𝐴))
Theorem	reabssgn 43649	Alternate expression for the absolute value of a real number. (Contributed by RP, 22-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = ((sgn‘𝐴) · 𝐴))
Theorem	sqrtcvallem2 43650	Equivalent to saying that the square of the imaginary component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval 43654. See imsqrtval 43657. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
Theorem	sqrtcvallem3 43651	Equivalent to saying that the absolute value of the imaginary component of the square root of a complex number is a real number. Lemma for sqrtcval 43654, sqrtcval2 43655, resqrtval 43656, and imsqrtval 43657. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
Theorem	sqrtcvallem4 43652	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 43654. See resqrtval 43656. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
Theorem	sqrtcvallem5 43653	Equivalent to saying that the real component of the square root of a complex number is a real number. Lemma for resqrtval 43656 and imsqrtval 43657. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
Theorem	sqrtcval 43654	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 15231 and crimi 15232. 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 43655	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 43654. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (if((ℑ‘𝐴) < 0, -i, i) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
Theorem	resqrtval 43656	Real part of the complex square root. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(√‘𝐴)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
Theorem	imsqrtval 43657	Imaginary part of the complex square root. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (ℑ‘(√‘𝐴)) = (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))
Theorem	resqrtvalex 43658	Example for resqrtval 43656. (Contributed by RP, 21-May-2024.)
⊢ (ℜ‘(√‘(;15 + (i · 8)))) = 4
Theorem	imsqrtvalex 43659	Example for imsqrtval 43657. (Contributed by RP, 21-May-2024.)
⊢ (ℑ‘(√‘(;15 + (i · 8)))) = 1
21.36.5  Additional statements on relations and subclasses
Theorem	al3im 43660	Version of ax-4 1809 for a nested implication. (Contributed by RP, 13-Apr-2020.)
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃))))
Theorem	intima0 43661*	Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.)
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}
Theorem	elimaint 43662*	Element of image of intersection. (Contributed by RP, 13-Apr-2020.)
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 ⟨𝑏, 𝑦⟩ ∈ 𝑎)
Theorem	cnviun 43663*	Converse of indexed union. (Contributed by RP, 20-Jun-2020.)
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵
Theorem	imaiun1 43664*	The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶)
Theorem	coiun1 43665*	Composition with an indexed union. Proof analogous to that of coiun 6276. (Contributed by RP, 20-Jun-2020.)
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	elintima 43666*	Element of intersection of images. (Contributed by RP, 13-Apr-2020.)
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ⟨𝑏, 𝑦⟩ ∈ 𝑎)
Theorem	intimass 43667*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}
Theorem	intimass2 43668*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵)
Theorem	intimag 43669*	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 43670*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ {𝐵})})
Theorem	intimasn2 43671*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
⊢ (𝐵 ∈ 𝑉 → (∩ 𝐴 “ {𝐵}) = ∩ 𝑥 ∈ 𝐴 (𝑥 “ {𝐵}))
Theorem	ss2iundf 43672*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝑌    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐺    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	ss2iundv 43673*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐺)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	cbviuneq12df 43674*	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 43675*	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 43676	Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ◡𝐴 = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	conrel2d 43677	Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ◡𝐴 = ∅)    ⇒   ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅)
21.36.5.1  Transitive relations (not to be confused with transitive classes).
Theorem	trrelind 43678	The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆))    ⇒   ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇)
Theorem	xpintrreld 43679	The intersection of a transitive relation with a Cartesian product is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵)))    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)
Theorem	restrreld 43680	The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴))    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆)
Theorem	trrelsuperreldg 43681	Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 25-Dec-2019.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆))
Theorem	trficl 43682*	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 43683	The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019.)
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆)
Theorem	trrelsuperrel2dg 43684	Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.)
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆))
21.36.5.2  Reflexive closures
Syntax	crcl 43685	Extend class notation with reflexive closure.
class r*
Definition	df-rcl 43686*	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 43687	Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.)
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
Theorem	dfrcl3 43688	Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.)
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1)))
Theorem	dfrcl4 43689*	Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020.)
⊢ r* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ {0, 1} (𝑟↑𝑟𝑛))
21.36.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 43690	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 43691	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 43692*	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 15097. (Contributed by RP, 1-Jun-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛))    ⇒   ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛)))
Theorem	eltrclrec 43693*	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 43694*	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 43695*	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 43696*	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 15097. (Contributed by RP, 21-Jul-2020.)
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛))    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑁 ⊆ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	fvmptiunrelexplb0d 43697*	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 43698*	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 43699*	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 43700	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 ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵))