| Metamath
Proof Explorer Theorem List (p. 384 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 | rncnv 38301 | Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.) |
| ⊢ ran ◡𝐴 = dom 𝐴 | ||
| Theorem | dfdm6 38302* | Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.) |
| ⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅} | ||
| Theorem | dfrn6 38303* | Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.) |
| ⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅} | ||
| Theorem | rncnvepres 38304 | The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
| ⊢ ran (◡ E ↾ 𝐴) = ∪ 𝐴 | ||
| Theorem | dmecd 38305 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8795). (Contributed by Peter Mazsa, 9-Oct-2018.) |
| ⊢ (𝜑 → dom 𝑅 = 𝐴) & ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | ||
| Theorem | dmec2d 38306 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8795). (Contributed by Peter Mazsa, 12-Oct-2018.) |
| ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅)) | ||
| Theorem | brid 38307 | Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.) |
| ⊢ (𝐴 I 𝐵 ↔ 𝐵 I 𝐴) | ||
| Theorem | ideq2 38308 | For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020.) (Revised by Peter Mazsa, 18-Dec-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | idresssidinxp 38309 | Condition for the identity restriction to be a subclass of identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
| ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴) ⊆ ( I ∩ (𝐴 × 𝐵))) | ||
| Theorem | idreseqidinxp 38310 | Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
| ⊢ (𝐴 ⊆ 𝐵 → ( I ∩ (𝐴 × 𝐵)) = ( I ↾ 𝐴)) | ||
| Theorem | extid 38311 | Property of identity relation, see also extep 38284, extssr 38510 and the comment of df-ssr 38499. (Contributed by Peter Mazsa, 5-Jul-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → ([𝐴]◡ I = [𝐵]◡ I ↔ 𝐴 = 𝐵)) | ||
| Theorem | inxpss 38312* | Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
| ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
| Theorem | idinxpss 38313* | Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
| ⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦)) | ||
| Theorem | ref5 38314* | Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 12-Dec-2023.) |
| ⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ 𝑅 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐵)𝑥𝑅𝑥) | ||
| Theorem | inxpss3 38315* | Two ways to say that an intersection with a Cartesian product is a subclass (see also inxpss 38312). (Contributed by Peter Mazsa, 8-Mar-2019.) |
| ⊢ (∀𝑥∀𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 → 𝑥(𝑆 ∩ (𝐴 × 𝐵))𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
| Theorem | inxpss2 38316* | Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.) |
| ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑆 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
| Theorem | inxpssidinxp 38317* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 38316. (Contributed by Peter Mazsa, 4-Jul-2019.) |
| ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ ( I ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥 = 𝑦)) | ||
| Theorem | idinxpssinxp 38318* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 38316. (Contributed by Peter Mazsa, 6-Mar-2019.) |
| ⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦)) | ||
| Theorem | idinxpssinxp2 38319* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
| Theorem | idinxpssinxp3 38320 | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019.) (Proof modification is discouraged.) |
| ⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ( I ↾ 𝐴) ⊆ 𝑅) | ||
| Theorem | idinxpssinxp4 38321* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 38319). (Contributed by Peter Mazsa, 8-Mar-2019.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
| Theorem | relcnveq3 38322* | Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.) |
| ⊢ (Rel 𝑅 → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
| Theorem | relcnveq 38323 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.) |
| ⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
| Theorem | relcnveq2 38324* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
| ⊢ (Rel 𝑅 → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
| Theorem | relcnveq4 38325* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
| ⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
| Theorem | qsresid 38326 | Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.) |
| ⊢ (𝐴 / (𝑅 ↾ 𝐴)) = (𝐴 / 𝑅) | ||
| Theorem | n0elqs 38327 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019.) |
| ⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ 𝐴 ⊆ dom 𝑅) | ||
| Theorem | n0elqs2 38328 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ dom (𝑅 ↾ 𝐴) = 𝐴) | ||
| Theorem | ecex2 38329 | Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.) |
| ⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V)) | ||
| Theorem | uniqsALTV 38330 | The union of a quotient set, like uniqs 8817 but with a weaker antecedent: only the restriction of 𝑅 by 𝐴 needs to be a set, not 𝑅 itself, see e.g. cnvepima 38338. (Contributed by Peter Mazsa, 20-Jun-2019.) |
| ⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
| Theorem | imaexALTV 38331 | Existence of an image of a class. Theorem 3.17 of [Monk1] p. 39. (cf. imaexg 7935) with weakened antecedent: only the restriction of 𝐴 by a set needs to be a set, not 𝐴 itself, see e.g. cnvepimaex 38337. (Contributed by Peter Mazsa, 22-Feb-2023.) (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∨ ((𝐴 ↾ 𝐵) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋)) → (𝐴 “ 𝐵) ∈ V) | ||
| Theorem | ecexALTV 38332 | Existence of a coset, like ecexg 8749 but with a weaker antecedent: only the restriction of 𝑅 by the singleton of 𝐴 needs to be a set, not 𝑅 itself, see e.g. eccnvepex 38336. (Contributed by Peter Mazsa, 22-Feb-2023.) |
| ⊢ ((𝑅 ↾ {𝐴}) ∈ 𝑉 → [𝐴]𝑅 ∈ V) | ||
| Theorem | rnresequniqs 38333 | The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.) |
| ⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅)) | ||
| Theorem | n0el2 38334 | 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 38335 | Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V) | ||
| Theorem | eccnvepex 38336 | The converse epsilon coset exists. (Contributed by Peter Mazsa, 22-Mar-2023.) |
| ⊢ [𝐴]◡ E ∈ V | ||
| Theorem | cnvepimaex 38337 | The image of converse epsilon exists, proof via imaexALTV 38331 (see also cnvepima 38338 and uniexg 7760 for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) ∈ V) | ||
| Theorem | cnvepima 38338 | The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴) | ||
| Theorem | inex3 38339 | Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V) | ||
| Theorem | inxpex 38340 | Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.) |
| ⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V) | ||
| Theorem | eqres 38341 | Converting a class constant definition by restriction (like df-ers 38664 or df-parts 38766) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.) |
| ⊢ 𝑅 = (𝑆 ↾ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵))) | ||
| Theorem | brrabga 38342* | The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.) |
| ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉𝑅𝐶 ↔ 𝜓)) | ||
| Theorem | brcnvrabga 38343* | The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅〈𝐵, 𝐶〉 ↔ 𝜓)) | ||
| Theorem | opideq 38344 | Equality conditions for ordered pairs 〈𝐴, 𝐴〉 and 〈𝐵, 𝐵〉. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.) |
| ⊢ (𝐴 ∈ 𝑉 → (〈𝐴, 𝐴〉 = 〈𝐵, 𝐵〉 ↔ 𝐴 = 𝐵)) | ||
| Theorem | iss2 38345 | 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 38346* | Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
| Theorem | dfrel5 38347 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.) |
| ⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅) | ||
| Theorem | dfrel6 38348 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.) |
| ⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅) | ||
| Theorem | cnvresrn 38349 | Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.) |
| ⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅 | ||
| Theorem | relssinxpdmrn 38350 | Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023.) |
| ⊢ (Rel 𝑅 → (𝑅 ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆)) | ||
| Theorem | cnvref4 38351 | Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023.) |
| ⊢ (Rel 𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆)) | ||
| Theorem | cnvref5 38352* | 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 38353* | 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 38354* | 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 38355* | Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦)) | ||
| Theorem | inecmo 38356* | 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 38357* | 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 38358* | 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 38359 | 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 38360* | 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 38361* | 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 38362* | 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 38363 | 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 38364 | "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 2636) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.) |
| ⊢ ((∃*𝑥𝜓 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜓 → 𝜑)) | ||
| Theorem | moantr 38365 | Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.) |
| ⊢ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒))) | ||
| Theorem | brabidgaw 38366* | The law of concretion for a binary relation. Special case of brabga 5539. Version of brabidga 38367 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Peter Mazsa, 24-Nov-2018.) (Revised by GG, 2-Apr-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝑥𝑅𝑦 ↔ 𝜑) | ||
| Theorem | brabidga 38367 | The law of concretion for a binary relation. Special case of brabga 5539. Usage of this theorem is discouraged because it depends on ax-13 2377, see brabidgaw 38366 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝑥𝑅𝑦 ↔ 𝜑) | ||
| Theorem | inxp2 38368* | Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.) |
| ⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)} | ||
| Theorem | opabf 38369 | 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 38370 | The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.) |
| ⊢ [𝐴]∅ = ∅ | ||
| Theorem | brcnvin 38371 | Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴))) | ||
| Definition | df-xrn 38372 | Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 38373 and brxrn 38375. This is Scott Fenton's df-txp 35855 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35855. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵)) | ||
| Theorem | xrnss3v 38373 | A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 35879 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35879. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V)) | ||
| Theorem | xrnrel 38374 | A range Cartesian product is a relation. This is Scott Fenton's txprel 35880 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 35880. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ Rel (𝐴 ⋉ 𝐵) | ||
| Theorem | brxrn 38375 | Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 38373, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)〈𝐵, 𝐶〉 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) | ||
| Theorem | brxrn2 38376* | A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = 〈𝑥, 𝑦〉 ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))) | ||
| Theorem | dfxrn2 38377* | Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.) |
| ⊢ (𝑅 ⋉ 𝑆) = ◡{〈〈𝑥, 𝑦〉, 𝑢〉 ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
| Theorem | xrneq1 38378 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)) | ||
| Theorem | xrneq1i 38379 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶) | ||
| Theorem | xrneq1d 38380 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)) | ||
| Theorem | xrneq2 38381 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
| Theorem | xrneq2i 38382 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵) | ||
| Theorem | xrneq2d 38383 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)) | ||
| Theorem | xrneq12 38384 | Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
| Theorem | xrneq12i 38385 | Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷) | ||
| Theorem | xrneq12d 38386 | Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)) | ||
| Theorem | elecxrn 38387* | Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = 〈𝑥, 𝑦〉 ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))) | ||
| Theorem | ecxrn 38388* | The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {〈𝑦, 𝑧〉 ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)}) | ||
| Theorem | disjressuc2 38389* | Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))) | ||
| Theorem | disjecxrn 38390 | Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅))) | ||
| Theorem | disjecxrncnvep 38391 | Two ways of saying that cosets are disjoint, special case of disjecxrn 38390. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))) | ||
| Theorem | disjsuc2 38392* | 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 38393* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.) |
| ⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{〈〈𝑦, 𝑧〉, 𝑢〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)〈𝑦, 𝑧〉))} | ||
| Theorem | xrninxp2 38394* | Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.) |
| ⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {〈𝑢, 𝑥〉 ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))} | ||
| Theorem | xrninxpex 38395 | 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 38396 | Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.) |
| ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) | ||
| Theorem | br1cnvxrn2 38397* | The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
| Theorem | elec1cnvxrn2 38398* | Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧))) | ||
| Theorem | rnxrn 38399* | Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.) |
| ⊢ ran (𝑅 ⋉ 𝑆) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
| Theorem | rnxrnres 38400* | Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.) |
| ⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)} | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |