HomeTheorem List (p. 148 of 466)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 148 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 0trrel 14701 | The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (∅ ∘ ∅) ⊆ ∅ | ||
| Theorem | cleq1lem 14702 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑))) | ||
| Theorem | cleq1 14703* | Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
| Theorem | clsslem 14704* | The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.) |
| ⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
| Syntax | ctcl 14705 | Extend class notation to include the transitive closure symbol. |
| class t+ | ||
| Syntax | crtcl 14706 | Extend class notation with reflexive-transitive closure. |
| class t* | ||
| Definition | df-trcl 14707* | 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 14708* | 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 14709* | Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
| Theorem | trclsslem 14710* | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
| ⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
| Theorem | trcleq2lem 14711 | Equality implies bijection. (Contributed by RP, 5-May-2020.) |
| ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
| Theorem | cvbtrcl 14712* | Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.) |
| ⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)} | ||
| Theorem | trcleq12lem 14713 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
| Theorem | trclexlem 14714 | 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 14715* | 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 14716* | 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 14717* | 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 14718* | 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 14719* | 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 14720* | The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) | ||
| Theorem | brintclab 14721* | Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.) |
| ⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥)) | ||
| Theorem | brtrclfv 14722* | Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
| Theorem | brcnvtrclfv 14723* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴))) | ||
| Theorem | brtrclfvcnv 14724* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
| Theorem | brcnvtrclfvcnv 14725* | 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 14726 | 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 14727 | The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
| Theorem | trclfvlb 14728 | The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvcotr 14729 | The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvlb2 14730 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅)) | ||
| Theorem | trclfvlb3 14731 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅)) | ||
| Theorem | cotrtrclfv 14732 | The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅) | ||
| Theorem | trclidm 14733 | The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅)) | ||
| Theorem | trclun 14734 | Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆)))) | ||
| Theorem | trclfvg 14735 | 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 14736 | 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 14737 | The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅)) | ||
| Theorem | dmtrclfv 14738 | 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 14739 | Extend class notation to include relation exponentiation. |
| class ↑𝑟 | ||
| Definition | df-relexp 14740* | 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 14741 | The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.) |
| ⊢ Rel dom ↑𝑟 | ||
| Theorem | relexp0g 14742 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | ||
| Theorem | relexp0 14743 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅)) | ||
| Theorem | relexp0d 14744 | 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 14745 | A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
| Theorem | relexp1g 14746 | A relation composed once is itself. (Contributed by RP, 22-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) | ||
| Theorem | dfid5 14747 | Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.) |
| ⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1)) | ||
| Theorem | dfid6 14748* | Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.) |
| ⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛)) | ||
| Theorem | relexp1d 14749 | 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 14750 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
| Theorem | relexpsucl 14751 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
| Theorem | relexpsucr 14752 | A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
| Theorem | relexpsucrd 14753 | 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 14754 | 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 14755 | Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | ||
| Theorem | relexpcnvd 14756 | 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 14757 | The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0)) | ||
| Theorem | relexprelg 14758 | 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 14759 | The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁)) | ||
| Theorem | relexpreld 14760 | 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 14761 | 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 14762 | 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 14763 | 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 14764 | 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 14765 | 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 14766 | 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 14767 | 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 14768 | 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 14769 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) | ||
| Theorem | relexpfldd 14770 | 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 14771 | Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | ||
| Theorem | relexpuzrel 14772 | 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 14773 | 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 14774 | 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 14775 | Extend class notation with recursively defined reflexive, transitive closure. |
| class t*rec | ||
| Definition | df-rtrclrec 14776* | 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 14777 | 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 14778* | 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 14779 | 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 14780 | 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 14781* | 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 14782 | 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‘𝑅)) | ||
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 14783* | 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 14784* | 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 14785* | 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*‘𝑅)𝑋 → 𝜏)) | ||
| Syntax | cshi 14786 | Extend class notation with function shifter. |
| class shift | ||
| Definition | df-shft 14787* | Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of ℂ) and produces a new function on ℂ. See shftval 14794 for its value. (Contributed by NM, 20-Jul-2005.) |
| ⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) | ||
| Theorem | shftlem 14788* | Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) | ||
| Theorem | shftuz 14789* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) | ||
| Theorem | shftfval 14790* | The value of the sequence shifter operation is a function on ℂ. 𝐴 is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → (𝐹 shift 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ (𝑥 − 𝐴)𝐹𝑦)}) | ||
| Theorem | shftdm 14791* | Domain of a relation shifted by 𝐴. The set on the right is more commonly notated as (dom 𝐹 + 𝐴) (meaning add 𝐴 to every element of dom 𝐹). (Contributed by Mario Carneiro, 3-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → dom (𝐹 shift 𝐴) = {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ dom 𝐹}) | ||
| Theorem | shftfib 14792 | Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) | ||
| Theorem | shftfn 14793* | Functionality and domain of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}) | ||
| Theorem | shftval 14794 | Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
| Theorem | shftval2 14795 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) | ||
| Theorem | shftval3 14796 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) | ||
| Theorem | shftval4 14797 | Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) | ||
| Theorem | shftval5 14798 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) | ||
| Theorem | shftf 14799* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) | ||
| Theorem | 2shfti 14800 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |