![]() |
Metamath
Proof Explorer Theorem List (p. 359 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrninxp2 35801* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {〈𝑢, 𝑥〉 ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))} | ||
Theorem | xrninxpex 35802 | Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) ∈ V) | ||
Theorem | inxpxrn 35803 | Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) | ||
Theorem | br1cnvxrn2 35804* | The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | elec1cnvxrn2 35805* | Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | rnxrn 35806* | Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.) |
⊢ ran (𝑅 ⋉ 𝑆) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrnres 35807* | Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.) |
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrncnvepres 35808* | 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 35809* | Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.) |
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)} | ||
Theorem | xrnres 35810 | Two ways to express restriction of range Cartesian product, see also xrnres2 35811, xrnres3 35812. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆) | ||
Theorem | xrnres2 35811 | Two ways to express restriction of range Cartesian product, see also xrnres 35810, xrnres3 35812. (Contributed by Peter Mazsa, 6-Sep-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres3 35812 | Two ways to express restriction of range Cartesian product, see also xrnres 35810, xrnres2 35811. (Contributed by Peter Mazsa, 28-Mar-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres4 35813 | Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴)))) | ||
Theorem | xrnresex 35814 | 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 35815 | 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 35816 | 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 35817 | 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 35818 | 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 35819* |
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 35821 and the comment of dfec2 8275). 𝑅 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 ). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 35822) or to the range of a range Cartesian product of classes (cf. dfcoss4 35823), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 35821. Technically, we can define it via composition (dfcoss3 35822) or as the range of a range Cartesian product (dfcoss4 35823), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 36074, df-funALTV 36075) and disjoints (dfdisjs 36101, dfdisjs2 36102, df-disjALTV 36098, dfdisjALTV2 36107) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Definition | df-coels 35820 | Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 35835. Possible definitions are the special cases of dfcoss3 35822 and dfcoss4 35823. (Contributed by Peter Mazsa, 20-Nov-2019.) |
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) | ||
Theorem | dfcoss2 35821* | 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 8275). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.) |
⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)} | ||
Theorem | dfcoss3 35822 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 35819). (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅) | ||
Theorem | dfcoss4 35823 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 35819). (Contributed by Peter Mazsa, 12-Jul-2021.) |
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅) | ||
Theorem | cossex 35824 | If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V) | ||
Theorem | cosscnvex 35825 | 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 35826 | Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V) | ||
Theorem | 1cossxrncnvepresex 35827 | 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 35828 | Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ Rel ≀ 𝑅 | ||
Theorem | relcoels 35829 | Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ Rel ∼ 𝐴 | ||
Theorem | cossss 35830 | Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵) | ||
Theorem | cosseq 35831 | Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | cosseqi 35832 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ≀ 𝐴 = ≀ 𝐵 | ||
Theorem | cosseqd 35833 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | 1cossres 35834* | The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ≀ (𝑅 ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Theorem | dfcoels 35835* | Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ∼ 𝐴 = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} | ||
Theorem | brcoss 35836* | 𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
Theorem | brcoss2 35837* | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅))) | ||
Theorem | brcoss3 35838 | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅)) | ||
Theorem | brcosscnvcoss 35839 | 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 35840* | 𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢))) | ||
Theorem | cocossss 35841* | Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧)) | ||
Theorem | cnvcosseq 35842 | The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ◡ ≀ 𝑅 = ≀ 𝑅 | ||
Theorem | br2coss 35843 | Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅)) | ||
Theorem | br1cossres 35844* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶))) | ||
Theorem | br1cossres2 35845* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅))) | ||
Theorem | relbrcoss 35846* | 𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅)))) | ||
Theorem | br1cossinres 35847* | 𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossxrnres 35848* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷)))) | ||
Theorem | br1cossinidres 35849* | 𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossincnvepres 35850* | 𝐵 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 35851* | 〈𝐵, 𝐶〉 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 35852* | 〈𝐵, 𝐶〉 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 35853 | The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ dom ≀ 𝑅 = dom ◡𝑅 | ||
Theorem | dmcoss2 35854 | The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ dom ≀ 𝑅 = ran 𝑅 | ||
Theorem | rncossdmcoss 35855 | The range of cosets is the domain of them (this should be rncoss 5808 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.) |
⊢ ran ≀ 𝑅 = dom ≀ 𝑅 | ||
Theorem | dm1cosscnvepres 35856 | 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 35857 | 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 35858* | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | eldmcoss2 35859 | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴)) | ||
Theorem | eldm1cossres 35860* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵)) | ||
Theorem | eldm1cossres2 35861* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅)) | ||
Theorem | refrelcosslem 35862 | Lemma for the left side of the refrelcoss3 35863 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.) |
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥 | ||
Theorem | refrelcoss3 35863* | The class of cosets by 𝑅 is reflexive, see dfrefrel3 35916. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅) | ||
Theorem | refrelcoss2 35864 | The class of cosets by 𝑅 is reflexive, see dfrefrel2 35915. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss3 35865 | The class of cosets by 𝑅 is symmetric, see dfsymrel3 35946. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss2 35866 | The class of cosets by 𝑅 is symmetric, see dfsymrel2 35945. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | cossssid 35867 | 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 35868* | 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 35869* | 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 35870* | 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 35871* | 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 35872* | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
Theorem | brcosscnv2 35873 | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅)) | ||
Theorem | br1cosscnvxrn 35874 | 𝐴 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 35875 | Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵) | ||
Theorem | cosscnvssid3 35876* | 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 35877* | 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 35878* | 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 35879 | Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.) |
⊢ ≀ ∅ = ∅ | ||
Theorem | cossid 35880 | Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.) |
⊢ ≀ I = I | ||
Theorem | cosscnvid 35881 | Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ≀ ◡ I = I | ||
Theorem | trcoss 35882* | Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.) |
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eleccossin 35883 | 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 35884* | 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 35885 |
Define the relations class. Proper class relations (like I, see
reli 5662) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 35887).
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 35887. 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 35910), 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 35885 (see df-refrels 35911 and the resulting dfrefrels2 35913 and dfrefrels3 35914). 3. Finally, in order to be able to work with proper classes (like iprc 7600) as well, we define the predicate of the relation (see df-refrel 35912) so that it is true for the relevant proper classes (see refrelid 35921), and that the element of the class of the required relations (e.g. elrefrels3 35918) and this predicate are the same in case of sets (see elrefrelsrel 35919). (Contributed by Peter Mazsa, 13-Jun-2018.) |
⊢ Rels = 𝒫 (V × V) | ||
Theorem | elrels2 35886 | The element of the relations class (df-rels 35885) and the relation predicate (df-rel 5526) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V))) | ||
Theorem | elrelsrel 35887 | The element of the relations class (df-rels 35885) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅)) | ||
Theorem | elrelsrelim 35888 | The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ (𝑅 ∈ Rels → Rel 𝑅) | ||
Theorem | elrels5 35889 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅)) | ||
Theorem | elrels6 35890 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)) | ||
Theorem | elrelscnveq3 35891* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq 35892 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | elrelscnveq2 35893* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq4 35894* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | cnvelrels 35895 | The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels ) | ||
Theorem | cosselrels 35896 | Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels ) | ||
Theorem | cosscnvelrels 35897 | Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels ) | ||
Definition | df-ssr 35898* |
Define the subsets class or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5430) and identity relation
(df-id 5425) classes. Subset relation class and Scott
Fenton's subset
class df-sset 33430 are the same: S = SSet (compare dfssr2 35899 with
df-sset 33430), the only reason we do not use dfssr2 35899 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 3898) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 35901. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3898. The only exception (aside from directly investigating the class S e.g. in relssr 35900 or in extssr 35909) is when we have a specific purpose with its usage, like in case of df-refs 35910 versus df-cnvrefs 35923, 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 35728, extep 35700 and extssr 35909, 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 35899 | Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E ))) | ||
Theorem | relssr 35900 | The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ Rel S |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |