![]() |
Metamath
Proof Explorer Theorem List (p. 381 of 485) | < 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-30820) |
![]() (30821-32343) |
![]() (32344-48429) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrneq1d 38001 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)) | ||
Theorem | xrneq2 38002 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
Theorem | xrneq2i 38003 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵) | ||
Theorem | xrneq2d 38004 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
Theorem | xrneq12 38005 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
Theorem | xrneq12i 38006 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷) | ||
Theorem | xrneq12d 38007 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
Theorem | elecxrn 38008* | Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = 〈𝑥, 𝑦〉 ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))) | ||
Theorem | ecxrn 38009* | The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {〈𝑦, 𝑧〉 ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)}) | ||
Theorem | disjressuc2 38010* | Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))) | ||
Theorem | disjecxrn 38011 | Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅))) | ||
Theorem | disjecxrncnvep 38012 | Two ways of saying that cosets are disjoint, special case of disjecxrn 38011. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))) | ||
Theorem | disjsuc2 38013* | Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))) | ||
Theorem | xrninxp 38014* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{〈〈𝑦, 𝑧〉, 𝑢〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)〈𝑦, 𝑧〉))} | ||
Theorem | xrninxp2 38015* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {〈𝑢, 𝑥〉 ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))} | ||
Theorem | xrninxpex 38016 | 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 38017 | Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) | ||
Theorem | br1cnvxrn2 38018* | The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | elec1cnvxrn2 38019* | Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | rnxrn 38020* | Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.) |
⊢ ran (𝑅 ⋉ 𝑆) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrnres 38021* | Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.) |
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrncnvepres 38022* | 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 38023* | Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.) |
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)} | ||
Theorem | xrnres 38024 | Two ways to express restriction of range Cartesian product, see also xrnres2 38025, xrnres3 38026. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆) | ||
Theorem | xrnres2 38025 | Two ways to express restriction of range Cartesian product, see also xrnres 38024, xrnres3 38026. (Contributed by Peter Mazsa, 6-Sep-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres3 38026 | Two ways to express restriction of range Cartesian product, see also xrnres 38024, xrnres2 38025. (Contributed by Peter Mazsa, 28-Mar-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres4 38027 | Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴)))) | ||
Theorem | xrnresex 38028 | 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 38029 | 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 38030 | 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 38031 | 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 38032 | 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 38033* |
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 38035 and the comment of dfec2 8728). 𝑅 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 38473). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38036) or to the range of a range Cartesian product of classes (cf. dfcoss4 38037), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38035. Technically, we can define it via composition (dfcoss3 38036) or as the range of a range Cartesian product (dfcoss4 38037), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 38303, df-funALTV 38304) and disjoints (dfdisjs 38330, dfdisjs2 38331, df-disjALTV 38327, dfdisjALTV2 38336) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Definition | df-coels 38034 | Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38052. Possible definitions are the special cases of dfcoss3 38036 and dfcoss4 38037. (Contributed by Peter Mazsa, 20-Nov-2019.) |
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) | ||
Theorem | dfcoss2 38035* | 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 8728). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.) |
⊢ ≀ 𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)} | ||
Theorem | dfcoss3 38036 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38033). (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅) | ||
Theorem | dfcoss4 38037 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38033). (Contributed by Peter Mazsa, 12-Jul-2021.) |
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅) | ||
Theorem | cosscnv 38038* | Class of cosets by the converse of 𝑅 (Contributed by Peter Mazsa, 17-Jun-2020.) |
⊢ ≀ ◡𝑅 = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)} | ||
Theorem | coss1cnvres 38039* | Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.) |
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))} | ||
Theorem | coss2cnvepres 38040* | Special case of coss1cnvres 38039. (Contributed by Peter Mazsa, 8-Jun-2020.) |
⊢ ≀ ◡(◡ E ↾ 𝐴) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))} | ||
Theorem | cossex 38041 | If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V) | ||
Theorem | cosscnvex 38042 | 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 38043 | Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V) | ||
Theorem | 1cossxrncnvepresex 38044 | 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 38045 | Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ Rel ≀ 𝑅 | ||
Theorem | relcoels 38046 | Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ Rel ∼ 𝐴 | ||
Theorem | cossss 38047 | Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵) | ||
Theorem | cosseq 38048 | Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | cosseqi 38049 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ≀ 𝐴 = ≀ 𝐵 | ||
Theorem | cosseqd 38050 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | 1cossres 38051* | The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ≀ (𝑅 ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Theorem | dfcoels 38052* | Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ∼ 𝐴 = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} | ||
Theorem | brcoss 38053* | 𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
Theorem | brcoss2 38054* | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅))) | ||
Theorem | brcoss3 38055 | Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅)) | ||
Theorem | brcosscnvcoss 38056 | 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 38057* | 𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢))) | ||
Theorem | cocossss 38058* | Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧)) | ||
Theorem | cnvcosseq 38059 | The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ◡ ≀ 𝑅 = ≀ 𝑅 | ||
Theorem | br2coss 38060 | Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅)) | ||
Theorem | br1cossres 38061* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶))) | ||
Theorem | br1cossres2 38062* | 𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅))) | ||
Theorem | brressn 38063 | Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(𝑅 ↾ {𝐴})𝐶 ↔ (𝐵 = 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | ressn2 38064* | 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 38065* | Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38064) is reflexive, see also refrelressn 38146. (Contributed by Peter Mazsa, 12-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ (dom (𝑅 ↾ {𝐴}) ∩ ran (𝑅 ↾ {𝐴}))𝑥(𝑅 ↾ {𝐴})𝑥) | ||
Theorem | antisymressn 38066 | Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38064) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024.) |
⊢ ∀𝑥∀𝑦((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑥) → 𝑥 = 𝑦) | ||
Theorem | trressn 38067 | Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38064) is transitive, see also trrelressn 38205. (Contributed by Peter Mazsa, 16-Jun-2024.) |
⊢ ∀𝑥∀𝑦∀𝑧((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑧) → 𝑥(𝑅 ↾ {𝐴})𝑧) | ||
Theorem | relbrcoss 38068* | 𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅)))) | ||
Theorem | br1cossinres 38069* | 𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossxrnres 38070* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷)))) | ||
Theorem | br1cossinidres 38071* | 𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossincnvepres 38072* | 𝐵 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 38073* | 〈𝐵, 𝐶〉 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 38074* | 〈𝐵, 𝐶〉 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 38075 | The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ dom ≀ 𝑅 = dom ◡𝑅 | ||
Theorem | dmcoss2 38076 | The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ dom ≀ 𝑅 = ran 𝑅 | ||
Theorem | rncossdmcoss 38077 | The range of cosets is the domain of them (this should be rncoss 5975 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.) |
⊢ ran ≀ 𝑅 = dom ≀ 𝑅 | ||
Theorem | dm1cosscnvepres 38078 | 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 38079 | 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 38080* | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | eldmcoss2 38081 | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴)) | ||
Theorem | eldm1cossres 38082* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵)) | ||
Theorem | eldm1cossres2 38083* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅)) | ||
Theorem | refrelcosslem 38084 | Lemma for the left side of the refrelcoss3 38085 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.) |
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥 | ||
Theorem | refrelcoss3 38085* | The class of cosets by 𝑅 is reflexive, see dfrefrel3 38138. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅) | ||
Theorem | refrelcoss2 38086 | The class of cosets by 𝑅 is reflexive, see dfrefrel2 38137. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss3 38087 | The class of cosets by 𝑅 is symmetric, see dfsymrel3 38172. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss2 38088 | The class of cosets by 𝑅 is symmetric, see dfsymrel2 38171. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | cossssid 38089 | 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 38090* | 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 38091* | 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 38092* | 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 38093* | 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 38094* | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
Theorem | brcosscnv2 38095 | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅)) | ||
Theorem | br1cosscnvxrn 38096 | 𝐴 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 38097 | Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵) | ||
Theorem | cosscnvssid3 38098* | 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 38099* | 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 38100* | 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 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |