![]() |
Metamath
Proof Explorer Theorem List (p. 387 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqvrelcoss4 38601* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Theorem | dfcoeleqvrels 38602 | Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 38600, eqvrelcoss3 38599 and eqvrelcoss4 38601 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels } | ||
Theorem | dfcoeleqvrel 38603 | Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 38600, eqvrelcoss3 38599 and eqvrelcoss4 38601 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴) | ||
Definition | df-redunds 38604* | Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 38607) is equivalent to satisfying the redundancy predicate (df-redund 38605). (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ Redunds = ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} | ||
Definition | df-redund 38605 | Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 38607) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) | ||
Definition | df-redundp 38606 | Define the redundancy operator for propositions, cf. df-redund 38605. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))) | ||
Theorem | brredunds 38607 | Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))) | ||
Theorem | brredundsredund 38608 | For sets, binary relation on the class of all redundant sets (brredunds 38607) is equivalent to satisfying the redundancy predicate (df-redund 38605). (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds 〈𝐵, 𝐶〉 ↔ 𝐴 Redund 〈𝐵, 𝐶〉)) | ||
Theorem | redundss3 38609 | Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐷 ⊆ 𝐶 ⇒ ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 → 𝐴 Redund 〈𝐵, 𝐷〉) | ||
Theorem | redundeq1 38610 | Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐴 = 𝐷 ⇒ ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ 𝐷 Redund 〈𝐵, 𝐶〉) | ||
Theorem | redundpim3 38611 | Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜃 → 𝜒) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃)) | ||
Theorem | redundpbi1 38612 | Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ (𝜑 ↔ 𝜃) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒)) | ||
Theorem | refrelsredund4 38613 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 38494) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund 〈 RefRels , ( RefRels ∩ SymRels )〉 | ||
Theorem | refrelsredund2 38614 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 38494) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund 〈 RefRels , EqvRels 〉 | ||
Theorem | refrelsredund3 38615* | The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 38495) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund 〈 RefRels , EqvRels 〉 | ||
Theorem | refrelredund4 38616 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 38496) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅)) | ||
Theorem | refrelredund2 38617 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 38496) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Theorem | refrelredund3 38618* | The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 38497) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Definition | df-dmqss 38619* | Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8749) of the relation on its domain is equal to the set. See comments of df-ers 38644 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.) |
⊢ DomainQss = {〈𝑥, 𝑦〉 ∣ (dom 𝑥 / 𝑥) = 𝑦} | ||
Definition | df-dmqs 38620 | Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 38628. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴) | ||
Theorem | dmqseq 38621 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqi 38622 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆) | ||
Theorem | dmqseqd 38623 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqeq1 38624 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | dmqseqeq1i 38625 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴) | ||
Theorem | dmqseqeq1d 38626 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | brdmqss 38627 | The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | brdmqssqs 38628 | If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴)) | ||
Theorem | n0eldmqs 38629 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅) | ||
Theorem | n0eldmqseq 38630 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.) |
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴) | ||
Theorem | n0elim 38631 | Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ (¬ ∅ ∈ 𝐴 → (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
Theorem | n0el3 38632 | Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (¬ ∅ ∈ 𝐴 ↔ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
Theorem | cnvepresdmqss 38633 | The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴)) | ||
Theorem | cnvepresdmqs 38634 | The domain quotient predicate for the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.) |
⊢ ((◡ E ↾ 𝐴) DomainQs 𝐴 ↔ ¬ ∅ ∈ 𝐴) | ||
Theorem | unidmqs 38635 | The range of a relation is equal to the union of the domain quotient. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ∪ (dom 𝑅 / 𝑅) = ran 𝑅)) | ||
Theorem | unidmqseq 38636 | The union of the domain quotient of a relation is equal to the class 𝐴 if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 28-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → (∪ (dom 𝑅 / 𝑅) = 𝐴 ↔ ran 𝑅 = 𝐴))) | ||
Theorem | dmqseqim 38637 | If the domain quotient of a relation is equal to the class 𝐴, then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → ran 𝑅 = ∪ 𝐴))) | ||
Theorem | dmqseqim2 38638 | Lemma for erimeq2 38659. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴)))) | ||
Theorem | releldmqs 38639* | Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅))) | ||
Theorem | eldmqs1cossres 38640* | Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴))) | ||
Theorem | releldmqscoss 38641* | Elementhood in the domain quotient of the class of cosets by a relation. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom ≀ 𝑅 / ≀ 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑥] ≀ 𝑅))) | ||
Theorem | dmqscoelseq 38642 | Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ ((dom ∼ 𝐴 / ∼ 𝐴) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴) | ||
Theorem | dmqs1cosscnvepreseq 38643 | Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ ((dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴) | ||
Definition | df-ers 38644 |
Define the class of equivalence relations on domain quotients (or: domain
quotients restricted to equivalence relations).
The present definition of equivalence relation in set.mm df-er 8743 "is not standard", "somewhat cryptic", has no constant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 38565, dfeqvrels2 38569, dfeqvrels3 38570 and df-eqvrel 38566, dfeqvrel2 38571, dfeqvrel3 38572 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8743. While we acknowledge the need of a domain component, the present df-er 8743 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38833 and pet 38832). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35916), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 38627), see erimeq 38660 vs. prter3 38863. While I'm sure we need both equivalence relation df-eqvrels 38565 and equivalence relation on domain quotient df-ers 38644, I'm not sure whether we need a third equivalence relation concept with the present dom 𝑅 = 𝐴 component as well: this needs further investigation. As a default I suppose that these two concepts df-eqvrels 38565 and df-ers 38644 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 38645 of the present df-er 8743. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Ers = ( DomainQss ↾ EqvRels ) | ||
Definition | df-erALTV 38645 | Equivalence relation with natural domain predicate, see also the comment of df-ers 38644. Alternate definition is dferALTV2 38649. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 38658. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-comembers 38646 | Define the class of comember equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022.) (Revised by Peter Mazsa, 24-Jul-2023.) |
⊢ CoMembErs = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎} | ||
Definition | df-comember 38647 |
Define the comember equivalence relation on the class 𝐴 (or, the
restricted coelement equivalence relation on its domain quotient 𝐴.)
Alternate definitions are dfcomember2 38654 and dfcomember3 38655.
Later on, in an application of set theory I make a distinction between the default elementhood concept and a special membership concept: membership equivalence relation will be an integral part of that membership concept. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴) | ||
Theorem | brers 38648 | Binary equivalence relation with natural domain, see the comment of df-ers 38644. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | dferALTV2 38649 | Equivalence relation with natural domain predicate, see the comment of df-ers 38644. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | erALTVeq1 38650 | Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | erALTVeq1i 38651 | Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴) | ||
Theorem | erALTVeq1d 38652 | Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | dfcomember 38653 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴) | ||
Theorem | dfcomember2 38654 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | dfcomember3 38655 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | eqvreldmqs 38656 | Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | eqvreldmqs2 38657 | Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | brerser 38658 | Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴)) | ||
Theorem | erimeq2 38659 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 38863 in a more convenient form , see also erimeq 38660). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅)) | ||
Theorem | erimeq 38660 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 38863 and erimeq2 38659). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅)) | ||
Definition | df-funss 38661 | Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 38662). It is used only by df-funsALTV 38662. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels } | ||
Definition | df-funsALTV 38662 | Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 38664, ... , dffunsALTV5 38668. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ FunsALTV = ( Funss ∩ Rels ) | ||
Definition | df-funALTV 38663 |
Define the function relation predicate, i.e., the function predicate.
This definition of the function predicate (based on a more general,
converse reflexive, relation) and the original definition of function in
set.mm df-fun 6564, are always the same, that is
( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 38679.
The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 38678. Alternate definitions are dffunALTV2 38669, ... , dffunALTV5 38672. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹)) | ||
Theorem | dffunsALTV 38664 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels } | ||
Theorem | dffunsALTV2 38665 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I } | ||
Theorem | dffunsALTV3 38666* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 )}. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∀𝑥∀𝑦((𝑢𝑓𝑥 ∧ 𝑢𝑓𝑦) → 𝑥 = 𝑦)} | ||
Theorem | dffunsALTV4 38667* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀𝑥1∃*𝑦1𝑥1𝑓𝑦1}. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∃*𝑥 𝑢𝑓𝑥} | ||
Theorem | dffunsALTV5 38668* | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)} | ||
Theorem | dffunALTV2 38669 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 38695. (Contributed by Peter Mazsa, 8-Feb-2018.) |
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
Theorem | dffunALTV3 38670* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 38696. Reproduction of dffun2 6572. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 ) ∧ Rel 𝐹). (Contributed by NM, 29-Dec-1996.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ Rel 𝐹)) | ||
Theorem | dffunALTV4 38671* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 38697. This is dffun6 6575. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀𝑥1∃*𝑦1𝑥1𝐹𝑦1 ∧ Rel 𝐹). (Contributed by NM, 9-Mar-1995.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ Rel 𝐹)) | ||
Theorem | dffunALTV5 38672* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 38698. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) | ||
Theorem | elfunsALTV 38673 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV2 38674 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV3 38675* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV4 38676* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV5 38677* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTVfunALTV 38678 | The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹)) | ||
Theorem | funALTVfun 38679 | Our definition of the function predicate df-funALTV 38663 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6564, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
Theorem | funALTVss 38680 | Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴)) | ||
Theorem | funALTVeq 38681 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Theorem | funALTVeqi 38682 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
Theorem | funALTVeqd 38683 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Definition | df-disjss 38684 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 38685). It is used only by df-disjs 38685. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
Definition | df-disjs 38685 |
Define the disjoint relations class, i.e., the class of disjoints. We
need Disjs for the definition of Parts and Part
for the
Partition-Equivalence Theorems: this need for Parts as disjoint relations
on their domain quotients is the reason why we must define Disjs
instead of simply using converse functions (cf. dfdisjALTV 38694).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38708. Alternate definitions are dfdisjs 38689, ... , dfdisjs5 38693. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjs = ( Disjss ∩ Rels ) | ||
Definition | df-disjALTV 38686 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 38694,
see the comment of df-disjs 38685 why we need disjoint relations instead of
converse functions anyway.
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38708. Alternate definitions are dfdisjALTV 38694, ... , dfdisjALTV5 38698. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
Definition | df-eldisjs 38687 | Define the disjoint element relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 38710. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
Definition | df-eldisj 38688 |
Define the disjoint element relation predicate, i.e., the disjoint
elementhood predicate. Read: the elements of 𝐴 are disjoint. The
element of the disjoint elements class and the disjoint elementhood
predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when
𝐴 is a set, see eleldisjseldisj 38710.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 38853 with dfeldisj5 38702. See also the comments of dfmembpart2 38751 and of df-parts 38746. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
Theorem | dfdisjs 38689 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
Theorem | dfdisjs2 38690 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
Theorem | dfdisjs3 38691* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
Theorem | dfdisjs4 38692* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
Theorem | dfdisjs5 38693* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
Theorem | dfdisjALTV 38694 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 38685 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV2 38695 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 38669. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV3 38696* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 38670. (Contributed by Peter Mazsa, 28-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV4 38697* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 38671. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV5 38698* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 38672. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
Theorem | dfeldisj2 38699 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
Theorem | dfeldisj3 38700* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |