Home | Metamath
Proof Explorer Theorem List (p. 149 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cleq1lem 14801 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑))) | ||
Theorem | cleq1 14802* | Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
Theorem | clsslem 14803* | The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.) |
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
Syntax | ctcl 14804 | Extend class notation to include the transitive closure symbol. |
class t+ | ||
Syntax | crtcl 14805 | Extend class notation with reflexive-transitive closure. |
class t* | ||
Definition | df-trcl 14806* | 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 14807* | 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 14808* | Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
Theorem | trclsslem 14809* | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
Theorem | trcleq2lem 14810 | Equality implies bijection. (Contributed by RP, 5-May-2020.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | cvbtrcl 14811* | Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.) |
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)} | ||
Theorem | trcleq12lem 14812 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | trclexlem 14813 | 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 14814* | 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 14815* | 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 14816* | 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 14817* | 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 14818* | 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 14819* | The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) | ||
Theorem | brintclab 14820* | Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.) |
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑥)) | ||
Theorem | brtrclfv 14821* | Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
Theorem | brcnvtrclfv 14822* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.) |
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴))) | ||
Theorem | brtrclfvcnv 14823* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
Theorem | brcnvtrclfvcnv 14824* | 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 14825 | 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 14826 | The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclfvlb 14827 | The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) | ||
Theorem | trclfvcotr 14828 | The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅)) | ||
Theorem | trclfvlb2 14829 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅)) | ||
Theorem | trclfvlb3 14830 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅)) | ||
Theorem | cotrtrclfv 14831 | The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) → (t+‘𝑅) = 𝑅) | ||
Theorem | trclidm 14832 | The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘(t+‘𝑅)) = (t+‘𝑅)) | ||
Theorem | trclun 14833 | Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (t+‘(𝑅 ∪ 𝑆)) = (t+‘((t+‘𝑅) ∪ (t+‘𝑆)))) | ||
Theorem | trclfvg 14834 | 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 14835 | 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 14836 | The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (t+‘𝑅)) | ||
Theorem | dmtrclfv 14837 | 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 14838 | Extend class notation to include relation exponentiation. |
class ↑𝑟 | ||
Definition | df-relexp 14839* | 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 14840 | The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.) |
⊢ Rel dom ↑𝑟 | ||
Theorem | relexp0g 14841 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | ||
Theorem | relexp0 14842 | A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅)) | ||
Theorem | relexp0d 14843 | 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 14844 | A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
Theorem | relexp1g 14845 | A relation composed once is itself. (Contributed by RP, 22-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) | ||
Theorem | dfid5 14846 | Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.) |
⊢ I = (𝑥 ∈ V ↦ (𝑥↑𝑟1)) | ||
Theorem | dfid6 14847* | Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∪ 𝑛 ∈ {1} (𝑥↑𝑟𝑛)) | ||
Theorem | relexp1d 14848 | 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 14849 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
Theorem | relexpsucl 14850 | A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) | ||
Theorem | relexpsucr 14851 | A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅 ∧ 𝑁 ∈ ℕ0) → (𝑅↑𝑟(𝑁 + 1)) = ((𝑅↑𝑟𝑁) ∘ 𝑅)) | ||
Theorem | relexpsucrd 14852 | 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 14853 | 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 14854 | Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | ||
Theorem | relexpcnvd 14855 | 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 14856 | The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0)) | ||
Theorem | relexprelg 14857 | 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 14858 | The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ Rel 𝑅) → Rel (𝑅↑𝑟𝑁)) | ||
Theorem | relexpreld 14859 | 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 14860 | 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 14861 | 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 14862 | 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 14863 | 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 14864 | 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 14865 | 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 14866 | 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 14867 | 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 14868 | The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ∪ ∪ (𝑅↑𝑟𝑁) ⊆ ∪ ∪ 𝑅) | ||
Theorem | relexpfldd 14869 | 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 14870 | Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | ||
Theorem | relexpuzrel 14871 | 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 14872 | 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 14873 | 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 14874 | Extend class notation with recursively defined reflexive, transitive closure. |
class t*rec | ||
Definition | df-rtrclrec 14875* | 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 14876 | 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 14877* | 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 14878 | 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 14879 | 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 14880* | 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 14881 | 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 14882* | 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 14883* | 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 14884* | 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 14885 | Extend class notation with function shifter. |
class shift | ||
Definition | df-shft 14886* | 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 14893 for its value. (Contributed by NM, 20-Jul-2005.) |
⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) | ||
Theorem | shftlem 14887* | Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)}) | ||
Theorem | shftuz 14888* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ (ℤ≥‘𝐵)} = (ℤ≥‘(𝐵 + 𝐴))) | ||
Theorem | shftfval 14889* | 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 14890* | 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 14891 | Value of a fiber of the relation 𝐹. (Contributed by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) | ||
Theorem | shftfn 14892* | 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 14893 | Value of a sequence shifted by 𝐴. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴))) | ||
Theorem | shftval2 14894 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘(𝐴 + 𝐶)) = (𝐹‘(𝐵 + 𝐶))) | ||
Theorem | shftval3 14895 | Value of a sequence shifted by 𝐴 − 𝐵. (Contributed by NM, 20-Jul-2005.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift (𝐴 − 𝐵))‘𝐴) = (𝐹‘𝐵)) | ||
Theorem | shftval4 14896 | Value of a sequence shifted by -𝐴. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) | ||
Theorem | shftval5 14897 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘(𝐵 + 𝐴)) = (𝐹‘𝐵)) | ||
Theorem | shftf 14898* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴):{𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵}⟶𝐶) | ||
Theorem | 2shfti 14899 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) shift 𝐵) = (𝐹 shift (𝐴 + 𝐵))) | ||
Theorem | shftidt2 14900 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |