| Metamath
Proof Explorer Theorem List (p. 386 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | relssr 38501 | The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.) |
| ⊢ Rel S | ||
| Theorem | brssr 38502 | The subset relation and subclass relationship (df-ss 3968) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | brssrid 38503 | Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴) | ||
| Theorem | issetssr 38504 | Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.) |
| ⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴) | ||
| Theorem | brssrres 38505 | Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
| ⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
| Theorem | br1cnvssrres 38506 | Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵))) | ||
| Theorem | brcnvssr 38507 | The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
| Theorem | brcnvssrid 38508 | Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴) | ||
| Theorem | br1cossxrncnvssrres 38509* | 〈𝐵, 𝐶〉 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 38510 | Property of subset relation, see also extid 38311, extep 38284 and the comment of df-ssr 38499. (Contributed by Peter Mazsa, 10-Jul-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵)) | ||
| Definition | df-refs 38511 |
Define the class of all reflexive sets. It is used only by df-refrels 38512.
We use subset relation S (df-ssr 38499) here to be able to define
converse reflexivity (df-cnvrefs 38526), see also the comment of df-ssr 38499.
The elements of this class are not necessarily relations (versus
df-refrels 38512).
Note the similarity of Definitions df-refs 38511, df-syms 38543 and df-trs 38573, cf. comments of dfrefrels2 38514. (Contributed by Peter Mazsa, 19-Jul-2019.) |
| ⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
| Definition | df-refrels 38512 |
Define the class of reflexive relations. This is practically dfrefrels2 38514
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 38514).
Another alternative definition is dfrefrels3 38515. The element of this class and the reflexive relation predicate (df-refrel 38513) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 38521. This definition is similar to the definitions of the classes of symmetric (df-symrels 38544) and transitive (df-trrels 38574) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
| ⊢ RefRels = ( Refs ∩ Rels ) | ||
| Definition | df-refrel 38513 | Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 38517. Alternate definitions are dfrefrel2 38516 and dfrefrel3 38517. For sets, being an element of the class of reflexive relations (df-refrels 38512) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 38521. (Contributed by Peter Mazsa, 16-Jul-2021.) |
| ⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
| Theorem | dfrefrels2 38514 |
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 7933)
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 3501. 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 38513. See
also the comment of df-rels 38486.
Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 38514, it keeps restriction of I: this is why the very similar definitions df-refs 38511, df-syms 38543 and df-trs 38573 diverge when we switch from (general) sets to relations in dfrefrels2 38514, dfsymrels2 38546 and dftrrels2 38576. (Contributed by Peter Mazsa, 20-Jul-2019.) |
| ⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} | ||
| Theorem | dfrefrels3 38515* | Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.) |
| ⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)} | ||
| Theorem | dfrefrel2 38516 | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
| Theorem | dfrefrel3 38517* |
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 7166 / idrefALT 6131 or df-reflexive 49287 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 38567. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 38590, 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 38321 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 38532. (Contributed by Peter Mazsa, 8-Jul-2019.) |
| ⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅)) | ||
| Theorem | dfrefrel5 38518* | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.) |
| ⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅)) | ||
| Theorem | elrefrels2 38519 | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
| ⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elrefrels3 38520* | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
| ⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elrefrelsrel 38521 | For sets, being an element of the class of reflexive relations (df-refrels 38512) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅)) | ||
| Theorem | refreleq 38522 | Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆)) | ||
| Theorem | refrelid 38523 | Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ RefRel I | ||
| Theorem | refrelcoss 38524 | The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.) |
| ⊢ RefRel ≀ 𝑅 | ||
| Theorem | refrelressn 38525 | Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38443) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴})) | ||
| Definition | df-cnvrefs 38526 | Define the class of all converse reflexive sets, see the comment of df-ssr 38499. It is used only by df-cnvrefrels 38527. (Contributed by Peter Mazsa, 22-Jul-2019.) |
| ⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
| Definition | df-cnvrefrels 38527 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 38529 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 38507) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23513), symmetric (df-syms 38543) and transitive (df-trs 38573) sets.
We use this concept to define functions (df-funsALTV 38682, df-funALTV 38683) and disjoints (df-disjs 38705, df-disjALTV 38706). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38537. Alternate definitions are dfcnvrefrels2 38529 and dfcnvrefrels3 38530. (Contributed by Peter Mazsa, 7-Jul-2019.) |
| ⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
| Definition | df-cnvrefrel 38528 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38532. Alternate definitions are dfcnvrefrel2 38531 and dfcnvrefrel3 38532. (Contributed by Peter Mazsa, 16-Jul-2021.) |
| ⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
| Theorem | dfcnvrefrels2 38529 | Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 21-Jul-2021.) |
| ⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
| Theorem | dfcnvrefrels3 38530* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
| ⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
| Theorem | dfcnvrefrel2 38531 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
| ⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
| Theorem | dfcnvrefrel3 38532* | 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 38517. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
| Theorem | dfcnvrefrel4 38533 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
| ⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅)) | ||
| Theorem | dfcnvrefrel5 38534* | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
| ⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
| Theorem | elcnvrefrels2 38535 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
| ⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elcnvrefrels3 38536* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
| ⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elcnvrefrelsrel 38537 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 38527) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
| Theorem | cnvrefrelcoss2 38538 | 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 38539 | 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 38540* | 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 38541* | 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 38542* | 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 38543 |
Define the class of all symmetric sets. It is used only by df-symrels 38544.
Note the similarity of Definitions df-refs 38511, df-syms 38543 and df-trs 38573, cf. the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 19-Jul-2019.) |
| ⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
| Definition | df-symrels 38544 |
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 38558. Alternate definitions are
dfsymrels2 38546, dfsymrels3 38547, dfsymrels4 38548 and dfsymrels5 38549.
This definition is similar to the definitions of the classes of reflexive (df-refrels 38512) and transitive (df-trrels 38574) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
| ⊢ SymRels = ( Syms ∩ Rels ) | ||
| Definition | df-symrel 38545 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 38544) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 38558. Alternate definitions are dfsymrel2 38550 and dfsymrel3 38551. (Contributed by Peter Mazsa, 16-Jul-2021.) |
| ⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
| Theorem | dfsymrels2 38546 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 20-Jul-2019.) |
| ⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
| Theorem | dfsymrels3 38547* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
| ⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
| Theorem | dfsymrels4 38548 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
| ⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
| Theorem | dfsymrels5 38549* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
| ⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
| Theorem | dfsymrel2 38550 | 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 38551* | 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 38552 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅)) | ||
| Theorem | dfsymrel5 38553* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅)) | ||
| Theorem | elsymrels2 38554 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elsymrels3 38555* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elsymrels4 38556 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elsymrels5 38557* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elsymrelsrel 38558 | For sets, being an element of the class of symmetric relations (df-symrels 38544) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅)) | ||
| Theorem | symreleq 38559 | Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆)) | ||
| Theorem | symrelim 38560 | Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
| Theorem | symrelcoss 38561 | The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.) |
| ⊢ SymRel ≀ 𝑅 | ||
| Theorem | idsymrel 38562 | The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.) |
| ⊢ SymRel I | ||
| Theorem | epnsymrel 38563 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
| ⊢ ¬ SymRel E | ||
| Theorem | symrefref2 38564 | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 38565. (Contributed by Peter Mazsa, 19-Jul-2018.) |
| ⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅)) | ||
| Theorem | symrefref3 38565* | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 38564. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)) | ||
| Theorem | refsymrels2 38566 | 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 38589) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38514, cf. the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 20-Jul-2019.) |
| ⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} | ||
| Theorem | refsymrels3 38567* | 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 38590) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 38515, cf. the comment of dfrefrel3 38517. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))} | ||
| Theorem | refsymrel2 38568 | 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 38516, cf. the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 23-Aug-2021.) |
| ⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅)) | ||
| Theorem | refsymrel3 38569* | 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 38517, cf. the comment of dfrefrel3 38517. (Contributed by Peter Mazsa, 23-Aug-2021.) |
| ⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅)) | ||
| Theorem | elrefsymrels2 38570 | 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 38589) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 38514, cf. the comment of dfrefrels2 38514. (Contributed by Peter Mazsa, 22-Jul-2019.) |
| ⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elrefsymrels3 38571* | 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 38590) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 38515, cf. the comment of dfrefrel3 38517. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | elrefsymrelsrel 38572 | 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 38573 |
Define the class of all transitive sets (versus the transitive class
defined in df-tr 5260). It is used only by df-trrels 38574.
Note the similarity of the definitions of df-refs 38511, df-syms 38543 and df-trs 38573. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
| Definition | df-trrels 38574 |
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 38582. Alternate definitions
are dftrrels2 38576 and dftrrels3 38577.
This definition is similar to the definitions of the classes of reflexive (df-refrels 38512) and symmetric (df-symrels 38544) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
| ⊢ TrRels = ( Trs ∩ Rels ) | ||
| Definition | df-trrel 38575 | Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 38574) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 38582. Alternate definitions are dftrrel2 38578 and dftrrel3 38579. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
| Theorem | dftrrels2 38576 |
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 5694 (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 38412 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 38577* | Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
| ⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)} | ||
| Theorem | dftrrel2 38578 | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
| Theorem | dftrrel3 38579* | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅)) | ||
| Theorem | eltrrels2 38580 | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eltrrels3 38581* | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
| ⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eltrrelsrel 38582 | 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 38583 | Equality theorem for the transitive relation predicate. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆)) | ||
| Theorem | trrelressn 38584 | Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38443) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.) |
| ⊢ TrRel (𝑅 ↾ {𝐴}) | ||
| Definition | df-eqvrels 38585 | Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 38595. Alternate definitions are dfeqvrels2 38589 and dfeqvrels3 38590. (Contributed by Peter Mazsa, 7-Nov-2018.) |
| ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | ||
| Definition | df-eqvrel 38586 | Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 38585) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 38595. Alternate definitions are dfeqvrel2 38591 and dfeqvrel3 38592. (Contributed by Peter Mazsa, 17-Apr-2019.) |
| ⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)) | ||
| Definition | df-coeleqvrels 38587 | Define the coelement equivalence relations class, the class of sets with coelement equivalence relations. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 38597. Alternate definition is dfcoeleqvrels 38622. (Contributed by Peter Mazsa, 28-Nov-2022.) |
| ⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels } | ||
| Definition | df-coeleqvrel 38588 | Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 38623. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 38597. (Contributed by Peter Mazsa, 11-Dec-2021.) |
| ⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) | ||
| Theorem | dfeqvrels2 38589 | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
| ⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} | ||
| Theorem | dfeqvrels3 38590* | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
| ⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
| Theorem | dfeqvrel2 38591 | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
| ⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅)) | ||
| Theorem | dfeqvrel3 38592* | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
| ⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅)) | ||
| Theorem | eleqvrels2 38593 | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
| ⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eleqvrels3 38594* | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
| ⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eleqvrelsrel 38595 | For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate. (Contributed by Peter Mazsa, 24-Aug-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅)) | ||
| Theorem | elcoeleqvrels 38596 | Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels )) | ||
| Theorem | elcoeleqvrelsrel 38597 | For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴)) | ||
| Theorem | eqvrelrel 38598 | An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.) |
| ⊢ ( EqvRel 𝑅 → Rel 𝑅) | ||
| Theorem | eqvrelrefrel 38599 | An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ ( EqvRel 𝑅 → RefRel 𝑅) | ||
| Theorem | eqvrelsymrel 38600 | An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ ( EqvRel 𝑅 → SymRel 𝑅) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |