Home | Metamath
Proof Explorer Theorem List (p. 357 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coss0 35601 | Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.) |
⊢ ≀ ∅ = ∅ | ||
Theorem | cossid 35602 | Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.) |
⊢ ≀ I = I | ||
Theorem | cosscnvid 35603 | Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ≀ ◡ I = I | ||
Theorem | trcoss 35604* | Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.) |
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eleccossin 35605 | Two ways of saying that the coset of 𝐴 and the coset of 𝐶 have the common element 𝐵. (Contributed by Peter Mazsa, 15-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∈ ([𝐴] ≀ 𝑅 ∩ [𝐶] ≀ 𝑅) ↔ (𝐴 ≀ 𝑅𝐵 ∧ 𝐵 ≀ 𝑅𝐶))) | ||
Theorem | trcoss2 35606* | Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.) |
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Definition | df-rels 35607 |
Define the relations class. Proper class relations (like I, see
reli 5692) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 35609).
The class of relations is a great tool we can use when we define classes of different relations as nullary class constants as required by the 2. point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 35609. When we want to define a specific class of relations as a nullary class constant, the appropriate method is the following: 1. We define the specific nullary class constant for general sets (see e.g. df-refs 35632), then 2. we get the required class of relations by the intersection of the class of general sets above with the class of relations df-rels 35607 (see df-refrels 35633 and the resulting dfrefrels2 35635 and dfrefrels3 35636). 3. Finally, in order to be able to work with proper classes (like iprc 7606) as well, we define the predicate of the relation (see df-refrel 35634) so that it is true for the relevant proper classes (see refrelid 35643), and that the element of the class of the required relations (e.g. elrefrels3 35640) and this predicate are the same in case of sets (see elrefrelsrel 35641). (Contributed by Peter Mazsa, 13-Jun-2018.) |
⊢ Rels = 𝒫 (V × V) | ||
Theorem | elrels2 35608 | The element of the relations class (df-rels 35607) and the relation predicate (df-rel 5556) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V))) | ||
Theorem | elrelsrel 35609 | The element of the relations class (df-rels 35607) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅)) | ||
Theorem | elrelsrelim 35610 | The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ (𝑅 ∈ Rels → Rel 𝑅) | ||
Theorem | elrels5 35611 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅)) | ||
Theorem | elrels6 35612 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)) | ||
Theorem | elrelscnveq3 35613* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq 35614 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | elrelscnveq2 35615* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq4 35616* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | cnvelrels 35617 | The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels ) | ||
Theorem | cosselrels 35618 | Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels ) | ||
Theorem | cosscnvelrels 35619 | Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels ) | ||
Definition | df-ssr 35620* |
Define the subsets class or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5459) and identity relation
(df-id 5454) classes. Subset relation class and Scott
Fenton's subset
class df-sset 33215 are the same: S = SSet (compare dfssr2 35621 with
df-sset 33215), the only reason we do not use dfssr2 35621 as the base
definition of the subsets class is the way we defined the epsilon
relation and the identity relation classes.
The binary relation on the class of subsets and the subclass relationship (df-ss 3951) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 35623. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3951. The only exception (aside from directly investigating the class S e.g. in relssr 35622 or in extssr 35631) is when we have a specific purpose with its usage, like in case of df-refs 35632 versus df-cnvrefs 35645, where we need S to define the class of reflexive sets in order to be able to define the class of converse reflexive sets with the help of the converse of S. The subsets class S has another place in set.mm as well: if we define extensional relation based on the common property in extid 35451, extep 35423 and extssr 35631, then "extrelssr" " |- ExtRel S " is a theorem along with "extrelep" " |- ExtRel E " and "extrelid" " |- ExtRel I " . (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ S = {〈𝑥, 𝑦〉 ∣ 𝑥 ⊆ 𝑦} | ||
Theorem | dfssr2 35621 | Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E ))) | ||
Theorem | relssr 35622 | The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ Rel S | ||
Theorem | brssr 35623 | The subset relation and subclass relationship (df-ss 3951) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | brssrid 35624 | Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴) | ||
Theorem | issetssr 35625 | Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴) | ||
Theorem | brssrres 35626 | Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
Theorem | br1cnvssrres 35627 | Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵))) | ||
Theorem | brcnvssr 35628 | The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
Theorem | brcnvssrid 35629 | Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴) | ||
Theorem | br1cossxrncnvssrres 35630* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by range Cartesian product with restricted converse subsets class: a binary relation. (Contributed by Peter Mazsa, 9-Jun-2021.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (◡ S ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝐶 ⊆ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐸 ⊆ 𝑢 ∧ 𝑢𝑅𝐷)))) | ||
Theorem | extssr 35631 | Property of subset relation, see also extid 35451, extep 35423 and the comment of df-ssr 35620. (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵)) | ||
Definition | df-refs 35632 |
Define the class of all reflexive sets. It is used only by df-refrels 35633.
We use subset relation S (df-ssr 35620) here to be able to define
converse reflexivity (df-cnvrefs 35645), see also the comment of df-ssr 35620.
The elements of this class are not necessarily relations (versus
df-refrels 35633).
Note the similarity of the definitions df-refs 35632, df-syms 35660 and df-trs 35690, cf. comments of dfrefrels2 35635. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-refrels 35633 |
Define the class of reflexive relations. This is practically dfrefrels2 35635
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 35635).
Another alternative definition is dfrefrels3 35636. The element of this class and the reflexive relation predicate (df-refrel 35634) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 35641. This definition is similar to the definitions of the classes of symmetric (df-symrels 35661) and transitive (df-trrels 35691) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ RefRels = ( Refs ∩ Rels ) | ||
Definition | df-refrel 35634 | Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 35638. Alternate definitions are dfrefrel2 35637 and dfrefrel3 35638. For sets, being an element of the class of reflexive relations (df-refrels 35633) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 35641. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfrefrels2 35635 |
Alternate definition of the class of reflexive relations. This is a 0-ary
class constant, which is recommended for definitions (see the 1.
Guideline at https://us.metamath.org/ileuni/mathbox.html).
Proper
classes (like I, see iprc 7606)
are not elements of this (or any)
class: if a class is an element of another class, it is not a proper class
but a set, see elex 3513. So if we use 0-ary constant classes as our
main
definitions, they are valid only for sets, not for proper classes. For
proper classes we use predicate-type definitions like df-refrel 35634. See
also the comment of df-rels 35607.
Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 35635, it keeps restriction of I: this is why the very similar definitions df-refs 35632, df-syms 35660 and df-trs 35690 diverge when we switch from (general) sets to relations in dfrefrels2 35635, dfsymrels2 35663 and dftrrels2 35693. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} | ||
Theorem | dfrefrels3 35636* | Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)} | ||
Theorem | dfrefrel2 35637 | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfrefrel3 35638* |
Alternate definition of the reflexive relation predicate. A relation is
reflexive iff: for all elements on its domain and range, if an element
of its domain is the same as an element of its range, then there is the
relation between them.
Note that this is definitely not the definition we are accustomed to, like e.g. idref 6901 / idrefALT 5967 or df-reflexive 44765 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 35684. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 35706, can we write the traditional form ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 for reflexive relations. For the special case with square Cartesian product when the two forms are equivalent see idinxpssinxp4 35460 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 35651. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅)) | ||
Theorem | elrefrels2 35639 | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrels3 35640* | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrelsrel 35641 | For sets, being an element of the class of reflexive relations (df-refrels 35633) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅)) | ||
Theorem | refreleq 35642 | Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆)) | ||
Theorem | refrelid 35643 | Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ RefRel I | ||
Theorem | refrelcoss 35644 | The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.) |
⊢ RefRel ≀ 𝑅 | ||
Definition | df-cnvrefs 35645 | Define the class of all converse reflexive sets, see the comment of df-ssr 35620. It is used only by df-cnvrefrels 35646. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-cnvrefrels 35646 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 35648 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 35628) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 22043), symmetric (df-syms 35660) and transitive (df-trs 35690) sets.
We use this concept to define functions (df-funsALTV 35796, df-funALTV 35797) and disjoints (df-disjs 35819, df-disjALTV 35820). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 35654. Alternate definitions are dfcnvrefrels2 35648 and dfcnvrefrels3 35649. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
Definition | df-cnvrefrel 35647 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 35651. Alternate definitions are dfcnvrefrel2 35650 and dfcnvrefrel3 35651. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrels2 35648 | Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
Theorem | dfcnvrefrels3 35649* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
Theorem | dfcnvrefrel2 35650 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel3 35651* | Alternate definition of the converse reflexive relation predicate. A relation is converse reflexive iff: for all elements on its domain and range, if for an element of its domain and for an element of its range there is the relation between them, then the two elements are the same, cf. the comment of dfrefrel3 35638. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | elcnvrefrels2 35652 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrels3 35653* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrelsrel 35654 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 35646) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
Theorem | cnvrefrelcoss2 35655 | Necessary and sufficient condition for a coset relation to be a converse reflexive relation. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( CnvRefRel ≀ 𝑅 ↔ ≀ 𝑅 ⊆ I ) | ||
Theorem | cosselcnvrefrels2 35656 | Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ ( ≀ 𝑅 ⊆ I ∧ ≀ 𝑅 ∈ Rels )) | ||
Theorem | cosselcnvrefrels3 35657* | Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦) ∧ ≀ 𝑅 ∈ Rels )) | ||
Theorem | cosselcnvrefrels4 35658* | Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑢∃*𝑥 𝑢𝑅𝑥 ∧ ≀ 𝑅 ∈ Rels )) | ||
Theorem | cosselcnvrefrels5 35659* | Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ ran 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 ∨ ([𝑥]◡𝑅 ∩ [𝑦]◡𝑅) = ∅) ∧ ≀ 𝑅 ∈ Rels )) | ||
Definition | df-syms 35660 |
Define the class of all symmetric sets. It is used only by df-symrels 35661.
Note the similarity of the definitions df-refs 35632, df-syms 35660 and df-trs 35690, cf. the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-symrels 35661 |
Define the class of symmetric relations. For sets, being an element of
the class of symmetric relations is equivalent to satisfying the symmetric
relation predicate, see elsymrelsrel 35675. Alternate definitions are
dfsymrels2 35663, dfsymrels3 35664, dfsymrels4 35665 and dfsymrels5 35666.
This definition is similar to the definitions of the classes of reflexive (df-refrels 35633) and transitive (df-trrels 35691) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ SymRels = ( Syms ∩ Rels ) | ||
Definition | df-symrel 35662 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 35661) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 35675. Alternate definitions are dfsymrel2 35667 and dfsymrel3 35668. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfsymrels2 35663 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
Theorem | dfsymrels3 35664* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
Theorem | dfsymrels4 35665 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
Theorem | dfsymrels5 35666* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
Theorem | dfsymrel2 35667 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019.) (Revised by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfsymrel3 35668* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ Rel 𝑅)) | ||
Theorem | dfsymrel4 35669 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfsymrel5 35670* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅)) | ||
Theorem | elsymrels2 35671 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels3 35672* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels4 35673 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels5 35674* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrelsrel 35675 | For sets, being an element of the class of symmetric relations (df-symrels 35661) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅)) | ||
Theorem | symreleq 35676 | Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆)) | ||
Theorem | symrelim 35677 | Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | symrelcoss 35678 | The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.) |
⊢ SymRel ≀ 𝑅 | ||
Theorem | idsymrel 35679 | The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.) |
⊢ SymRel I | ||
Theorem | epnsymrel 35680 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ SymRel E | ||
Theorem | symrefref2 35681 | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 35682. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅)) | ||
Theorem | symrefref3 35682* | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 35681. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)) | ||
Theorem | refsymrels2 35683 | Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 35705) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 35635, cf. the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} | ||
Theorem | refsymrels3 35684* | Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 35706) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 35636, cf. the comment of dfrefrel3 35638. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))} | ||
Theorem | refsymrel2 35685 | A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrel2 35637, cf. the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | refsymrel3 35686* | A relation which is reflexive and symmetric (like an equivalence relation) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for its reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrel3 35638, cf. the comment of dfrefrel3 35638. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅)) | ||
Theorem | elrefsymrels2 35687 | Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 35705) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 35635, cf. the comment of dfrefrels2 35635. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrels3 35688* | Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 35706) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 35636, cf. the comment of dfrefrel3 35638. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrelsrel 35689 | For sets, being an element of the class of reflexive and symmetric relations is equivalent to satisfying the reflexive and symmetric relation predicates. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( RefRel 𝑅 ∧ SymRel 𝑅))) | ||
Definition | df-trs 35690 |
Define the class of all transitive sets (versus the transitive class
defined in df-tr 5165). It is used only by df-trrels 35691.
Note the similarity of the definitions of df-refs 35632, df-syms 35660 and df-trs 35690. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-trrels 35691 |
Define the class of transitive relations. For sets, being an element of
the class of transitive relations is equivalent to satisfying the
transitive relation predicate, see eltrrelsrel 35699. Alternate definitions
are dftrrels2 35693 and dftrrels3 35694.
This definition is similar to the definitions of the classes of reflexive (df-refrels 35633) and symmetric (df-symrels 35661) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ TrRels = ( Trs ∩ Rels ) | ||
Definition | df-trrel 35692 | Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 35691) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 35699. Alternate definitions are dftrrel2 35695 and dftrrel3 35696. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dftrrels2 35693 |
Alternate definition of the class of transitive relations.
I'd prefer to define the class of transitive relations by using the definition of composition by [Suppes] p. 63. df-coSUP (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝐴𝑢 ∧ 𝑢𝐵𝑦)} as opposed to the present definition of composition df-co 5558 (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} because the Suppes definition keeps the order of 𝐴, 𝐵, 𝐶, 𝑅, 𝑆, 𝑇 by default in trsinxpSUP (((𝑅 ∩ (𝐴 × 𝐵)) ∘ (𝑆 ∩ (𝐵 × 𝐶))) ⊆ (𝑇 ∩ (𝐴 × 𝐶)) ↔ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵∀ 𝑧 ∈ 𝐶((𝑥𝑅𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑇𝑧)) while the present definition of composition disarranges them: trsinxp (((𝑆 ∩ (𝐵 × 𝐶)) ∘ (𝑅 ∩ (𝐴 × 𝐵))) ⊆ (𝑇 ∩ (𝐴 × 𝐶 )) ↔ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵∀𝑧 ∈ 𝐶((𝑥𝑅𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑇𝑧) ). This is not mission critical to me, the implication of the Suppes definition is just more aesthetic, at least in the above case. If we swap to the Suppes definition of class composition, I would define the present class of all transitive sets as df-trsSUP and I would consider to switch the definition of the class of cosets by 𝑅 from the present df-coss 35541 to a df-cossSUP. But perhaps there is a mathematical reason to keep the present definition of composition. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟} | ||
Theorem | dftrrels3 35694* | Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)} | ||
Theorem | dftrrel2 35695 | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dftrrel3 35696* | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅)) | ||
Theorem | eltrrels2 35697 | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrels3 35698* | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrelsrel 35699 | For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ TrRels ↔ TrRel 𝑅)) | ||
Theorem | trreleq 35700 | Equality theorem for the transitive relation predicate. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |