P. 144 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14301-14400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrdlen2s2 14301	A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrdl2exs2 14302*	A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 2) → ∃𝑠 ∈ 𝑆 ∃𝑡 ∈ 𝑆 𝑊 = ⟨“𝑠𝑡”⟩)
Theorem	pfx2 14303	A prefix of length two. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrd3tpop 14304	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 14305	A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)(𝑊‘2)”⟩)
Theorem	repsw2 14306	The "repeated symbol word" of length two. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = ⟨“𝑆𝑆”⟩)
Theorem	repsw3 14307	The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = ⟨“𝑆𝑆𝑆”⟩)
Theorem	swrd2lsw 14308	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 14309	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 14310	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	ccatw2s1ccatws2OLD 14311	Obsolete version of ccatw2s1ccatws2 14310 as of 29-Jan-2024. 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.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ ⟨“𝑋𝑌”⟩))
Theorem	ccat2s1fvwALT 14312	Alternate proof of ccat2s1fvw 13992 using words of length 2, see df-s2 14204. 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	ccat2s1fvwALTOLD 14313	Obsolete version of ccat2s1fvwALT 14312 as of 28-Jan-2024. Alternate proof of ccat2s1fvwOLD 13993 using words of length 2, see df-s2 14204. 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.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	wwlktovf 14314*	Lemma 1 for wrd2f1tovbij 14318. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷⟶𝑅
Theorem	wwlktovf1 14315*	Lemma 2 for wrd2f1tovbij 14318. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷–1-1→𝑅
Theorem	wwlktovfo 14316*	Lemma 3 for wrd2f1tovbij 14318. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅)
Theorem	wwlktovf1o 14317*	Lemma 4 for wrd2f1tovbij 14318. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wrd2f1tovbij 14318*	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 14319	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 14320*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
Theorem	s3sndisj 14321*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {⟨“𝐴𝐵𝑐”⟩})
Theorem	s3iunsndisj 14322*	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 14323	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑇)    &   ⊢ (𝜑 → 𝐻 ∈ Word 𝑇)    &   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐺))    &   ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘f 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘f 𝑅𝐺) ++ (𝐹 ∘f 𝑅𝐻)))
Theorem	ofs1 14324	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f 𝑅⟨“𝐵”⟩) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofs2 14325	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 6902. 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 5966. 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 9164, which is a closure relative to a different transitive property, df-tr 5165.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 14326	Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷))
Theorem	trrelssd 14327	The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑅)    ⇒   ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅)
Theorem	xpcogend 14328	The most interesting case of the composition of two cross products. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷))
Theorem	xpcoidgend 14329	If two classes are not disjoint, then the composition of their cross-product with itself is idempotent. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐵))
Theorem	cotr2g 14330*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14331 for the main application. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝐵 ⊆ 𝐷    &   ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸    &   ⊢ ran 𝐴 ⊆ 𝐹    ⇒   ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Theorem	cotr2 14331*	Two ways of saying a relation is transitive. Special instance of cotr2g 14330. (Contributed by RP, 22-Mar-2020.)
⊢ dom 𝑅 ⊆ 𝐴    &   ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵    &   ⊢ ran 𝑅 ⊆ 𝐶    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	cotr3 14332*	Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.)
⊢ 𝐴 = dom 𝑅    &   ⊢ 𝐵 = (𝐴 ∩ 𝐶)    &   ⊢ 𝐶 = ran 𝑅    ⇒   ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
Theorem	coemptyd 14333	Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅)
Theorem	xptrrel 14334	The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
Theorem	0trrel 14335	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
⊢ (∅ ∘ ∅) ⊆ ∅
5.8.2  Basic properties of closures
Theorem	cleq1lem 14336	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑)))
Theorem	cleq1 14337*	Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)})
Theorem	clsslem 14338*	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 14339	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 14340	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 14341*	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 14342*	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 14343*	Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trclsslem 14344*	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)})
Theorem	trcleq2lem 14345	Equality implies bijection. (Contributed by RP, 5-May-2020.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	cvbtrcl 14346*	Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.)
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}
Theorem	trcleq12lem 14347	Equality implies bijection. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
Theorem	trclexlem 14348	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 14349*	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 14350*	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 14351*	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 14352*	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 14353*	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 14354*	The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)})
Theorem	brintclab 14355*	Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.)
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥))
Theorem	brtrclfv 14356*	Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfv 14357*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴)))
Theorem	brtrclfvcnv 14358*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵)))
Theorem	brcnvtrclfvcnv 14359*	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 14360	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 14361	The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclfvlb 14362	The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅))
Theorem	trclfvcotr 14363	The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅))
Theorem	trclfvlb2 14364	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅))
Theorem	trclfvlb3 14365	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅))
Theorem	cotrtrclfv 14366	The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅)
Theorem	trclidm 14367	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅))
Theorem	trclun 14368	Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆))))
Theorem	trclfvg 14369	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 14370	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 14371	The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅))
Theorem	dmtrclfv 14372	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 14373	Extend class notation to include relation exponentiation.
class ↑𝑟
Definition	df-relexp 14374*	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	relexp0g 14375	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Theorem	relexp0 14376	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexp0d 14377	A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
Theorem	relexpsucnnr 14378	A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexp1g 14379	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅)
Theorem	dfid5 14380	Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1))
Theorem	dfid6 14381*	Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.)
⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛))
Theorem	relexpsucr 14382	A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅))
Theorem	relexpsucrd 14383	A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑁 ∈ ℕ0 → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)))
Theorem	relexp1d 14384	A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑅↑𝑟1) = 𝑅)
Theorem	relexpsucnnl 14385	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucl 14386	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))
Theorem	relexpsucld 14387	A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑁 ∈ ℕ0 → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))))
Theorem	relexpcnv 14388	Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))
Theorem	relexpcnvd 14389	Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑁 ∈ ℕ0 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)))
Theorem	relexp0rel 14390	The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.)
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0))
Theorem	relexprelg 14391	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 14392	The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁))
Theorem	relexpreld 14393	The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑁 ∈ ℕ0 → Rel (𝑅↑𝑟𝑁)))
Theorem	relexpnndm 14394	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 14395	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 14396	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 14397	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.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → (𝑁 ∈ ℕ0 → dom (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅))
Theorem	relexpnnrn 14398	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 14399	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 14400	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ran (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅)