Home | Metamath
Proof Explorer Theorem List (p. 410 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | conrel2d 40901 | Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ◡𝐴 = ∅) ⇒ ⊢ (𝜑 → (𝐵 ∘ 𝐴) = ∅) | ||
Theorem | trrelind 40902 | The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) & ⊢ (𝜑 → 𝑇 = (𝑅 ∩ 𝑆)) ⇒ ⊢ (𝜑 → (𝑇 ∘ 𝑇) ⊆ 𝑇) | ||
Theorem | xpintrreld 40903 | The intersection of a transitive relation with a Cartesian product is a transitve relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ∩ (𝐴 × 𝐵))) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | restrreld 40904 | The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 = (𝑅 ↾ 𝐴)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) | ||
Theorem | trrelsuperreldg 40905 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑆 = (dom 𝑅 × ran 𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Theorem | trficl 40906* | The class of all transitive relations has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ (𝑧 ∘ 𝑧) ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | cnvtrrel 40907 | The converse of a transitive relation is a transitive relation. (Contributed by RP, 25-Dec-2019.) |
⊢ ((𝑆 ∘ 𝑆) ⊆ 𝑆 ↔ (◡𝑆 ∘ ◡𝑆) ⊆ ◡𝑆) | ||
Theorem | trrelsuperrel2dg 40908 | Concrete construction of a superclass of relation 𝑅 which is a transitive relation. (Contributed by RP, 20-Jul-2020.) |
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) | ||
Syntax | crcl 40909 | Extend class notation with reflexive closure. |
class r* | ||
Definition | df-rcl 40910* | Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) | ||
Theorem | dfrcl2 40911 | Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | ||
Theorem | dfrcl3 40912 | Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.) |
⊢ r* = (𝑥 ∈ V ↦ ((𝑥↑𝑟0) ∪ (𝑥↑𝑟1))) | ||
Theorem | dfrcl4 40913* | Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020.) |
⊢ r* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ {0, 1} (𝑟↑𝑟𝑛)) | ||
In order for theorems on the transitive closure of a relation to be grouped together before the concept of continuity, we really need an analogue of ↑𝑟 that works on finite ordinals or finite sets instead of natural numbers. | ||
Theorem | relexp2 40914 | A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟2) = (𝑅 ∘ 𝑅)) | ||
Theorem | relexpnul 40915 | If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ Rel 𝑅) ∧ (𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)) → ((dom (𝑅↑𝑟𝑁) ∩ ran (𝑅↑𝑟𝑀)) = ∅ ↔ (𝑅↑𝑟(𝑁 + 𝑀)) = ∅)) | ||
Theorem | eliunov2 40916* | Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. Generalized from dfrtrclrec2 14604. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | eltrclrec 40917* | Membership in the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ 𝑋 ∈ (𝑅↑𝑟𝑛))) | ||
Theorem | elrtrclrec 40918* | Membership in the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ ℕ0 𝑋 ∈ (𝑅↑𝑟𝑛))) | ||
Theorem | briunov2 40919* | Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌)) | ||
Theorem | brmptiunrelexpd 40920* | If two elements are connected by an indexed union of relational powers, then they are connected via 𝑛 instances the relation, for some 𝑛. Generalization of dfrtrclrec2 14604. (Contributed by RP, 21-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) ⇒ ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvmptiunrelexplb0d 40921* | If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → 0 ∈ 𝑁) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (𝐶‘𝑅)) | ||
Theorem | fvmptiunrelexplb0da 40922* | If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 0 ∈ 𝑁) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (𝐶‘𝑅)) | ||
Theorem | fvmptiunrelexplb1d 40923* | If the indexed union ranges over the first power of the relation, then the relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ V) & ⊢ (𝜑 → 1 ∈ 𝑁) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (𝐶‘𝑅)) | ||
Theorem | brfvid 40924 | If two elements are connected by a value of the identity relation, then they are connected via the argument. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | brfvidRP 40925 | If two elements are connected by a value of the identity relation, then they are connected via the argument. This is an example which uses brmptiunrelexpd 40920. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | fvilbd 40926 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | fvilbdRP 40927 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | brfvrcld 40928 | If two elements are connected by the reflexive closure of a relation, then they are connected via zero or one instances the relation. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ (𝐴(𝑅↑𝑟0)𝐵 ∨ 𝐴(𝑅↑𝑟1)𝐵))) | ||
Theorem | brfvrcld2 40929 | If two elements are connected by the reflexive closure of a relation, then they are equal or related by relation. (Contributed by RP, 21-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵))) | ||
Theorem | fvrcllb0d 40930 | A restriction of the identity relation is a subset of the reflexive closure of a set. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (r*‘𝑅)) | ||
Theorem | fvrcllb0da 40931 | A restriction of the identity relation is a subset of the reflexive closure of a relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (r*‘𝑅)) | ||
Theorem | fvrcllb1d 40932 | A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (r*‘𝑅)) | ||
Theorem | brtrclrec 40933* | Two classes related by the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ 𝑋(𝑅↑𝑟𝑛)𝑌)) | ||
Theorem | brrtrclrec 40934* | Two classes related by the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ ℕ0 𝑋(𝑅↑𝑟𝑛)𝑌)) | ||
Theorem | briunov2uz 40935* | Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋(𝐶‘𝑅)𝑌 ↔ ∃𝑛 ∈ 𝑁 𝑋(𝑅 ↑ 𝑛)𝑌)) | ||
Theorem | eliunov2uz 40936* | Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. The index set 𝑁 is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 = (ℤ≥‘𝑀)) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | ov2ssiunov2 40937* | Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 14603 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝑅 ↑ 𝑀) ⊆ (𝐶‘𝑅)) | ||
Theorem | relexp0eq 40938 | The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) → ((dom 𝐴 ∪ ran 𝐴) = (dom 𝐵 ∪ ran 𝐵) ↔ (𝐴↑𝑟0) = (𝐵↑𝑟0))) | ||
Theorem | iunrelexp0 40939* | Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ({0, 1} ∩ 𝑍) ≠ ∅) → (∪ 𝑥 ∈ 𝑍 (𝑅↑𝑟𝑥)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexpxpnnidm 40940 | Any positive power of a Cartesian product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝑁) = (𝐴 × 𝐵))) | ||
Theorem | relexpiidm 40941 | Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) | ||
Theorem | relexpss1d 40942 | The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑟𝑁) ⊆ (𝐵↑𝑟𝑁)) | ||
Theorem | comptiunov2i 40943* | The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.) |
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) & ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) & ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) & ⊢ 𝐼 ∈ V & ⊢ 𝐽 ∈ V & ⊢ 𝐾 = (𝐼 ∪ 𝐽) & ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⇒ ⊢ (𝑋 ∘ 𝑌) = 𝑍 | ||
Theorem | corclrcl 40944 | The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ r*) = r* | ||
Theorem | iunrelexpmin1 40945* | The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∀𝑠((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) | ||
Theorem | relexpmulnn 40946 | With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | relexpmulg 40947 | With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | trclrelexplem 40948* | The union of relational powers to positive multiples of 𝑁 is a subset to the transitive closure raised to the power of 𝑁. (Contributed by RP, 15-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ∪ 𝑘 ∈ ℕ ((𝐷↑𝑟𝑘)↑𝑟𝑁) ⊆ (∪ 𝑗 ∈ ℕ (𝐷↑𝑟𝑗)↑𝑟𝑁)) | ||
Theorem | iunrelexpmin2 40949* | The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0) → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) | ||
Theorem | relexp01min 40950 | With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾)) ∧ (𝐽 ∈ {0, 1} ∧ 𝐾 ∈ {0, 1})) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) | ||
Theorem | relexp1idm 40951 | Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1)↑𝑟1) = (𝑅↑𝑟1)) | ||
Theorem | relexp0idm 40952 | Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟0)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexp0a 40953 | Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0)) | ||
Theorem | relexpxpmin 40954 | The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)) | ||
Theorem | relexpaddss 40955 | The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where 𝑅 is a relation as shown by relexpaddd 14600 or when the sum of the powers isn't 1 as shown by relexpaddg 14599. (Contributed by RP, 3-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ⊆ (𝑅↑𝑟(𝑁 + 𝑀))) | ||
Theorem | iunrelexpuztr 40956* | The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 14606. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = (ℤ≥‘𝑀) ∧ 𝑀 ∈ ℕ0) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅)) | ||
Theorem | dftrcl3 40957* | Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.) |
⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) | ||
Theorem | brfvtrcld 40958* | If two elements are connected by the transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some counting number 𝑛. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvtrcllb1d 40959 | A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t+‘𝑅)) | ||
Theorem | trclfvcom 40960 | The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (𝑅 ∘ (t+‘𝑅))) | ||
Theorem | cnvtrclfv 40961 | The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ◡(t+‘𝑅) = (t+‘◡𝑅)) | ||
Theorem | cotrcltrcl 40962 | The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.) |
⊢ (t+ ∘ t+) = t+ | ||
Theorem | trclimalb2 40963 | Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 “ (𝐴 ∪ 𝐵)) ⊆ 𝐵) → ((t+‘𝑅) “ 𝐴) ⊆ 𝐵) | ||
Theorem | brtrclfv2 40964* | Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋(t+‘𝑅)𝑌 ↔ 𝑌 ∈ ∩ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})) | ||
Theorem | trclfvdecomr 40965 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅))) | ||
Theorem | trclfvdecoml 40966 | The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ (𝑅 ∘ (t+‘𝑅)))) | ||
Theorem | dmtrclfvRP 40967 | The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅) | ||
Theorem | rntrclfvRP 40968 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
Theorem | rntrclfv 40969 | The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
Theorem | dfrtrcl3 40970* | Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 14608. (Contributed by RP, 5-Jun-2020.) |
⊢ t* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) | ||
Theorem | brfvrtrcld 40971* | If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via 𝑛 instances the relation, for some natural number 𝑛. Similar of dfrtrclrec2 14604. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t*‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvrtrcllb0d 40972 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*‘𝑅)) | ||
Theorem | fvrtrcllb0da 40973 | A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*‘𝑅)) | ||
Theorem | fvrtrcllb1d 40974 | A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t*‘𝑅)) | ||
Theorem | dfrtrcl4 40975 | Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.) |
⊢ t* = (𝑟 ∈ V ↦ ((𝑟↑𝑟0) ∪ (t+‘𝑟))) | ||
Theorem | corcltrcl 40976 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.) |
⊢ (r* ∘ t+) = t* | ||
Theorem | cortrcltrcl 40977 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t* ∘ t+) = t* | ||
Theorem | corclrtrcl 40978 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ t*) = t* | ||
Theorem | cotrclrcl 40979 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.) |
⊢ (t+ ∘ r*) = t* | ||
Theorem | cortrclrcl 40980 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t* ∘ r*) = t* | ||
Theorem | cotrclrtrcl 40981 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t+ ∘ t*) = t* | ||
Theorem | cortrclrtrcl 40982 | The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
⊢ (t* ∘ t*) = t* | ||
Theorems inspired by Begriffsschrift without restricting form and content to closely parallel those in [Frege1879]. | ||
Theorem | frege77d 40983 | If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 77 of [Frege1879] p. 62. Compare with frege77 41177. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) & ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege81d 40984 | If the image of 𝑈 is a subset 𝑈, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 81 of [Frege1879] p. 63. Compare with frege81 41181. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege83d 40985 | If the image of the union of 𝑈 and 𝑉 is a subset of the union of 𝑈 and 𝑉, 𝐴 is an element of 𝑈 and 𝐵 follows 𝐴 in the transitive closure of 𝑅, then 𝐵 is an element of the union of 𝑈 and 𝑉. Similar to Proposition 83 of [Frege1879] p. 65. Compare with frege83 41183. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑉)) ⊆ (𝑈 ∪ 𝑉)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑉)) | ||
Theorem | frege96d 40986 | If 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 96 of [Frege1879] p. 71. Compare with frege96 41196. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege87d 40987 | If the images of both {𝐴} and 𝑈 are subsets of 𝑈 and 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 follows 𝐶 in 𝑅, then 𝐵 is an element of 𝑈. Similar to Proposition 87 of [Frege1879] p. 66. Compare with frege87 41187. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶𝑅𝐵) & ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege91d 40988 | If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 41191. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege97d 40989 | If 𝐴 contains all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴. Similar to Proposition 97 of [Frege1879] p. 71. Compare with frege97 41197. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 = ((t+‘𝑅) “ 𝑈)) ⇒ ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | frege98d 40990 | If 𝐶 follows 𝐴 and 𝐵 follows 𝐶 in the transitive closure of 𝑅, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 98 of [Frege1879] p. 71. Compare with frege98 41198. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶(t+‘𝑅)𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege102d 40991 | If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 102 of [Frege1879] p. 72. Compare with frege102 41202. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege106d 40992 | If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅. Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 41206. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege108d 40993 | If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 108 of [Frege1879] p. 74. Compare with frege108 41208. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege109d 40994 | If 𝐴 contains all elements of 𝑈 and all elements after those in 𝑈 in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴. Similar to Proposition 109 of [Frege1879] p. 74. Compare with frege109 41209. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((t+‘𝑅) “ 𝑈))) ⇒ ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | frege114d 40995 | If either 𝑅 relates 𝐴 and 𝐵 or 𝐴 and 𝐵 are the same, then either 𝐴 and 𝐵 are the same, 𝑅 relates 𝐴 and 𝐵, 𝑅 relates 𝐵 and 𝐴. Similar to Proposition 114 of [Frege1879] p. 76. Compare with frege114 41214. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴)) | ||
Theorem | frege111d 40996 | If either 𝐴 and 𝐶 are the same or 𝐶 follows 𝐴 in the transitive closure of 𝑅 and 𝐵 is the successor to 𝐶, then either 𝐴 and 𝐵 are the same or 𝐴 follows 𝐵 or 𝐵 and 𝐴 in the transitive closure of 𝑅. Similar to Proposition 111 of [Frege1879] p. 75. Compare with frege111 41211. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝑅)𝐴)) | ||
Theorem | frege122d 40997 | If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 is the successor of 𝑋, then 𝐴 and 𝐵 are the same (or 𝐵 follows 𝐴 in the transitive closure of 𝐹). Similar to Proposition 122 of [Frege1879] p. 79. Compare with frege122 41222. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝐵 = (𝐹‘𝑋)) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege124d 40998 | If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in the transitive closure of 𝐹. Similar to Proposition 124 of [Frege1879] p. 80. Compare with frege124 41224. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege126d 40999 | If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐵 follows 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹. Similar to Proposition 126 of [Frege1879] p. 81. Compare with frege126 41226. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) | ||
Theorem | frege129d 41000 | If 𝐹 is a function and (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹, the successor of 𝐴 is either 𝐵 or it follows 𝐵 or it comes before 𝐵 in the transitive closure of 𝐹. Similar to Proposition 129 of [Frege1879] p. 83. Comparw with frege129 41229. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴)) & ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |