Home | Metamath
Proof Explorer Theorem List (p. 365 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | abeqinbi 36401* | Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} & ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓} | ||
Theorem | rabeqel 36402* | Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eqrelf 36403* | The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | releleccnv 36404 | Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | releccnveq 36405* | Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵))) | ||
Theorem | opelvvdif 36406 | Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ((V × V) ∖ 𝑅) ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅)) | ||
Theorem | vvdifopab 36407* | Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ ((V × V) ∖ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑦〉 ∣ ¬ 𝜑} | ||
Theorem | brvdif 36408 | Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵) | ||
Theorem | brvdif2 36409 | Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | brvvdif 36410 | Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)) | ||
Theorem | brvbrvvdif 36411 | Binary relation with the complement under the universal class of ordered pairs is the same as with universal complement. (Contributed by Peter Mazsa, 28-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ 𝐴(V ∖ 𝑅)𝐵)) | ||
Theorem | brcnvep 36412 | The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | elecALTV 36413 | Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 8550 with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | brcnvepres 36414 | Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) | ||
Theorem | brres2 36415 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.) |
⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶) | ||
Theorem | eldmres 36416* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝐵𝑅𝑦))) | ||
Theorem | eldm4 36417* | Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑦 𝑦 ∈ [𝐴]𝑅)) | ||
Theorem | eldmres2 36418* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ [𝐵]𝑅))) | ||
Theorem | eceq1i 36419 | Equality theorem for 𝐶-coset of 𝐴 and 𝐶-coset of 𝐵, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐴]𝐶 = [𝐵]𝐶 | ||
Theorem | elecres 36420 | Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | ecres 36421* | Restricted coset of 𝐵. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ [𝐵](𝑅 ↾ 𝐴) = {𝑥 ∣ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝑥)} | ||
Theorem | ecres2 36422 | The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.) |
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅) | ||
Theorem | eccnvepres 36423* | Restricted converse epsilon coset of 𝐵. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → [𝐵](◡ E ↾ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝐵 ∈ 𝐴}) | ||
Theorem | eleccnvep 36424 | Elementhood in the converse epsilon coset of 𝐴 is elementhood in 𝐴. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡ E ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | eccnvep 36425 | The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡ E = 𝐴) | ||
Theorem | extep 36426 | Property of epsilon relation, see also extid 36453, extssr 36634 and the comment of df-ssr 36623. (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ E = [𝐵]◡ E ↔ 𝐴 = 𝐵)) | ||
Theorem | eccnvepres2 36427 | The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019.) |
⊢ (𝐵 ∈ 𝐴 → [𝐵](◡ E ↾ 𝐴) = 𝐵) | ||
Theorem | eccnvepres3 36428 | Condition for a restricted converse epsilon coset of a set to be the set itself. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ (𝐵 ∈ dom (◡ E ↾ 𝐴) → [𝐵](◡ E ↾ 𝐴) = 𝐵) | ||
Theorem | eldmqsres 36429* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 (∃𝑥 𝑥 ∈ [𝑢]𝑅 ∧ 𝐵 = [𝑢]𝑅))) | ||
Theorem | eldmqsres2 36430* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑢]𝑅)) | ||
Theorem | qsss1 36431 | Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 / 𝐶) ⊆ (𝐵 / 𝐶)) | ||
Theorem | qseq1i 36432 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 / 𝐶) = (𝐵 / 𝐶) | ||
Theorem | qseq1d 36433 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | brinxprnres 36434 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | inxprnres 36435* | Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)} | ||
Theorem | dfres4 36436 | Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ↾ 𝐴) = (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) | ||
Theorem | exan3 36437* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅) ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
Theorem | exanres 36438* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres3 36439* | Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres2 36440* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆))) | ||
Theorem | cnvepres 36441* | Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ (◡ E ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)} | ||
Theorem | eqrel2 36442* | Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))) | ||
Theorem | rncnv 36443 | Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.) |
⊢ ran ◡𝐴 = dom 𝐴 | ||
Theorem | dfdm6 36444* | Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅} | ||
Theorem | dfrn6 36445* | Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.) |
⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅} | ||
Theorem | rncnvepres 36446 | 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 36447 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8555). (Contributed by Peter Mazsa, 9-Oct-2018.) |
⊢ (𝜑 → dom 𝑅 = 𝐴) & ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | ||
Theorem | dmec2d 36448 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 8555). (Contributed by Peter Mazsa, 12-Oct-2018.) |
⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅)) | ||
Theorem | brid 36449 | Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.) |
⊢ (𝐴 I 𝐵 ↔ 𝐵 I 𝐴) | ||
Theorem | ideq2 36450 | 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 36451 | 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 36452 | 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 36453 | Property of identity relation, see also extep 36426, extssr 36634 and the comment of df-ssr 36623. (Contributed by Peter Mazsa, 5-Jul-2019.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴]◡ I = [𝐵]◡ I ↔ 𝐴 = 𝐵)) | ||
Theorem | inxpss 36454* | Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | idinxpss 36455* | 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 | inxpss3 36456* | Two ways to say that an intersection with a Cartesian product is a subclass (see also inxpss 36454). (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ (∀𝑥∀𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 → 𝑥(𝑆 ∩ (𝐴 × 𝐵))𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | inxpss2 36457* | Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑆 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | inxpssidinxp 36458* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 36457. (Contributed by Peter Mazsa, 4-Jul-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ ( I ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥 = 𝑦)) | ||
Theorem | idinxpssinxp 36459* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 36457. (Contributed by Peter Mazsa, 6-Mar-2019.) |
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | idinxpssinxp2 36460* | 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 36461 | 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 36462* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 36460). (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | relcnveq3 36463* | Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.) |
⊢ (Rel 𝑅 → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | relcnveq 36464 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.) |
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | relcnveq2 36465* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ (Rel 𝑅 → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | relcnveq4 36466* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | qsresid 36467 | Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.) |
⊢ (𝐴 / (𝑅 ↾ 𝐴)) = (𝐴 / 𝑅) | ||
Theorem | n0elqs 36468 | 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 36469 | 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 36470 | Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.) |
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V)) | ||
Theorem | uniqsALTV 36471 | The union of a quotient set, like uniqs 8575 but with a weaker antecedent: only the restricion of 𝑅 by 𝐴 needs to be a set, not 𝑅 itself, see e.g. cnvepima 36479. (Contributed by Peter Mazsa, 20-Jun-2019.) |
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
Theorem | imaexALTV 36472 | Existence of an image of a class. Theorem 3.17 of [Monk1] p. 39. (cf. imaexg 7771) with weakened antecedent: only the restricion of 𝐴 by a set needs to be a set, not 𝐴 itself, see e.g. cnvepimaex 36478. (Contributed by Peter Mazsa, 22-Feb-2023.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∨ ((𝐴 ↾ 𝐵) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋)) → (𝐴 “ 𝐵) ∈ V) | ||
Theorem | ecexALTV 36473 | Existence of a coset, like ecexg 8511 but with a weaker antecedent: only the restricion of 𝑅 by the singleton of 𝐴 needs to be a set, not 𝑅 itself, see e.g. eccnvepex 36477. (Contributed by Peter Mazsa, 22-Feb-2023.) |
⊢ ((𝑅 ↾ {𝐴}) ∈ 𝑉 → [𝐴]𝑅 ∈ V) | ||
Theorem | rnresequniqs 36474 | The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018.) |
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ran (𝑅 ↾ 𝐴) = ∪ (𝐴 / 𝑅)) | ||
Theorem | n0el2 36475 | 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 36476 | Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E ↾ 𝐴) ∈ V) | ||
Theorem | eccnvepex 36477 | The converse epsilon coset exists. (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ [𝐴]◡ E ∈ V | ||
Theorem | cnvepimaex 36478 | The image of converse epsilon exists, proof via imaexALTV 36472 (see also cnvepima 36479 and uniexg 7602 for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) ∈ V) | ||
Theorem | cnvepima 36479 | The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E “ 𝐴) = ∪ 𝐴) | ||
Theorem | inex3 36480 | Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | inxpex 36481 | Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019.) |
⊢ ((𝑅 ∈ 𝑊 ∨ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑅 ∩ (𝐴 × 𝐵)) ∈ V) | ||
Theorem | eqres 36482 | Converting a class constant definition by restriction (like df-ers 36782 or ~? df-parts ) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.) |
⊢ 𝑅 = (𝑆 ↾ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴𝑆𝐵))) | ||
Theorem | brrabga 36483* | The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉𝑅𝐶 ↔ 𝜓)) | ||
Theorem | brcnvrabga 36484* | The law of concretion for the converse of operation class abstraction. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑅〈𝐵, 𝐶〉 ↔ 𝜓)) | ||
Theorem | opideq 36485 | Equality conditions for ordered pairs 〈𝐴, 𝐴〉 and 〈𝐵, 𝐵〉. (Contributed by Peter Mazsa, 22-Jul-2019.) (Revised by Thierry Arnoux, 16-Feb-2022.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐴, 𝐴〉 = 〈𝐵, 𝐵〉 ↔ 𝐴 = 𝐵)) | ||
Theorem | iss2 36486 | 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 36487* | Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ◡𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | dfrel5 36488 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ dom 𝑅) = 𝑅) | ||
Theorem | dfrel6 36489 | Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019.) |
⊢ (Rel 𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅) | ||
Theorem | cnvresrn 36490 | Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021.) |
⊢ (◡𝑅 ↾ ran 𝑅) = ◡𝑅 | ||
Theorem | ecin0 36491* | 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 36492* | 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 36493* | Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ∨ (𝐶 ∩ 𝐷) = ∅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧∀𝑦 ∈ 𝐵 ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → 𝑥 = 𝑦)) | ||
Theorem | inecmo 36494* | 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 36495* | 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 36496* | 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 36497 | 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 36498* | 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 36499* | 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 36500* | 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 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |