P. 150 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14901-15000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	s7f1o 14901	A length 7 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by AV, 2-Aug-2025.)
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐷 ∈ 𝑉 ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉)) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺)) ∧ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ (𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺)) ∧ (𝐶 ≠ 𝐷 ∧ (𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺))) ∧ ((𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺) ∧ (𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺)))) → (𝐾 = ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ → 𝐾:(0..^7)–1-1-onto→(({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})))
Theorem	s3sndisj 14902*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {⟨“𝐴𝐵𝑐”⟩})
Theorem	s3iunsndisj 14903*	The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){⟨“𝑎𝐵𝑐”⟩})
Theorem	ofccat 14904	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑇)    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑇)    &   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐺))    &   ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘f 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘f 𝑅𝐺) ++ (𝐹 ∘f 𝑅𝐻)))
Theorem	ofs1 14905	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f 𝑅⟨“𝐵”⟩) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofs2 14906	Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇)) → (⟨“𝐴𝐵”⟩ ∘f 𝑅⟨“𝐶𝐷”⟩) = ⟨“(𝐴𝑅𝐶)(𝐵𝑅𝐷)”⟩)
5.8  Reflexive and transitive closures of relations A relation, 𝑅, has the reflexive property if 𝐴𝑅𝐴 holds whenever 𝐴 is an element which could be related by the relation, namely, an element of its domain or range. Eliminating dummy variables, we see that a segment of the identity relation must be a subset of the relation, or ( I ↾ (ran 𝑅 ∪ dom 𝑅)) ⊆ 𝑅. See idref 7101. A relation, 𝑅, has the transitive property if 𝐴𝑅𝐶 holds whenever there exists an intermediate value 𝐵 such that both 𝐴𝑅𝐵 and 𝐵𝑅𝐶 hold. This can be expressed without dummy variables as (𝑅 ∘ 𝑅) ⊆ 𝑅. See cotr 6077. The transitive closure of a relation, (t+‘𝑅), is the smallest superset of the relation which has the transitive property. Likewise, the reflexive-transitive closure, (t*‘𝑅), is the smallest superset which has both the reflexive and transitive properties. Not to be confused with the transitive closure of a set, trcl 9649, which is a closure relative to a different transitive property, df-tr 5208.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 14907	Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷))
Theorem	trrelssd 14908	The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅)
Theorem	xpcogend 14909	The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷))
Theorem	xpcoidgend 14910	If two classes are not disjoint, then the composition of their Cartesian product with itself is idempotent. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐵))
Theorem	cotr2g 14911*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14912 for the main application. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝐵 ⊆ 𝐷    &   ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸    &   ⊢ ran 𝐴 ⊆ 𝐹    ⇒   ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr2 14912*	Two ways of saying a relation is transitive. Special instance of cotr2g 14911. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝑅 ⊆ 𝐴    &   ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵    &   ⊢ ran 𝑅 ⊆ 𝐶    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	cotr3 14913*	Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.)
⊢ 𝐴 = dom 𝑅    &   ⊢ 𝐵 = (𝐴 ∩ 𝐶)    &   ⊢ 𝐶 = ran 𝑅    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	coemptyd 14914	Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	xptrrel 14915	The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
Theorem	0trrel 14916	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (∅ ∘ ∅) ⊆ ∅
5.8.2  Basic properties of closures
Theorem	cleq1lem 14917	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑)))
Theorem	cleq1 14918*	Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)})
Theorem	clsslem 14919*	The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.)
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)})
5.8.3  Definitions and basic properties of transitive closures
Syntax	ctcl 14920	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 14921	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 14922*	Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.)
⊢ t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
Definition	df-rtrcl 14923*	Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011.)
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
Theorem	trcleq1 14924*	Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trclsslem 14925*	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trcleq2lem 14926	Equality implies bijection. (Contributed by RP, 5-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	cvbtrcl 14927*	Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.)
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}
Theorem	trcleq12lem 14928	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	trclexlem 14929	Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 5-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V)
Theorem	trclublem 14930*	If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})
Theorem	trclubi 14931*	The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.)
⊢ Rel 𝑅    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (dom 𝑅 × ran 𝑅)
Theorem	trclubgi 14932*	The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure. (Contributed by RP, 3-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.)
⊢ 𝑅 ∈ V    ⇒   ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))
Theorem	trclub 14933*	The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ (dom 𝑅 × ran 𝑅))
Theorem	trclubg 14934*	The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure (as a relation). (Contributed by RP, 17-May-2020.)
⊢ (𝑅 ∈ 𝑉 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclfv 14935*	The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})
Theorem	brintclab 14936*	Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.)
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥))
Theorem	brtrclfv 14937*	Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfv 14938*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴)))
Theorem	brtrclfvcnv 14939*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfvcnv 14940*	Two ways of expressing the transitive closure of the converse of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴)))
Theorem	trclfvss 14941	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑅 ⊆ 𝑆) → (t+‘𝑅) ⊆ (t+‘𝑆))
Theorem	trclfvub 14942	The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclfvlb 14943	The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcotr 14944	The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅))
Theorem	trclfvlb2 14945	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅))
Theorem	trclfvlb3 14946	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅))
Theorem	cotrtrclfv 14947	The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅)
Theorem	trclidm 14948	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅))
Theorem	trclun 14949	Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆))))
Theorem	trclfvg 14950	The value of the transitive closure of a relation is a superset or (for proper classes) the empty set. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ⊆ (t+‘𝑅) ∨ (t+‘𝑅) = ∅)
Theorem	trclfvcotrg 14951	The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020.)
⊢ ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅)
Theorem	reltrclfv 14952	The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅))
Theorem	dmtrclfv 14953	The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅)
5.8.4  Exponentiation of relations
Syntax	crelexp 14954	Extend class notation to include relation exponentiation.
class ↑𝑟
Definition	df-relexp 14955*	Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 22-May-2020.)
⊢ ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
Theorem	reldmrelexp 14956	The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.)
⊢ Rel dom ↑𝑟
Theorem	relexp0g 14957	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Theorem	relexp0 14958	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexp0d 14959	A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexpsucnnr 14960	A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexp1g 14961	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅)
Theorem	dfid5 14962	Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1))
Theorem	dfid6 14963*	Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛))
Theorem	relexp1d 14964	A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟1) = 𝑅)
Theorem	relexpsucnnl 14965	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucl 14966	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucr 14967	A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexpsucrd 14968	A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexpsucld 14969	A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpcnv 14970	Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))
Theorem	relexpcnvd 14971	Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))
Theorem	relexp0rel 14972	The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.)
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0))
Theorem	relexprelg 14973	The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ (𝑁 = 1 → Rel 𝑅)) → Rel (𝑅↑𝑟𝑁))
Theorem	relexprel 14974	The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpreld 14975	The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → Rel (𝑅↑𝑟𝑁))
Theorem	relexpnndm 14976	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅)
Theorem	relexpdmg 14977	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅))
Theorem	relexpdm 14978	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpdmd 14979	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → dom (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpnnrn 14980	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ ran 𝑅)
Theorem	relexprng 14981	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅))
Theorem	relexprn 14982	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexprnd 14983	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ran (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpfld 14984	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpfldd 14985	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpaddnn 14986	Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	relexpuzrel 14987	The exponentiation of a class to an integer greater than 1 is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpaddg 14988	Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	relexpaddd 14989	Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
5.8.5  Reflexive-transitive closure as an indexed union
Syntax	crtrcl 14990	Extend class notation with recursively defined reflexive, transitive closure.
class t*rec
Definition	df-rtrclrec 14991*	The reflexive, transitive closure of a relation constructed as the union of all finite exponentiations. (Contributed by Drahflow, 12-Nov-2015.)
⊢ t*rec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))
Theorem	rtrclreclem1 14992	The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑅 ⊆ (t*rec‘𝑅))
Theorem	dfrtrclrec2 14993*	If two elements are connected by a reflexive, transitive closure, then they are connected via 𝑛 instances the relation, for some 𝑛. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵))
Theorem	rtrclreclem2 14994	The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*rec‘𝑅))
Theorem	rtrclreclem3 14995	The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅))
Theorem	rtrclreclem4 14996*	The reflexive, transitive closure of 𝑅 is the smallest reflexive, transitive relation which contains 𝑅 and the identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
Theorem	dfrtrcl2 14997	The two definitions t* and t*rec of the reflexive, transitive closure coincide if 𝑅 is indeed a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → (t*‘𝑅) = (t*rec‘𝑅))
5.8.6  Principle of transitive induction. If we have a statement that holds for some element, and a relation between elements that implies if it holds for the first element then it must hold for the second element, the principle of transitive induction shows the statement holds for any element related to the first by the (reflexive-)transitive closure of the relation.
Theorem	relexpindlem 14998*	Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜂 → Rel 𝑅)    &   ⊢ (𝜂 → 𝑆 ∈ 𝑉)    &   ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))    &   ⊢ (𝜂 → 𝜒)    &   ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))    ⇒   ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
Theorem	relexpind 14999*	Principle of transitive induction, finite version. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜂 → Rel 𝑅)    &   ⊢ (𝜂 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜂 → 𝑋 ∈ 𝑊)    &   ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜏))    &   ⊢ (𝜂 → 𝜒)    &   ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))    ⇒   ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑋 → 𝜏)))
Theorem	rtrclind 15000*	Principle of transitive induction. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.)
⊢ (𝜂 → Rel 𝑅)    &   ⊢ (𝜂 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜂 → 𝑋 ∈ 𝑊)    &   ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜏))    &   ⊢ (𝜂 → 𝜒)    &   ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))    ⇒   ⊢ (𝜂 → (𝑆(t*‘𝑅)𝑋 → 𝜏))