Home | Metamath
Proof Explorer Theorem List (p. 400 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfrcl4 39901* | 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 39902 | 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 39903 | 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 39904* | 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 14406. (Contributed by RP, 1-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉) → (𝑋 ∈ (𝐶‘𝑅) ↔ ∃𝑛 ∈ 𝑁 𝑋 ∈ (𝑅 ↑ 𝑛))) | ||
Theorem | eltrclrec 39905* | 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 39906* | 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 39907* | 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 39908* | 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 14406. (Contributed by RP, 21-Jul-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) & ⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝑁 ⊆ ℕ0) ⇒ ⊢ (𝜑 → (𝐴(𝐶‘𝑅)𝐵 ↔ ∃𝑛 ∈ 𝑁 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvmptiunrelexplb0d 39909* | 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 39910* | 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 39911* | 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 39912 | 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 39913 | 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 39908. (Contributed by RP, 21-Jul-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴( I ‘𝑅)𝐵 ↔ 𝐴𝑅𝐵)) | ||
Theorem | fvilbd 39914 | A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ ( I ‘𝑅)) | ||
Theorem | fvilbdRP 39915 | 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 39916 | 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 39917 | 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 39918 | 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 39919 | 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 39920 | A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (r*‘𝑅)) | ||
Theorem | brtrclrec 39921* | 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 39922* | 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 39923* | 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 39924* | 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 39925* | Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 14407 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟 ↑ 𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁) → (𝑅 ↑ 𝑀) ⊆ (𝐶‘𝑅)) | ||
Theorem | relexp0eq 39926 | 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 39927* | Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ({0, 1} ∩ 𝑍) ≠ ∅) → (∪ 𝑥 ∈ 𝑍 (𝑅↑𝑟𝑥)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexpxpnnidm 39928 | Any positive power of a cross product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) → ((𝐴 × 𝐵)↑𝑟𝑁) = (𝐴 × 𝐵))) | ||
Theorem | relexpiidm 39929 | Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) | ||
Theorem | relexpss1d 39930 | The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑟𝑁) ⊆ (𝐵↑𝑟𝑁)) | ||
Theorem | comptiunov2i 39931* | The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.) |
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) & ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) & ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) & ⊢ 𝐼 ∈ V & ⊢ 𝐽 ∈ V & ⊢ 𝐾 = (𝐼 ∪ 𝐽) & ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) & ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⇒ ⊢ (𝑋 ∘ 𝑌) = 𝑍 | ||
Theorem | corclrcl 39932 | The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ r*) = r* | ||
Theorem | iunrelexpmin1 39933* | 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 39934 | 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 39935 | 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 39936* | 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 39937* | 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 39938 | 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 39939 | Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1)↑𝑟1) = (𝑅↑𝑟1)) | ||
Theorem | relexp0idm 39940 | Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟0)↑𝑟0) = (𝑅↑𝑟0)) | ||
Theorem | relexp0a 39941 | Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴↑𝑟𝑁)↑𝑟0) ⊆ (𝐴↑𝑟0)) | ||
Theorem | relexpxpmin 39942 | The composition of powers of a cross-product of non-disjoint sets is the cross product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) ≠ ∅) ∧ (𝐼 = if(𝐽 < 𝐾, 𝐽, 𝐾) ∧ 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)) → (((𝐴 × 𝐵)↑𝑟𝐽)↑𝑟𝐾) = ((𝐴 × 𝐵)↑𝑟𝐼)) | ||
Theorem | relexpaddss 39943 | 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 14403 or when the sum of the powers isn't 1 as shown by relexpaddg 14402. (Contributed by RP, 3-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ⊆ (𝑅↑𝑟(𝑁 + 𝑀))) | ||
Theorem | iunrelexpuztr 39944* | The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 14409. (Contributed by RP, 4-Jun-2020.) |
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = (ℤ≥‘𝑀) ∧ 𝑀 ∈ ℕ0) → ((𝐶‘𝑅) ∘ (𝐶‘𝑅)) ⊆ (𝐶‘𝑅)) | ||
Theorem | dftrcl3 39945* | Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.) |
⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) | ||
Theorem | brfvtrcld 39946* | 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 39947 | A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t+‘𝑅)) | ||
Theorem | trclfvcom 39948 | The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (𝑅 ∘ (t+‘𝑅))) | ||
Theorem | cnvtrclfv 39949 | 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 39950 | The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.) |
⊢ (t+ ∘ t+) = t+ | ||
Theorem | trclimalb2 39951 | Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑅 “ (𝐴 ∪ 𝐵)) ⊆ 𝐵) → ((t+‘𝑅) “ 𝐴) ⊆ 𝐵) | ||
Theorem | brtrclfv2 39952* | Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋(t+‘𝑅)𝑌 ↔ 𝑌 ∈ ∩ {𝑓 ∣ (𝑅 “ ({𝑋} ∪ 𝑓)) ⊆ 𝑓})) | ||
Theorem | trclfvdecomr 39953 | 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 39954 | 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 39955 | 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 39956 | 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 39957 | 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 39958* | Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 14411. (Contributed by RP, 5-Jun-2020.) |
⊢ t* = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) | ||
Theorem | brfvrtrcld 39959* | 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 14406. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → (𝐴(t*‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) | ||
Theorem | fvrtrcllb0d 39960 | 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 39961 | 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 39962 | A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (t*‘𝑅)) | ||
Theorem | dfrtrcl4 39963 | 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 39964 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.) |
⊢ (r* ∘ t+) = t* | ||
Theorem | cortrcltrcl 39965 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t* ∘ t+) = t* | ||
Theorem | corclrtrcl 39966 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (r* ∘ t*) = t* | ||
Theorem | cotrclrcl 39967 | The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.) |
⊢ (t+ ∘ r*) = t* | ||
Theorem | cortrclrcl 39968 | Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t* ∘ r*) = t* | ||
Theorem | cotrclrtrcl 39969 | Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.) |
⊢ (t+ ∘ t*) = t* | ||
Theorem | cortrclrtrcl 39970 | 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 39971 | 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 40166. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) & ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege81d 39972 | 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 40170. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege83d 39973 | 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 40172. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) & ⊢ (𝜑 → (𝑅 “ (𝑈 ∪ 𝑉)) ⊆ (𝑈 ∪ 𝑉)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∪ 𝑉)) | ||
Theorem | frege96d 39974 | 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 40185. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege87d 39975 | 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 40176. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶𝑅𝐵) & ⊢ (𝜑 → (𝑅 “ {𝐴}) ⊆ 𝑈) & ⊢ (𝜑 → (𝑅 “ 𝑈) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | frege91d 39976 | If 𝐵 follows 𝐴 in 𝑅 then 𝐵 follows 𝐴 in the transitive closure of 𝑅. Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 40180. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege97d 39977 | 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 40186. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 = ((t+‘𝑅) “ 𝑈)) ⇒ ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | frege98d 39978 | 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 40187. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐶) & ⊢ (𝜑 → 𝐶(t+‘𝑅)𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege102d 39979 | 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 40191. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴(t+‘𝑅)𝐵) | ||
Theorem | frege106d 39980 | If 𝐵 follows 𝐴 in 𝑅, then either 𝐴 and 𝐵 are the same or 𝐵 follows 𝐴 in 𝑅. Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 40195. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege108d 39981 | 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 40197. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege109d 39982 | 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 40198. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((t+‘𝑅) “ 𝑈))) ⇒ ⊢ (𝜑 → (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | frege114d 39983 | 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 40203. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵𝑅𝐴)) | ||
Theorem | frege111d 39984 | 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 40200. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐶 ∨ 𝐴 = 𝐶)) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝑅)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝑅)𝐴)) | ||
Theorem | frege122d 39985 | 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 40211. (Contributed by RP, 15-Jul-2020.) |
⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝐵 = (𝐹‘𝑋)) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege124d 39986 | 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 40213. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | frege126d 39987 | 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 40215. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝑋 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐴 = (𝐹‘𝑋)) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) | ||
Theorem | frege129d 39988 | 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 40218. (Contributed by RP, 16-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐹) & ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴)) & ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐵(t+‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(t+‘𝐹)𝐵)) | ||
Theorem | frege131d 39989 | If 𝐹 is a function and 𝐴 contains all elements of 𝑈 and all elements before or after those elements of 𝑈 in the transitive closure of 𝐹, then the image under 𝐹 of 𝐴 is a subclass of 𝐴. Similar to Proposition 131 of [Frege1879] p. 85. Compare with frege131 40220. (Contributed by RP, 17-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(t+‘𝐹) “ 𝑈) ∪ ((t+‘𝐹) “ 𝑈)))) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴) | ||
Theorem | frege133d 39990 | If 𝐹 is a function and 𝐴 and 𝐵 both follow 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹 (or both if it loops). Similar to Proposition 133 of [Frege1879] p. 86. Compare with frege133 40222. (Contributed by RP, 18-Jul-2020.) |
⊢ (𝜑 → 𝐹 ∈ V) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐴) & ⊢ (𝜑 → 𝑋(t+‘𝐹)𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → (𝐴(t+‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(t+‘𝐹)𝐴)) | ||
In 1879, Frege introduced notation for documenting formal reasoning about propositions (and classes) which covered elements of propositional logic, predicate calculus and reasoning about relations. However, due to the pitfalls of naive set theory, adapting this work for inclusion in set.mm required dividing statements about propositions from those about classes and identifying when a restriction to sets is required. For an overview comparing the details of Frege's two-dimensional notation and that used in set.mm, see mmfrege.html. See ru 3770 for discussion of an example of a class that is not a set. Numbered propositions from [Frege1879]. ax-frege1 40016, ax-frege2 40017, ax-frege8 40035, ax-frege28 40056, ax-frege31 40060, ax-frege41 40071, frege52 (see ax-frege52a 40083, frege52b 40115, and ax-frege52c 40114 for translations), frege54 (see ax-frege54a 40088, frege54b 40119 and ax-frege54c 40118 for translations) and frege58 (see ax-frege58a 40101, ax-frege58b 40127 and frege58c 40147 for translations) are considered "core" or axioms. However, at least ax-frege8 40035 can be derived from ax-frege1 40016 and ax-frege2 40017, see axfrege8 40033. Frege introduced implication, negation and the universal quantifier as primitives and did not in the numbered propositions use other logical connectives other than equivalence introduced in ax-frege52a 40083, frege52b 40115, and ax-frege52c 40114. In dffrege69 40158, Frege introduced 𝑅 hereditary 𝐴 to say that relation 𝑅, when restricted to operate on elements of class 𝐴, will only have elements of class 𝐴 in its domain; see df-he 39999 for a definition in terms of image and subset. In dffrege76 40165, Frege introduced notation for the concept of two sets related by the transitive closure of a relation, for which we write 𝑋(t+‘𝑅)𝑌, which requires 𝑅 to also be a set. In dffrege99 40188, Frege introduced notation for the concept of two sets either identical or related by the transitive closure of a relation, for which we write 𝑋((t+‘𝑅) ∪ I )𝑌, which is a superclass of sets related by the reflexive-transitive relation 𝑋(t*‘𝑅)𝑌. Finally, in dffrege115 40204, Frege introduced notation for the concept of a relation having the property elements in its domain pair up with only one element each in its range, for which we write Fun ◡◡𝑅 (to ignore any non-relational content of the class 𝑅). Frege did this without the expressing concept of a relation (or its transitive closure) as a class, and needed to invent conventions for discussing indeterminate propositions with two slots free and how to recognize which of the slots was domain and which was range. See mmfrege.html 40204 for details. English translations for specific propositions lifted in part from a translation by Stefan Bauer-Mengelberg as reprinted in From Frege to Goedel: A Source Book in Mathematical Logic, 1879-1931. An attempt to align these propositions in the larger set.mm database has also been made. See frege77d 39971 for an example. | ||
Section 2 introduces the turnstile ⊢ which turns an idea which may be true 𝜑 into an assertion that it does hold true ⊢ 𝜑. Section 5 introduces implication, (𝜑 → 𝜓). Section 6 introduces the single rule of interference relied upon, modus ponens ax-mp 5. Section 7 introduces negation and with in synonyms for or (¬ 𝜑 → 𝜓), and ¬ (𝜑 → ¬ 𝜓), and two for exclusive-or corresponding to df-or 842, df-an 397, dfxor4 39991, dfxor5 39992. Section 8 introduces the problematic notation for identity of conceptual content which must be separated into cases for biimplication (𝜑 ↔ 𝜓) or class equality 𝐴 = 𝐵 in this adaptation. Section 10 introduces "truth functions" for one or two variables in equally troubling notation, as the arguments may be understood to be logical predicates or collections. Here f(𝜑) is interpreted to mean if-(𝜑, 𝜓, 𝜒) where the content of the "function" is specified by the latter two argments or logical equivalent, while g(𝐴) is read as 𝐴 ∈ 𝐺 and h(𝐴, 𝐵) as 𝐴𝐻𝐵. This necessarily introduces a need for set theory as both 𝐴 ∈ 𝐺 and 𝐴𝐻𝐵 cannot hold unless 𝐴 is a set. (Also 𝐵.) Section 11 introduces notation for generality, but there is no standard notation for generality when the variable is a proposition because it was realized after Frege that the universe of all possible propositions includes paradoxical constructions leading to the failure of naive set theory. So adopting f(𝜑) as if-(𝜑, 𝜓, 𝜒) would result in the translation of ∀𝜑 f (𝜑) as (𝜓 ∧ 𝜒). For collections, we must generalize over set variables or run into the same problems; this leads to ∀𝐴 g(𝐴) being translated as ∀𝑎𝑎 ∈ 𝐺 and so forth. Under this interpreation the text of section 11 gives us sp 2172 (or simpl 483 and simpr 485 and anifp 1062 in the propositional case) and statements similar to cbvalivw 2005, ax-gen 1787, alrimiv 1919, and alrimdv 1921. These last four introduce a generality and have no useful definition in terms of propositional variables. Section 12 introduces some combinations of primitive symbols and their human language counterparts. Using class notation, these can also be expressed without dummy variables. All are A, ∀𝑥𝑥 ∈ 𝐴, ¬ ∃𝑥¬ 𝑥 ∈ 𝐴 alex 1817, 𝐴 = V eqv 3503; Some are not B, ¬ ∀𝑥𝑥 ∈ 𝐵, ∃𝑥¬ 𝑥 ∈ 𝐵 exnal 1818, 𝐵 ⊊ V pssv 4396, 𝐵 ≠ V nev 39995; There are no C, ∀𝑥¬ 𝑥 ∈ 𝐶, ¬ ∃𝑥𝑥 ∈ 𝐶 alnex 1773, 𝐶 = ∅ eq0 4307; There exist D, ¬ ∀𝑥¬ 𝑥 ∈ 𝐷, ∃𝑥𝑥 ∈ 𝐷 df-ex 1772, ∅ ⊊ 𝐷 0pss 4394, 𝐷 ≠ ∅ n0 4309. Notation for relations between expressions also can be written in various ways. All E are P, ∀𝑥(𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑃), ¬ ∃𝑥(𝑥 ∈ 𝐸 ∧ ¬ 𝑥 ∈ 𝑃) dfss6 3956, 𝐸 = (𝐸 ∩ 𝑃) df-ss 3951, 𝐸 ⊆ 𝑃 dfss2 3954; No F are P, ∀𝑥(𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑃), ¬ ∃𝑥(𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝑃) alinexa 1834, (𝐹 ∩ 𝑃) = ∅ disj1 4399; Some G are not P, ¬ ∀𝑥(𝑥 ∈ 𝐺 → 𝑥 ∈ 𝑃), ∃𝑥(𝑥 ∈ 𝐺 ∧ ¬ 𝑥 ∈ 𝑃) exanali 1850, (𝐺 ∩ 𝑃) ⊊ 𝐺 nssinpss 4232, ¬ 𝐺 ⊆ 𝑃 nss 4028; Some H are P, ¬ ∀𝑥(𝑥 ∈ 𝐻 → ¬ 𝑥 ∈ 𝑃), ∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑥 ∈ 𝑃) exnalimn 1835, ∅ ⊊ (𝐻 ∩ 𝑃) 0pssin 39996, (𝐻 ∩ 𝑃) ≠ ∅ ndisj 4326. | ||
Theorem | dfxor4 39991 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ ((¬ 𝜑 → 𝜓) → ¬ (𝜑 → ¬ 𝜓))) | ||
Theorem | dfxor5 39992 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓))) | ||
Theorem | df3or2 39993 | Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 → (¬ 𝜓 → 𝜒))) | ||
Theorem | df3an2 39994 | Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (𝜑 → (𝜓 → ¬ 𝜒))) | ||
Theorem | nev 39995* | Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ≠ V ↔ ¬ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | 0pssin 39996* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
⊢ (∅ ⊊ (𝐴 ∩ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
The statement 𝑅 hereditary 𝐴 means relation 𝑅 is hereditary (in the sense of Frege) in the class 𝐴 or (𝑅 “ 𝐴) ⊆ 𝐴. The former is only a slight reduction in the number of symbols, but this reduces the number of floating hypotheses needed to be checked. As Frege was not using the language of classes or sets, this naturally differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on. | ||
Theorem | rp-imass 39997 | If the 𝑅-image of a class 𝐴 is a subclass of 𝐵, then the restriction of 𝑅 to 𝐴 is a subset of the Cartesian product of 𝐴 and 𝐵. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐵 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐵)) | ||
Syntax | whe 39998 | The property of relation 𝑅 being hereditary in class 𝐴. |
wff 𝑅 hereditary 𝐴 | ||
Definition | df-he 39999 | The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | dfhe2 40000 | The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |