![]() |
Metamath
Proof Explorer Theorem List (p. 386 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 | elrefrelsrel 38501 | For sets, being an element of the class of reflexive relations (df-refrels 38492) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅)) | ||
Theorem | refreleq 38502 | Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆)) | ||
Theorem | refrelid 38503 | Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ RefRel I | ||
Theorem | refrelcoss 38504 | The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.) |
⊢ RefRel ≀ 𝑅 | ||
Theorem | refrelressn 38505 | Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38423) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴})) | ||
Definition | df-cnvrefs 38506 | Define the class of all converse reflexive sets, see the comment of df-ssr 38479. It is used only by df-cnvrefrels 38507. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-cnvrefrels 38507 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 38509 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 38487) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23528), symmetric (df-syms 38523) and transitive (df-trs 38553) sets.
We use this concept to define functions (df-funsALTV 38662, df-funALTV 38663) and disjoints (df-disjs 38685, df-disjALTV 38686). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38517. Alternate definitions are dfcnvrefrels2 38509 and dfcnvrefrels3 38510. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
Definition | df-cnvrefrel 38508 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38512. Alternate definitions are dfcnvrefrel2 38511 and dfcnvrefrel3 38512. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrels2 38509 | Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
Theorem | dfcnvrefrels3 38510* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
Theorem | dfcnvrefrel2 38511 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel3 38512* | 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 38497. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel4 38513 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel5 38514* | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | elcnvrefrels2 38515 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrels3 38516* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrelsrel 38517 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 38507) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
Theorem | cnvrefrelcoss2 38518 | 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 38519 | 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 38520* | 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 38521* | 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 38522* | 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 38523 |
Define the class of all symmetric sets. It is used only by df-symrels 38524.
Note the similarity of Definitions df-refs 38491, df-syms 38523 and df-trs 38553, cf. the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-symrels 38524 |
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 38538. Alternate definitions are
dfsymrels2 38526, dfsymrels3 38527, dfsymrels4 38528 and dfsymrels5 38529.
This definition is similar to the definitions of the classes of reflexive (df-refrels 38492) and transitive (df-trrels 38554) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ SymRels = ( Syms ∩ Rels ) | ||
Definition | df-symrel 38525 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 38524) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 38538. Alternate definitions are dfsymrel2 38530 and dfsymrel3 38531. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfsymrels2 38526 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
Theorem | dfsymrels3 38527* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
Theorem | dfsymrels4 38528 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
Theorem | dfsymrels5 38529* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
Theorem | dfsymrel2 38530 | 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 38531* | 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 38532 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfsymrel5 38533* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅)) | ||
Theorem | elsymrels2 38534 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels3 38535* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels4 38536 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels5 38537* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrelsrel 38538 | For sets, being an element of the class of symmetric relations (df-symrels 38524) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅)) | ||
Theorem | symreleq 38539 | Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆)) | ||
Theorem | symrelim 38540 | Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | symrelcoss 38541 | The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.) |
⊢ SymRel ≀ 𝑅 | ||
Theorem | idsymrel 38542 | The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.) |
⊢ SymRel I | ||
Theorem | epnsymrel 38543 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ SymRel E | ||
Theorem | symrefref2 38544 | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 38545. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅)) | ||
Theorem | symrefref3 38545* | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 38544. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)) | ||
Theorem | refsymrels2 38546 | 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 38569) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38494, cf. the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} | ||
Theorem | refsymrels3 38547* | 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 38570) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 38495, cf. the comment of dfrefrel3 38497. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))} | ||
Theorem | refsymrel2 38548 | 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 38496, cf. the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | refsymrel3 38549* | 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 38497, cf. the comment of dfrefrel3 38497. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅)) | ||
Theorem | elrefsymrels2 38550 | 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 38569) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 38494, cf. the comment of dfrefrels2 38494. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrels3 38551* | 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 38570) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 38495, cf. the comment of dfrefrel3 38497. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrelsrel 38552 | 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 38553 |
Define the class of all transitive sets (versus the transitive class
defined in df-tr 5265). It is used only by df-trrels 38554.
Note the similarity of the definitions of df-refs 38491, df-syms 38523 and df-trs 38553. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-trrels 38554 |
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 38562. Alternate definitions
are dftrrels2 38556 and dftrrels3 38557.
This definition is similar to the definitions of the classes of reflexive (df-refrels 38492) and symmetric (df-symrels 38524) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ TrRels = ( Trs ∩ Rels ) | ||
Definition | df-trrel 38555 | Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 38554) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 38562. Alternate definitions are dftrrel2 38558 and dftrrel3 38559. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dftrrels2 38556 |
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 5697 (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 38392 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 38557* | Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)} | ||
Theorem | dftrrel2 38558 | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dftrrel3 38559* | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅)) | ||
Theorem | eltrrels2 38560 | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrels3 38561* | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrelsrel 38562 | 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 38563 | 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 38564 | Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38423) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.) |
⊢ TrRel (𝑅 ↾ {𝐴}) | ||
Definition | df-eqvrels 38565 | 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 38575. Alternate definitions are dfeqvrels2 38569 and dfeqvrels3 38570. (Contributed by Peter Mazsa, 7-Nov-2018.) |
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | ||
Definition | df-eqvrel 38566 | Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 38565) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 38575. Alternate definitions are dfeqvrel2 38571 and dfeqvrel3 38572. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)) | ||
Definition | df-coeleqvrels 38567 | 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 38577. Alternate definition is dfcoeleqvrels 38602. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels } | ||
Definition | df-coeleqvrel 38568 | Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 38603. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 38577. (Contributed by Peter Mazsa, 11-Dec-2021.) |
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) | ||
Theorem | dfeqvrels2 38569 | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} | ||
Theorem | dfeqvrels3 38570* | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
Theorem | dfeqvrel2 38571 | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfeqvrel3 38572* | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅)) | ||
Theorem | eleqvrels2 38573 | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrels3 38574* | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrelsrel 38575 | 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 38576 | Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels )) | ||
Theorem | elcoeleqvrelsrel 38577 | 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 38578 | An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.) |
⊢ ( EqvRel 𝑅 → Rel 𝑅) | ||
Theorem | eqvrelrefrel 38579 | An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → RefRel 𝑅) | ||
Theorem | eqvrelsymrel 38580 | An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → SymRel 𝑅) | ||
Theorem | eqvreltrrel 38581 | An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → TrRel 𝑅) | ||
Theorem | eqvrelim 38582 | Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | eqvreleq 38583 | Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvreleqi 38584 | Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆) | ||
Theorem | eqvreleqd 38585 | Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvrelsym 38586 | An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) | ||
Theorem | eqvrelsymb 38587 | An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | eqvreltr 38588 | An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | eqvreltrd 38589 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvreltr4d 38590 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvrelref 38591 | An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐴) | ||
Theorem | eqvrelth 38592 | Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
Theorem | eqvrelcl 38593 | Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) | ||
Theorem | eqvrelthi 38594 | Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) | ||
Theorem | eqvreldisj 38595 | Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ ( EqvRel 𝑅 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) | ||
Theorem | qsdisjALTV 38596 | Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) (Revised by Peter Mazsa, 3-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) ⇒ ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
Theorem | eqvrelqsel 38597 | If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 28-Dec-2019.) |
⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅) | ||
Theorem | eqvrelcoss 38598 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅) | ||
Theorem | eqvrelcoss3 38599* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eqvrelcoss2 38600 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |