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	wrd3tpop 14901	A word of length three represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = {⟨0, (𝑊‘0)⟩, ⟨1, (𝑊‘1)⟩, ⟨2, (𝑊‘2)⟩})
Theorem	wrdlen3s3 14902	A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)(𝑊‘2)”⟩)
Theorem	repsw2 14903	The "repeated symbol word" of length two. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = ⟨“𝑆𝑆”⟩)
Theorem	repsw3 14904	The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = ⟨“𝑆𝑆𝑆”⟩)
Theorem	swrd2lsw 14905	Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 substr ⟨((♯‘𝑊) − 2), (♯‘𝑊)⟩) = ⟨“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”⟩)
Theorem	2swrd2eqwrdeq 14906	Two words of length at least two are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))))
Theorem	ccatw2s1ccatws2 14907	The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.) (Revised by AV, 29-Jan-2024.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ ⟨“𝑋𝑌”⟩))
Theorem	ccat2s1fvwALT 14908	Alternate proof of ccat2s1fvw 14590 using words of length 2, see df-s2 14801. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (Revised by AV, 28-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (♯‘𝑊)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	wwlktovf 14909*	Lemma 1 for wrd2f1tovbij 14913. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷⟶𝑅
Theorem	wwlktovf1 14910*	Lemma 2 for wrd2f1tovbij 14913. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷–1-1→𝑅
Theorem	wwlktovfo 14911*	Lemma 3 for wrd2f1tovbij 14913. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅)
Theorem	wwlktovf1o 14912*	Lemma 4 for wrd2f1tovbij 14913. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wrd2f1tovbij 14913*	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 14914	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 14915*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
Theorem	s3sndisj 14916*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {⟨“𝐴𝐵𝑐”⟩})
Theorem	s3iunsndisj 14917*	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 14918	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑇)    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑇)    &   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐺))    &   ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘f 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘f 𝑅𝐺) ++ (𝐹 ∘f 𝑅𝐻)))
Theorem	ofs1 14919	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f 𝑅⟨“𝐵”⟩) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofs2 14920	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 7146. 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 6111. 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 9725, which is a closure relative to a different transitive property, df-tr 5266.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 14921	Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷))
Theorem	trrelssd 14922	The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅)
Theorem	xpcogend 14923	The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷))
Theorem	xpcoidgend 14924	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 14925*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14926 for the main application. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝐵 ⊆ 𝐷    &   ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸    &   ⊢ ran 𝐴 ⊆ 𝐹    ⇒   ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr2 14926*	Two ways of saying a relation is transitive. Special instance of cotr2g 14925. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝑅 ⊆ 𝐴    &   ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵    &   ⊢ ran 𝑅 ⊆ 𝐶    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	cotr3 14927*	Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.)
⊢ 𝐴 = dom 𝑅    &   ⊢ 𝐵 = (𝐴 ∩ 𝐶)    &   ⊢ 𝐶 = ran 𝑅    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	coemptyd 14928	Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	xptrrel 14929	The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
Theorem	0trrel 14930	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (∅ ∘ ∅) ⊆ ∅
5.8.2  Basic properties of closures
Theorem	cleq1lem 14931	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑)))
Theorem	cleq1 14932*	Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)})
Theorem	clsslem 14933*	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 14934	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 14935	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 14936*	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 14937*	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 14938*	Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trclsslem 14939*	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trcleq2lem 14940	Equality implies bijection. (Contributed by RP, 5-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	cvbtrcl 14941*	Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.)
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}
Theorem	trcleq12lem 14942	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	trclexlem 14943	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 14944*	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 14945*	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 14946*	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 14947*	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 14948*	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 14949*	The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})
Theorem	brintclab 14950*	Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.)
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥))
Theorem	brtrclfv 14951*	Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfv 14952*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴)))
Theorem	brtrclfvcnv 14953*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfvcnv 14954*	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 14955	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 14956	The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclfvlb 14957	The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcotr 14958	The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅))
Theorem	trclfvlb2 14959	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅))
Theorem	trclfvlb3 14960	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅))
Theorem	cotrtrclfv 14961	The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅)
Theorem	trclidm 14962	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅))
Theorem	trclun 14963	Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆))))
Theorem	trclfvg 14964	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 14965	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 14966	The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅))
Theorem	dmtrclfv 14967	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 14968	Extend class notation to include relation exponentiation.
class ↑𝑟
Definition	df-relexp 14969*	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 14970	The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.)
⊢ Rel dom ↑𝑟
Theorem	relexp0g 14971	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Theorem	relexp0 14972	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexp0d 14973	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 14974	A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexp1g 14975	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅)
Theorem	dfid5 14976	Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1))
Theorem	dfid6 14977*	Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛))
Theorem	relexp1d 14978	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 14979	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucl 14980	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucr 14981	A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexpsucrd 14982	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 14983	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 14984	Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))
Theorem	relexpcnvd 14985	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 14986	The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.)
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0))
Theorem	relexprelg 14987	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 14988	The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpreld 14989	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 14990	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 14991	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 14992	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 14993	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 14994	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 14995	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 14996	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 14997	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 14998	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)
Theorem	relexpfldd 14999	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 15000	Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))