P. 147 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wwlktovfo 14601*	Lemma 3 for wrd2f1tovbij 14603. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅)
Theorem	wwlktovf1o 14602*	Lemma 4 for wrd2f1tovbij 14603. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wrd2f1tovbij 14603*	There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → ∃𝑓 𝑓:{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋})
Theorem	eqwrds3 14604	A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = ⟨“𝐴𝐵𝐶”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))))
Theorem	wrdl3s3 14605*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
Theorem	s3sndisj 14606*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {⟨“𝐴𝐵𝑐”⟩})
Theorem	s3iunsndisj 14607*	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 14608	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑇)    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑇)    &   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐺))    &   ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘f 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘f 𝑅𝐺) ++ (𝐹 ∘f 𝑅𝐻)))
Theorem	ofs1 14609	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f 𝑅⟨“𝐵”⟩) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofs2 14610	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 7000. 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 6006. 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 9417, which is a closure relative to a different transitive property, df-tr 5188.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 14611	Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷))
Theorem	trrelssd 14612	The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅)
Theorem	xpcogend 14613	The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷))
Theorem	xpcoidgend 14614	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 14615*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14616 for the main application. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝐵 ⊆ 𝐷    &   ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸    &   ⊢ ran 𝐴 ⊆ 𝐹    ⇒   ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr2 14616*	Two ways of saying a relation is transitive. Special instance of cotr2g 14615. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝑅 ⊆ 𝐴    &   ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵    &   ⊢ ran 𝑅 ⊆ 𝐶    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	cotr3 14617*	Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.)
⊢ 𝐴 = dom 𝑅    &   ⊢ 𝐵 = (𝐴 ∩ 𝐶)    &   ⊢ 𝐶 = ran 𝑅    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	coemptyd 14618	Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	xptrrel 14619	The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
Theorem	0trrel 14620	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (∅ ∘ ∅) ⊆ ∅
5.8.2  Basic properties of closures
Theorem	cleq1lem 14621	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑)))
Theorem	cleq1 14622*	Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)})
Theorem	clsslem 14623*	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 14624	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 14625	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 14626*	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 14627*	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 14628*	Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trclsslem 14629*	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trcleq2lem 14630	Equality implies bijection. (Contributed by RP, 5-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	cvbtrcl 14631*	Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.)
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}
Theorem	trcleq12lem 14632	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	trclexlem 14633	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 14634*	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 14635*	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 14636*	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 14637*	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 14638*	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 14639*	The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})
Theorem	brintclab 14640*	Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.)
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥))
Theorem	brtrclfv 14641*	Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfv 14642*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴)))
Theorem	brtrclfvcnv 14643*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfvcnv 14644*	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 14645	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 14646	The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclfvlb 14647	The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcotr 14648	The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅))
Theorem	trclfvlb2 14649	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅))
Theorem	trclfvlb3 14650	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅))
Theorem	cotrtrclfv 14651	The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅)
Theorem	trclidm 14652	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅))
Theorem	trclun 14653	Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆))))
Theorem	trclfvg 14654	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 14655	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 14656	The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅))
Theorem	dmtrclfv 14657	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 14658	Extend class notation to include relation exponentiation.
class ↑𝑟
Definition	df-relexp 14659*	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 14660	The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.)
⊢ Rel dom ↑𝑟
Theorem	relexp0g 14661	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Theorem	relexp0 14662	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexp0d 14663	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 14664	A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexp1g 14665	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅)
Theorem	dfid5 14666	Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1))
Theorem	dfid6 14667*	Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛))
Theorem	relexp1d 14668	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 14669	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucl 14670	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucr 14671	A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexpsucrd 14672	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 14673	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 14674	Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))
Theorem	relexpcnvd 14675	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 14676	The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.)
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0))
Theorem	relexprelg 14677	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 14678	The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpreld 14679	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 14680	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 14681	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 14682	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 14683	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 14684	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 14685	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 14686	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 14687	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 14688	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpfldd 14689	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 14690	Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))
Theorem	relexpuzrel 14691	The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpaddg 14692	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 14693	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 14694	Extend class notation with recursively defined reflexive, transitive closure.
class t*rec
Definition	df-rtrclrec 14695*	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 14696	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 14697*	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 14698	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 14699	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 14700*	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‘𝑅) ⊆ 𝑠))