| Metamath
Proof Explorer Theorem List (p. 151 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | wrdl3s3 15001* | A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) | ||
| Theorem | s2rn 15002 | Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.) |
| ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽”〉 = {𝐼, 𝐽}) | ||
| Theorem | s3rn 15003 | Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.) |
| ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐾 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽𝐾”〉 = {𝐼, 𝐽, 𝐾}) | ||
| Theorem | s7rn 15004 | Range of a length 7 string. (Contributed by AV, 30-Jul-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})) | ||
| Theorem | s7f1o 15005 | 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 15006* | The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.) |
| ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {〈“𝐴𝐵𝑐”〉}) | ||
| Theorem | s3iunsndisj 15007* | 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 15008 | Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
| ⊢ (𝜑 → 𝐸 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑇) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑇) & ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐺)) & ⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐻)) ⇒ ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘f 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘f 𝑅𝐺) ++ (𝐹 ∘f 𝑅𝐻))) | ||
| Theorem | ofs1 15009 | Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
| ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (〈“𝐴”〉 ∘f 𝑅〈“𝐵”〉) = 〈“(𝐴𝑅𝐵)”〉) | ||
| Theorem | ofs2 15010 | Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
| ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇)) → (〈“𝐴𝐵”〉 ∘f 𝑅〈“𝐶𝐷”〉) = 〈“(𝐴𝑅𝐶)(𝐵𝑅𝐷)”〉) | ||
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 7166. 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 6130. 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 9768, which is a closure relative to a different transitive property, df-tr 5260. | ||
| Theorem | coss12d 15011 | Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷)) | ||
| Theorem | trrelssd 15012 | The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ 𝑅) & ⊢ (𝜑 → 𝑇 ⊆ 𝑅) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅) | ||
| Theorem | xpcogend 15013 | The most interesting case of the composition of two Cartesian products. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷)) | ||
| Theorem | xpcoidgend 15014 | 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 15015* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 15016 for the main application. (Contributed by RP, 22-Mar-2020.) |
| ⊢ dom 𝐵 ⊆ 𝐷 & ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸 & ⊢ ran 𝐴 ⊆ 𝐹 ⇒ ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
| Theorem | cotr2 15016* | Two ways of saying a relation is transitive. Special instance of cotr2g 15015. (Contributed by RP, 22-Mar-2020.) |
| ⊢ dom 𝑅 ⊆ 𝐴 & ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵 & ⊢ ran 𝑅 ⊆ 𝐶 ⇒ ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
| Theorem | cotr3 15017* | Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.) |
| ⊢ 𝐴 = dom 𝑅 & ⊢ 𝐵 = (𝐴 ∩ 𝐶) & ⊢ 𝐶 = ran 𝑅 ⇒ ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
| Theorem | coemptyd 15018 | Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
| Theorem | xptrrel 15019 | The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) | ||
| Theorem | 0trrel 15020 | The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (∅ ∘ ∅) ⊆ ∅ | ||
| Theorem | cleq1lem 15021 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑))) | ||
| Theorem | cleq1 15022* | Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
| Theorem | clsslem 15023* | The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.) |
| ⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
| Syntax | ctcl 15024 | Extend class notation to include the transitive closure symbol. |
| class t+ | ||
| Syntax | crtcl 15025 | Extend class notation with reflexive-transitive closure. |
| class t* | ||
| Definition | df-trcl 15026* | 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 15027* | 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 15028* | Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
| Theorem | trclsslem 15029* | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
| ⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
| Theorem | trcleq2lem 15030 | Equality implies bijection. (Contributed by RP, 5-May-2020.) |
| ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
| Theorem | cvbtrcl 15031* | Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.) |
| ⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)} | ||
| Theorem | trcleq12lem 15032 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
| Theorem | trclexlem 15033 | 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 15034* | 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 15035* | 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 15036* | 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 15037* | 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 15038* | 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 15039* | The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) | ||
| Theorem | brintclab 15040* | Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.) |
| ⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑥)) | ||
| Theorem | brtrclfv 15041* | Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
| Theorem | brcnvtrclfv 15042* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴))) | ||
| Theorem | brtrclfvcnv 15043* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
| Theorem | brcnvtrclfvcnv 15044* | 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 15045 | 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 15046 | The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
| Theorem | trclfvlb 15047 | The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvcotr 15048 | The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvlb2 15049 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvlb3 15050 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅)) | ||
| Theorem | cotrtrclfv 15051 | The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅) | ||
| Theorem | trclidm 15052 | The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅)) | ||
| Theorem | trclun 15053 | Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆)))) | ||
| Theorem | trclfvg 15054 | 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 15055 | 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 15056 | The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅)) | ||
| Theorem | dmtrclfv 15057 | The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅) | ||
| Syntax | crelexp 15058 | Extend class notation to include relation exponentiation. |
| class ↑𝑟 | ||
| Definition | df-relexp 15059* | 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 15060 | The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.) |
| ⊢ Rel dom ↑𝑟 | ||
| Theorem | relexp0g 15061 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | ||
| Theorem | relexp0 15062 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅)) | ||
| Theorem | relexp0d 15063 | 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 15064 | A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
| Theorem | relexp1g 15065 | A relation composed once is itself. (Contributed by RP, 22-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) | ||
| Theorem | dfid5 15066 | Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.) |
| ⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1)) | ||
| Theorem | dfid6 15067* | Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.) |
| ⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛)) | ||
| Theorem | relexp1d 15068 | 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 15069 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
| Theorem | relexpsucl 15070 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
| Theorem | relexpsucr 15071 | A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
| Theorem | relexpsucrd 15072 | 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 15073 | 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 15074 | Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | ||
| Theorem | relexpcnvd 15075 | 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 15076 | The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0)) | ||
| Theorem | relexprelg 15077 | 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 15078 | The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁)) | ||
| Theorem | relexpreld 15079 | 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 15080 | 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 15081 | 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 15082 | 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 15083 | 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 15084 | 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 15085 | 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 15086 | 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 15087 | 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 15088 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) | ||
| Theorem | relexpfldd 15089 | 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 15090 | Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | ||
| Theorem | relexpuzrel 15091 | 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 15092 | 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 15093 | 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) ⇒ ⊢ (𝜑 → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | ||
| Syntax | crtrcl 15094 | Extend class notation with recursively defined reflexive, transitive closure. |
| class t*rec | ||
| Definition | df-rtrclrec 15095* | 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 15096 | 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 15097* | 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 15098 | 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 15099 | 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 15100* | 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‘𝑅) ⊆ 𝑠)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |