![]() |
Metamath
Proof Explorer Theorem List (p. 373 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rnresequniqs 37201 | The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.) |
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅)) | ||
Theorem | n0el2 37202 | Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 31-Jan-2018.) |
⊢ (¬ ∅ ∈ 𝐴 ↔ dom (◡ E ↾ 𝐴) = 𝐴) | ||
Theorem | cnvepresex 37203 | Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V) | ||
Theorem | eccnvepex 37204 | The converse epsilon coset exists. (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ [𝐴]◡ E ∈ V | ||
Theorem | cnvepimaex 37205 | The image of converse epsilon exists, proof via imaexALTV 37199 (see also cnvepima 37206 and uniexg 7730 for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) ∈ V) | ||
Theorem | cnvepima 37206 | The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴) | ||
Theorem | inex3 37207 | Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | inxpex 37208 | Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.) |
⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V) | ||
Theorem | eqres 37209 | Converting a class constant definition by restriction (like df-ers 37533 or df-parts 37635) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.) |
⊢ 𝑅 = (𝑆 ↾ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵))) | ||
Theorem | brrabga 37210* | The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩𝑅𝐶 ↔ 𝜓)) | ||
Theorem | brcnvrabga 37211* | The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅⟨𝐵, 𝐶⟩ ↔ 𝜓)) | ||
Theorem | opideq 37212 | Equality conditions for ordered pairs ⟨𝐴, 𝐴⟩ and ⟨𝐵, 𝐵⟩. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.) |
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐴⟩ = ⟨𝐵, 𝐵⟩ ↔ 𝐴 = 𝐵)) | ||
Theorem | iss2 37213 | A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) | ||
Theorem | eldmcnv 37214* | Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | dfrel5 37215 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅) | ||
Theorem | dfrel6 37216 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.) |
⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅) | ||
Theorem | cnvresrn 37217 | Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.) |
⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅 | ||
Theorem | relssinxpdmrn 37218 | Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023.) |
⊢ (Rel 𝑅 → (𝑅 ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆)) | ||
Theorem | cnvref4 37219 | Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023.) |
⊢ (Rel 𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆)) | ||
Theorem | cnvref5 37220* | Two ways to say that a relation is a subclass of the identity relation. (Contributed by Peter Mazsa, 26-Jun-2019.) |
⊢ (Rel 𝑅 → (𝑅 ⊆ I ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦))) | ||
Theorem | ecin0 37221* | Two ways of saying that the coset of 𝐴 and the coset of 𝐵 have no elements in common. (Contributed by Peter Mazsa, 1-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∀𝑥(𝐴𝑅𝑥 → ¬ 𝐵𝑅𝑥))) | ||
Theorem | ecinn0 37222* | Two ways of saying that the coset of 𝐴 and the coset of 𝐵 have some elements in common. (Contributed by Peter Mazsa, 23-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅ ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
Theorem | ineleq 37223* | Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦)) | ||
Theorem | inecmo 37224* | Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Rel 𝑅 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ ([𝐵]𝑅 ∩ [𝐶]𝑅) = ∅) ↔ ∀𝑧∃*𝑥 ∈ 𝐴 𝐵𝑅𝑧)) | ||
Theorem | inecmo2 37225* | Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018.) (Revised by Peter Mazsa, 2-Sep-2021.) |
⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 ∈ 𝐴 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | ineccnvmo 37226* | Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 2-Sep-2021.) |
⊢ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 = 𝑧 ∨ ([𝑦]◡𝐹 ∩ [𝑧]◡𝐹) = ∅) ↔ ∀𝑥∃*𝑦 ∈ 𝐵 𝑥𝐹𝑦) | ||
Theorem | alrmomorn 37227 | Equivalence of an "at most one" and an "at most one" restricted to the range inside a universal quantification. (Contributed by Peter Mazsa, 3-Sep-2021.) |
⊢ (∀𝑥∃*𝑦 ∈ ran 𝑅 𝑥𝑅𝑦 ↔ ∀𝑥∃*𝑦 𝑥𝑅𝑦) | ||
Theorem | alrmomodm 37228* | Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (Rel 𝑅 → (∀𝑥∃*𝑢 ∈ dom 𝑅 𝑢𝑅𝑥 ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥)) | ||
Theorem | ineccnvmo2 37229* | Equivalence of a double universal quantification restricted to the range and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 4-Sep-2021.) |
⊢ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ↔ ∀𝑢∃*𝑥 𝑢𝐹𝑥) | ||
Theorem | inecmo3 37230* | Equivalence of a double universal quantification restricted to the domain and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ((∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | moeu2 37231 | Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024.) |
⊢ (∃*𝑥𝜑 ↔ (¬ ∃𝑥𝜑 ∨ ∃!𝑥𝜑)) | ||
Theorem | mopickr 37232 | "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 (pm2.21 123) and *14.26 (eupickbi 2633) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.) |
⊢ ((∃*𝑥𝜓 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜓 → 𝜑)) | ||
Theorem | moantr 37233 | Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.) |
⊢ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒))) | ||
Theorem | brabidgaw 37234* | The law of concretion for a binary relation. Special case of brabga 5535. Version of brabidga 37235 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Peter Mazsa, 24-Nov-2018.) (Revised by Gino Giotto, 2-Apr-2024.) |
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ (𝑥𝑅𝑦 ↔ 𝜑) | ||
Theorem | brabidga 37235 | The law of concretion for a binary relation. Special case of brabga 5535. Usage of this theorem is discouraged because it depends on ax-13 2372, see brabidgaw 37234 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.) |
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ (𝑥𝑅𝑦 ↔ 𝜑) | ||
Theorem | inxp2 37236* | Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.) |
⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)} | ||
Theorem | opabf 37237 | A class abstraction of a collection of ordered pairs with a negated wff is the empty set. (Contributed by Peter Mazsa, 21-Oct-2019.) (Proof shortened by Thierry Arnoux, 18-Feb-2022.) |
⊢ ¬ 𝜑 ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = ∅ | ||
Theorem | ec0 37238 | The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.) |
⊢ [𝐴]∅ = ∅ | ||
Theorem | 0qs 37239 | Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019.) |
⊢ (∅ / 𝑅) = ∅ | ||
Theorem | brcnvin 37240 | Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴))) | ||
Definition | df-xrn 37241 | Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 37242 and brxrn 37244. This is Scott Fenton's df-txp 34826 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 34826. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵)) | ||
Theorem | xrnss3v 37242 | A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 34850 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 34850. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V)) | ||
Theorem | xrnrel 37243 | A range Cartesian product is a relation. This is Scott Fenton's txprel 34851 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 34851. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Rel (𝐴 ⋉ 𝐵) | ||
Theorem | brxrn 37244 | Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 37242, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) | ||
Theorem | brxrn2 37245* | A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))) | ||
Theorem | dfxrn2 37246* | Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.) |
⊢ (𝑅 ⋉ 𝑆) = ◡{⟨⟨𝑥, 𝑦⟩, 𝑢⟩ ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | xrneq1 37247 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)) | ||
Theorem | xrneq1i 37248 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶) | ||
Theorem | xrneq1d 37249 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)) | ||
Theorem | xrneq2 37250 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
Theorem | xrneq2i 37251 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵) | ||
Theorem | xrneq2d 37252 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
Theorem | xrneq12 37253 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
Theorem | xrneq12i 37254 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷) | ||
Theorem | xrneq12d 37255 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
Theorem | elecxrn 37256* | Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))) | ||
Theorem | ecxrn 37257* | The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)}) | ||
Theorem | disjressuc2 37258* | Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))) | ||
Theorem | disjecxrn 37259 | Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅))) | ||
Theorem | disjecxrncnvep 37260 | Two ways of saying that cosets are disjoint, special case of disjecxrn 37259. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))) | ||
Theorem | disjsuc2 37261* | 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 37262* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))} | ||
Theorem | xrninxp2 37263* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))} | ||
Theorem | xrninxpex 37264 | 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 37265 | Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) | ||
Theorem | br1cnvxrn2 37266* | The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | elec1cnvxrn2 37267* | Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
Theorem | rnxrn 37268* | Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.) |
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrnres 37269* | Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.) |
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
Theorem | rnxrncnvepres 37270* | 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 37271* | Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.) |
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)} | ||
Theorem | xrnres 37272 | Two ways to express restriction of range Cartesian product, see also xrnres2 37273, xrnres3 37274. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆) | ||
Theorem | xrnres2 37273 | Two ways to express restriction of range Cartesian product, see also xrnres 37272, xrnres3 37274. (Contributed by Peter Mazsa, 6-Sep-2021.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres3 37274 | Two ways to express restriction of range Cartesian product, see also xrnres 37272, xrnres2 37273. (Contributed by Peter Mazsa, 28-Mar-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴)) | ||
Theorem | xrnres4 37275 | Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.) |
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴)))) | ||
Theorem | xrnresex 37276 | 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 37277 | 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 37278 | 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 37279 | 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 37280 | 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 37281* |
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 37283 and the comment of dfec2 8706). 𝑅 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 37721). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 37284) or to the range of a range Cartesian product of classes (cf. dfcoss4 37285), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 37283. Technically, we can define it via composition (dfcoss3 37284) or as the range of a range Cartesian product (dfcoss4 37285), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 37551, df-funALTV 37552) and disjoints (dfdisjs 37578, dfdisjs2 37579, df-disjALTV 37575, dfdisjALTV2 37584) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Definition | df-coels 37282 | Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 37300. Possible definitions are the special cases of dfcoss3 37284 and dfcoss4 37285. (Contributed by Peter Mazsa, 20-Nov-2019.) |
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) | ||
Theorem | dfcoss2 37283* | 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 8706). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.) |
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)} | ||
Theorem | dfcoss3 37284 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 37281). (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅) | ||
Theorem | dfcoss4 37285 | Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 37281). (Contributed by Peter Mazsa, 12-Jul-2021.) |
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅) | ||
Theorem | cosscnv 37286* | Class of cosets by the converse of 𝑅 (Contributed by Peter Mazsa, 17-Jun-2020.) |
⊢ ≀ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)} | ||
Theorem | coss1cnvres 37287* | Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.) |
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))} | ||
Theorem | coss2cnvepres 37288* | Special case of coss1cnvres 37287. (Contributed by Peter Mazsa, 8-Jun-2020.) |
⊢ ≀ ◡(◡ E ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))} | ||
Theorem | cossex 37289 | If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V) | ||
Theorem | cosscnvex 37290 | 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 37291 | Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V) | ||
Theorem | 1cossxrncnvepresex 37292 | 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 37293 | Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ Rel ≀ 𝑅 | ||
Theorem | relcoels 37294 | Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ Rel ∼ 𝐴 | ||
Theorem | cossss 37295 | Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵) | ||
Theorem | cosseq 37296 | Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | cosseqi 37297 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ≀ 𝐴 = ≀ 𝐵 | ||
Theorem | cosseqd 37298 | Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵) | ||
Theorem | 1cossres 37299* | The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ≀ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)} | ||
Theorem | dfcoels 37300* | Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.) |
⊢ ∼ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |