![]() |
Metamath
Proof Explorer Theorem List (p. 387 of 489) | < 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-30950) |
![]() (30951-32473) |
![]() (32474-48899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmqseqeq1d 38601 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | brdmqss 38602 | The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | brdmqssqs 38603 | 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 38604 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅) | ||
Theorem | n0eldmqseq 38605 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.) |
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴) | ||
Theorem | n0elim 38606 | 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 38607 | 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 38608 | 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 38609 | 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 38610 | 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 38611 | 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 38612 | 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 38613 | Lemma for erimeq2 38634. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴)))) | ||
Theorem | releldmqs 38614* | Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅))) | ||
Theorem | eldmqs1cossres 38615* | Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴))) | ||
Theorem | releldmqscoss 38616* | 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 38617 | 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 38618 | 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 38619 |
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 8763 "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 38540, dfeqvrels2 38544, dfeqvrels3 38545 and df-eqvrel 38541, dfeqvrel2 38546, dfeqvrel3 38547 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8763. While we acknowledge the need of a domain component, the present df-er 8763 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38808 and pet 38807). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35899), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 38602), see erimeq 38635 vs. prter3 38838. While I'm sure we need both equivalence relation df-eqvrels 38540 and equivalence relation on domain quotient df-ers 38619, 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 38540 and df-ers 38619 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 38620 of the present df-er 8763. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Ers = ( DomainQss ↾ EqvRels ) | ||
Definition | df-erALTV 38620 | Equivalence relation with natural domain predicate, see also the comment of df-ers 38619. Alternate definition is dferALTV2 38624. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 38633. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-comembers 38621 | 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 38622 |
Define the comember equivalence relation on the class 𝐴 (or, the
restricted coelement equivalence relation on its domain quotient 𝐴.)
Alternate definitions are dfcomember2 38629 and dfcomember3 38630.
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 38623 | Binary equivalence relation with natural domain, see the comment of df-ers 38619. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | dferALTV2 38624 | Equivalence relation with natural domain predicate, see the comment of df-ers 38619. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | erALTVeq1 38625 | Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | erALTVeq1i 38626 | Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴) | ||
Theorem | erALTVeq1d 38627 | Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | dfcomember 38628 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴) | ||
Theorem | dfcomember2 38629 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | dfcomember3 38630 | 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 38631 | 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 38632 | 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 38633 | 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 38634 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 38838 in a more convenient form , see also erimeq 38635). (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 38635 | 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 38838 and erimeq2 38634). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅)) | ||
Definition | df-funss 38636 | Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 38637). It is used only by df-funsALTV 38637. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels } | ||
Definition | df-funsALTV 38637 | Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 38639, ... , dffunsALTV5 38643. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ FunsALTV = ( Funss ∩ Rels ) | ||
Definition | df-funALTV 38638 |
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 6575, are always the same, that is
( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 38654.
The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 38653. Alternate definitions are dffunALTV2 38644, ... , dffunALTV5 38647. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹)) | ||
Theorem | dffunsALTV 38639 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels } | ||
Theorem | dffunsALTV2 38640 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I } | ||
Theorem | dffunsALTV3 38641* | 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 38642* | 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 38643* | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)} | ||
Theorem | dffunALTV2 38644 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 38670. (Contributed by Peter Mazsa, 8-Feb-2018.) |
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
Theorem | dffunALTV3 38645* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 38671. Reproduction of dffun2 6583. 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 38646* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 38672. This is dffun6 6586. 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 38647* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 38673. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) | ||
Theorem | elfunsALTV 38648 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV2 38649 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV3 38650* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV4 38651* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV5 38652* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTVfunALTV 38653 | 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 38654 | Our definition of the function predicate df-funALTV 38638 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6575, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
Theorem | funALTVss 38655 | 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 38656 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Theorem | funALTVeqi 38657 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
Theorem | funALTVeqd 38658 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Definition | df-disjss 38659 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 38660). It is used only by df-disjs 38660. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
Definition | df-disjs 38660 |
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 38669).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38683. Alternate definitions are dfdisjs 38664, ... , dfdisjs5 38668. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjs = ( Disjss ∩ Rels ) | ||
Definition | df-disjALTV 38661 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 38669,
see the comment of df-disjs 38660 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 38683. Alternate definitions are dfdisjALTV 38669, ... , dfdisjALTV5 38673. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
Definition | df-eldisjs 38662 | 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 38685. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
Definition | df-eldisj 38663 |
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 38685.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 38828 with dfeldisj5 38677. See also the comments of dfmembpart2 38726 and of df-parts 38721. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
Theorem | dfdisjs 38664 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
Theorem | dfdisjs2 38665 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
Theorem | dfdisjs3 38666* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
Theorem | dfdisjs4 38667* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
Theorem | dfdisjs5 38668* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
Theorem | dfdisjALTV 38669 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 38660 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV2 38670 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 38644. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV3 38671* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 38645. (Contributed by Peter Mazsa, 28-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV4 38672* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 38646. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV5 38673* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 38647. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
Theorem | dfeldisj2 38674 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
Theorem | dfeldisj3 38675* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) | ||
Theorem | dfeldisj4 38676* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
Theorem | dfeldisj5 38677* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
Theorem | eldisjs 38678 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs2 38679 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs3 38680* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs4 38681* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs5 38682* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
Theorem | eldisjsdisj 38683 | The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅)) | ||
Theorem | eleldisjs 38684 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 38685 | The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴)) | ||
Theorem | disjrel 38686 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 38687 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 38688 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 38689 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 38690 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 38691 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 38692 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 38693 | Lemma for the equality theorem for partition parteq1 38730. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 38694 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 38695 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 38696 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 38697 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 38698 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 38699 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjres 38700* | Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |