| Metamath
Proof Explorer Theorem List (p. 385 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rnxrncnvepres 38401* | Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021.) |
| ⊢ ran (𝑅 ⋉ (◡ E ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 𝑢 ∧ 𝑢𝑅𝑥)} | ||
| Theorem | rnxrnidres 38402* | Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.) |
| ⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)} | ||
| Theorem | xrnres 38403 | Two ways to express restriction of range Cartesian product, see also xrnres2 38404, xrnres3 38405. (Contributed by Peter Mazsa, 5-Jun-2021.) |
| ⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆) | ||
| Theorem | xrnres2 38404 | Two ways to express restriction of range Cartesian product, see also xrnres 38403, xrnres3 38405. (Contributed by Peter Mazsa, 6-Sep-2021.) |
| ⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴)) | ||
| Theorem | xrnres3 38405 | Two ways to express restriction of range Cartesian product, see also xrnres 38403, xrnres2 38404. (Contributed by Peter Mazsa, 28-Mar-2020.) |
| ⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴)) | ||
| Theorem | xrnres4 38406 | Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.) |
| ⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴)))) | ||
| Theorem | xrnresex 38407 | Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 7-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ (𝑆 ↾ 𝐴) ∈ 𝑋) → (𝑅 ⋉ (𝑆 ↾ 𝐴)) ∈ V) | ||
| Theorem | xrnidresex 38408 | Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ ( I ↾ 𝐴)) ∈ V) | ||
| Theorem | xrncnvepresex 38409 | Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) | ||
| Theorem | brin2 38410 | Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆)〈𝐵, 𝐵〉)) | ||
| Theorem | brin3 38411 | Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) (Avoid depending on this detail.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}})) | ||
| Definition | df-coss 38412* |
Define the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by
𝑅 iff there exists a set 𝑢 such
that both 𝑢𝑅𝑥 and
𝑢𝑅𝑦 hold, i.e., both 𝑥 and
𝑦
are are elements of the 𝑅
-coset of 𝑢 (see dfcoss2 38414 and the comment of dfec2 8748). 𝑅 is
usually a relation.
This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to 𝑅, the right side relate to ≀ 𝑅 (see e.g. pet 38852). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38415) or to the range of a range Cartesian product of classes (cf. dfcoss4 38416), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38414. Technically, we can define it via composition (dfcoss3 38415) or as the range of a range Cartesian product (dfcoss4 38416), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 38682, df-funALTV 38683) and disjoints (dfdisjs 38709, dfdisjs2 38710, df-disjALTV 38706, dfdisjALTV2 38715) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.) |
| ⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
| Definition | df-coels 38413 | Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38431. Possible definitions are the special cases of dfcoss3 38415 and dfcoss4 38416. (Contributed by Peter Mazsa, 20-Nov-2019.) |
| ⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) | ||
| Theorem | dfcoss2 38414* | Alternate definition of the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑥 and 𝑦 are are elements of the 𝑅-coset of 𝑢 (see also the comment of dfec2 8748). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.) |
| ⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)} | ||
| Theorem | dfcoss3 38415 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38412). (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅) | ||
| Theorem | dfcoss4 38416 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38412). (Contributed by Peter Mazsa, 12-Jul-2021.) |
| ⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅) | ||
| Theorem | cosscnv 38417* | Class of cosets by the converse of 𝑅 (Contributed by Peter Mazsa, 17-Jun-2020.) |
| ⊢ ≀ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)} | ||
| Theorem | coss1cnvres 38418* | Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.) |
| ⊢ ≀ ◡(𝑅 ↾ 𝐴) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))} | ||
| Theorem | coss2cnvepres 38419* | Special case of coss1cnvres 38418. (Contributed by Peter Mazsa, 8-Jun-2020.) |
| ⊢ ≀ ◡(◡ E ↾ 𝐴) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))} | ||
| Theorem | cossex 38420 | If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V) | ||
| Theorem | cosscnvex 38421 | If 𝐴 is a set then the class of cosets by the converse of 𝐴 is a set. (Contributed by Peter Mazsa, 18-Oct-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ V) | ||
| Theorem | 1cosscnvepresex 38422 | Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V) | ||
| Theorem | 1cossxrncnvepresex 38423 | Sufficient condition for a restricted converse epsilon range Cartesian product to be a set. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) | ||
| Theorem | relcoss 38424 | Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ Rel ≀ 𝑅 | ||
| Theorem | relcoels 38425 | Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.) |
| ⊢ Rel ∼ 𝐴 | ||
| Theorem | cossss 38426 | Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.) |
| ⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵) | ||
| Theorem | cosseq 38427 | Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.) |
| ⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵) | ||
| Theorem | cosseqi 38428 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ≀ 𝐴 = ≀ 𝐵 | ||
| Theorem | cosseqd 38429 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵) | ||
| Theorem | 1cossres 38430* | The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.) |
| ⊢ ≀ (𝑅 ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
| Theorem | dfcoels 38431* | Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.) |
| ⊢ ∼ 𝐴 = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} | ||
| Theorem | brcoss 38432* | 𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
| Theorem | brcoss2 38433* | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅))) | ||
| Theorem | brcoss3 38434 | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅)) | ||
| Theorem | brcosscnvcoss 38435 | For sets, the 𝐴 and 𝐵 cosets by 𝑅 binary relation and the 𝐵 and 𝐴 cosets by 𝑅 binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ 𝐵 ≀ 𝑅𝐴)) | ||
| Theorem | brcoels 38436* | 𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢))) | ||
| Theorem | cocossss 38437* | Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.) |
| ⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧)) | ||
| Theorem | cnvcosseq 38438 | The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.) |
| ⊢ ◡ ≀ 𝑅 = ≀ 𝑅 | ||
| Theorem | br2coss 38439 | Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅)) | ||
| Theorem | br1cossres 38440* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶))) | ||
| Theorem | br1cossres2 38441* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅))) | ||
| Theorem | brressn 38442 | Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(𝑅 ↾ {𝐴})𝐶 ↔ (𝐵 = 𝐴 ∧ 𝐵𝑅𝐶))) | ||
| Theorem | ressn2 38443* | A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024.) |
| ⊢ (𝑅 ↾ {𝐴}) = {〈𝑎, 𝑢〉 ∣ (𝑎 = 𝐴 ∧ 𝐴𝑅𝑢)} | ||
| Theorem | refressn 38444* | Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38443) is reflexive, see also refrelressn 38525. (Contributed by Peter Mazsa, 12-Jun-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ (dom (𝑅 ↾ {𝐴}) ∩ ran (𝑅 ↾ {𝐴}))𝑥(𝑅 ↾ {𝐴})𝑥) | ||
| Theorem | antisymressn 38445 | Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38443) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024.) |
| ⊢ ∀𝑥∀𝑦((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑥) → 𝑥 = 𝑦) | ||
| Theorem | trressn 38446 | Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38443) is transitive, see also trrelressn 38584. (Contributed by Peter Mazsa, 16-Jun-2024.) |
| ⊢ ∀𝑥∀𝑦∀𝑧((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑧) → 𝑥(𝑅 ↾ {𝐴})𝑧) | ||
| Theorem | relbrcoss 38447* | 𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅)))) | ||
| Theorem | br1cossinres 38448* | 𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶)))) | ||
| Theorem | br1cossxrnres 38449* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.) |
| ⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷)))) | ||
| Theorem | br1cossinidres 38450* | 𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶)))) | ||
| Theorem | br1cossincnvepres 38451* | 𝐵 and 𝐶 are cosets by an intersection with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (◡ E ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝐵 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐶)))) | ||
| Theorem | br1cossxrnidres 38452* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by a range Cartesian product with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.) |
| ⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ ( I ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐸 ∧ 𝑢𝑅𝐷)))) | ||
| Theorem | br1cossxrncnvepres 38453* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by a range Cartesian product with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 12-May-2021.) |
| ⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐸 ∈ 𝑢 ∧ 𝑢𝑅𝐷)))) | ||
| Theorem | dmcoss3 38454 | The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.) |
| ⊢ dom ≀ 𝑅 = dom ◡𝑅 | ||
| Theorem | dmcoss2 38455 | The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ dom ≀ 𝑅 = ran 𝑅 | ||
| Theorem | rncossdmcoss 38456 | The range of cosets is the domain of them (this should be rncoss 5986 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.) |
| ⊢ ran ≀ 𝑅 = dom ≀ 𝑅 | ||
| Theorem | dm1cosscnvepres 38457 | The domain of cosets of the restricted converse epsilon relation is the union of the restriction. (Contributed by Peter Mazsa, 18-May-2019.) (Revised by Peter Mazsa, 26-Sep-2021.) |
| ⊢ dom ≀ (◡ E ↾ 𝐴) = ∪ 𝐴 | ||
| Theorem | dmcoels 38458 | The domain of coelements in 𝐴 is the union of 𝐴. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Peter Mazsa, 5-Apr-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
| ⊢ dom ∼ 𝐴 = ∪ 𝐴 | ||
| Theorem | eldmcoss 38459* | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
| Theorem | eldmcoss2 38460 | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴)) | ||
| Theorem | eldm1cossres 38461* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵)) | ||
| Theorem | eldm1cossres2 38462* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅)) | ||
| Theorem | refrelcosslem 38463 | Lemma for the left side of the refrelcoss3 38464 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.) |
| ⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥 | ||
| Theorem | refrelcoss3 38464* | The class of cosets by 𝑅 is reflexive, see dfrefrel3 38517. (Contributed by Peter Mazsa, 30-Jul-2019.) |
| ⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅) | ||
| Theorem | refrelcoss2 38465 | The class of cosets by 𝑅 is reflexive, see dfrefrel2 38516. (Contributed by Peter Mazsa, 30-Jul-2019.) |
| ⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
| Theorem | symrelcoss3 38466 | The class of cosets by 𝑅 is symmetric, see dfsymrel3 38551. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
| ⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅) | ||
| Theorem | symrelcoss2 38467 | The class of cosets by 𝑅 is symmetric, see dfsymrel2 38550. (Contributed by Peter Mazsa, 27-Dec-2018.) |
| ⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
| Theorem | cossssid 38468 | Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 27-Jul-2021.) |
| ⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅))) | ||
| Theorem | cossssid2 38469* | Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.) |
| ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥∀𝑦(∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦)) | ||
| Theorem | cossssid3 38470* | Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.) |
| ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∀𝑥∀𝑦((𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦)) | ||
| Theorem | cossssid4 38471* | Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∃*𝑥 𝑢𝑅𝑥) | ||
| Theorem | cossssid5 38472* | Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥 ∈ ran 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 ∨ ([𝑥]◡𝑅 ∩ [𝑦]◡𝑅) = ∅)) | ||
| Theorem | brcosscnv 38473* | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
| Theorem | brcosscnv2 38474 | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅)) | ||
| Theorem | br1cosscnvxrn 38475 | 𝐴 and 𝐵 are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡(𝑅 ⋉ 𝑆)𝐵 ↔ (𝐴 ≀ ◡𝑅𝐵 ∧ 𝐴 ≀ ◡𝑆𝐵))) | ||
| Theorem | 1cosscnvxrn 38476 | Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
| ⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵) | ||
| Theorem | cosscnvssid3 38477* | Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021.) |
| ⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣)) | ||
| Theorem | cosscnvssid4 38478* | Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥) | ||
| Theorem | cosscnvssid5 38479* | Equivalent expressions for the class of cosets by the converse of the relation 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅) ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
| Theorem | coss0 38480 | Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.) |
| ⊢ ≀ ∅ = ∅ | ||
| Theorem | cossid 38481 | Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.) |
| ⊢ ≀ I = I | ||
| Theorem | cosscnvid 38482 | Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.) |
| ⊢ ≀ ◡ I = I | ||
| Theorem | trcoss 38483* | Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.) |
| ⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
| Theorem | eleccossin 38484 | Two ways of saying that the coset of 𝐴 and the coset of 𝐶 have the common element 𝐵. (Contributed by Peter Mazsa, 15-Oct-2021.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∈ ([𝐴] ≀ 𝑅 ∩ [𝐶] ≀ 𝑅) ↔ (𝐴 ≀ 𝑅𝐵 ∧ 𝐵 ≀ 𝑅𝐶))) | ||
| Theorem | trcoss2 38485* | Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.) |
| ⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
| Definition | df-rels 38486 |
Define the relations class. Proper class relations (like I, see
reli 5836) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 38488).
The class of relations is a great tool we can use when we define classes of different relations as nullary class constants as required by the 2. point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 38488. When we want to define a specific class of relations as a nullary class constant, the appropriate method is the following: 1. We define the specific nullary class constant for general sets (see e.g. df-refs 38511), then 2. we get the required class of relations by the intersection of the class of general sets above with the class of relations df-rels 38486 (see df-refrels 38512 and the resulting dfrefrels2 38514 and dfrefrels3 38515). 3. Finally, in order to be able to work with proper classes (like iprc 7933) as well, we define the predicate of the relation (see df-refrel 38513) so that it is true for the relevant proper classes (see refrelid 38523), and that the element of the class of the required relations (e.g. elrefrels3 38520) and this predicate are the same in case of sets (see elrefrelsrel 38521). (Contributed by Peter Mazsa, 13-Jun-2018.) |
| ⊢ Rels = 𝒫 (V × V) | ||
| Theorem | elrels2 38487 | The element of the relations class (df-rels 38486) and the relation predicate (df-rel 5692) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V))) | ||
| Theorem | elrelsrel 38488 | The element of the relations class (df-rels 38486) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅)) | ||
| Theorem | elrelsrelim 38489 | The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.) |
| ⊢ (𝑅 ∈ Rels → Rel 𝑅) | ||
| Theorem | elrels5 38490 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅)) | ||
| Theorem | elrels6 38491 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)) | ||
| Theorem | elrelscnveq3 38492* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
| Theorem | elrelscnveq 38493 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
| Theorem | elrelscnveq2 38494* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
| Theorem | elrelscnveq4 38495* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
| Theorem | cnvelrels 38496 | The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels ) | ||
| Theorem | cosselrels 38497 | Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels ) | ||
| Theorem | cosscnvelrels 38498 | Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels ) | ||
| Definition | df-ssr 38499* |
Define the subsets class or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5584) and identity relation
(df-id 5578) classes. Subset relation class and Scott
Fenton's subset
class df-sset 35857 are the same: S = SSet (compare dfssr2 38500 with
df-sset 35857), the only reason we do not use dfssr2 38500 as the base
definition of the subsets class is the way we defined the epsilon
relation and the identity relation classes.
The binary relation on the class of subsets and the subclass relationship (df-ss 3968) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 38502. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3968. The only exception (aside from directly investigating the class S e.g. in relssr 38501 or in extssr 38510) is when we have a specific purpose with its usage, like in case of df-refs 38511 versus df-cnvrefs 38526, where we need S to define the class of reflexive sets in order to be able to define the class of converse reflexive sets with the help of the converse of S. The subsets class S has another place in set.mm as well: if we define extensional relation based on the common property in extid 38311, extep 38284 and extssr 38510, then "extrelssr" " |- ExtRel S " is a theorem along with "extrelep" " |- ExtRel E " and "extrelid" " |- ExtRel I " . (Contributed by Peter Mazsa, 25-Jul-2019.) |
| ⊢ S = {〈𝑥, 𝑦〉 ∣ 𝑥 ⊆ 𝑦} | ||
| Theorem | dfssr2 38500 | Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.) |
| ⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E ))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |