![]() |
Metamath
Proof Explorer Theorem List (p. 350 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-cnvrefs 34901 | Define the class of all converse reflexive sets, cf. the comment of df-ssr 34876. It is used only by df-cnvrefrels 34902. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-cnvrefrels 34902 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 34904 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 34884) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 21717), symmetric (df-syms 34916) and transitive (df-trs 34946) sets.
We use this concept to define functions ( ~? df-funsALTV , ~? df-funALTV ) and disjoints ( ~? df-disjs , ~? df-disjALTV ). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, cf. elcnvrefrelsrel 34910. Alternate definitions are dfcnvrefrels2 34904 and dfcnvrefrels3 34905. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
Definition | df-cnvrefrel 34903 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), cf. the comment of dfcnvrefrel3 34907. Alternate definitions are dfcnvrefrel2 34906 and dfcnvrefrel3 34907. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrels2 34904 | Alternate definition of the class of converse reflexive relations. Cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
Theorem | dfcnvrefrels3 34905* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
Theorem | dfcnvrefrel2 34906 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel3 34907* | 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 34894. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | elcnvrefrels2 34908 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrels3 34909* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrelsrel 34910 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 34902) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
Theorem | cnvrefrelcoss2 34911 | 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 34912 | 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 34913* | 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 34914* | 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 34915* | 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 34916 |
Define the class of all symmetric sets. It is used only by df-symrels 34917.
Note the similarity of the definitions df-refs 34888, df-syms 34916 and df-trs 34946, cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-symrels 34917 |
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, cf. elsymrelsrel 34931. Alternate definitions are
dfsymrels2 34919, dfsymrels3 34920, dfsymrels4 34921 and dfsymrels5 34922.
This definition is similar to the definitions of the classes of reflexive (df-refrels 34889) and transitive (df-trrels 34947) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ SymRels = ( Syms ∩ Rels ) | ||
Definition | df-symrel 34918 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 34917) is equivalent to satisfying the symmetric relation predicate, cf. elsymrelsrel 34931. Alternate definitions are dfsymrel2 34923 and dfsymrel3 34924. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfsymrels2 34919 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
Theorem | dfsymrels3 34920* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
Theorem | dfsymrels4 34921 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
Theorem | dfsymrels5 34922* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
Theorem | dfsymrel2 34923 | 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 34924* | 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 34925 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfsymrel5 34926* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅)) | ||
Theorem | elsymrels2 34927 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels3 34928* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels4 34929 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels5 34930* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrelsrel 34931 | For sets, being an element of the class of symmetric relations (df-symrels 34917) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅)) | ||
Theorem | symreleq 34932 | Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆)) | ||
Theorem | symrelim 34933 | Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | symrelcoss 34934 | The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.) |
⊢ SymRel ≀ 𝑅 | ||
Theorem | idsymrel 34935 | The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.) |
⊢ SymRel I | ||
Theorem | epnsymrel 34936 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ SymRel E | ||
Theorem | symrefref2 34937 | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, cf. symrefref3 34938. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅)) | ||
Theorem | symrefref3 34938* | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, cf. symrefref2 34937. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)) | ||
Theorem | refsymrels2 34939 | 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 34960) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 34891, cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} | ||
Theorem | refsymrels3 34940* | 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 34961) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 34892, cf. the comment of dfrefrels3 34892. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))} | ||
Theorem | refsymrel2 34941 | 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 34893, cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | refsymrel3 34942* | 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 34894, cf. the comment of dfrefrel3 34894. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅)) | ||
Theorem | elrefsymrels2 34943 | 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 34960) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 34891, cf. the comment of dfrefrels2 34891. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrels3 34944* | 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 34961) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 34892, cf. the comment of dfrefrels3 34892. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrelsrel 34945 | 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 34946 |
Define the class of all transitive sets (versus the transitive class
defined in df-tr 4988). It is used only by df-trrels 34947.
Note the similarity of the definitions of df-refs 34888, df-syms 34916 and df-trs 34946. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-trrels 34947 |
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, cf. eltrrelsrel 34955. Alternate definitions
are dftrrels2 34949 and dftrrels3 34950.
This definition is similar to the definitions of the classes of reflexive (df-refrels 34889) and symmetric (df-symrels 34917) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ TrRels = ( Trs ∩ Rels ) | ||
Definition | df-trrel 34948 | Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 34947) is equivalent to satisfying the transitive relation predicate, cf. eltrrelsrel 34955. Alternate definitions are dftrrel2 34951 and dftrrel3 34952. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dftrrels2 34949 |
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 5364 (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} because the Suppes definition keeps the order of 𝐴, 𝐵, 𝐶, 𝑅, 𝑆, 𝑇 by default in trsinxpSUP ( ( ( R i^i ( A X. B ) ) o. ( S i^i ( B X. C ) ) ) C_ ( T i^i ( A X. C ) ) <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y S z ) -> x T z ) ) while the present definition of composition disarranges them: trsinxp ( ( ( S i^i ( B X. C ) ) o. ( R i^i ( A X. B ) ) ) C_ ( T i^i ( A X. C ) ) <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y S z ) -> x T z ) ). 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 34797 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 34950* | Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)} | ||
Theorem | dftrrel2 34951 | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dftrrel3 34952* | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅)) | ||
Theorem | eltrrels2 34953 | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrels3 34954* | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrelsrel 34955 | 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 34956 | Equality theorem for the transitive relation predicate. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆)) | ||
Definition | df-eqvrels 34957 | 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, cf. eleqvrelsrel 34966. Alternate definitions are dfeqvrels2 34960 and dfeqvrels3 34961. (Contributed by Peter Mazsa, 7-Nov-2018.) |
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | ||
Definition | df-eqvrel 34958 | Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 34957) is equivalent to satisfying the equivalence relation predicate, cf. eleqvrelsrel 34966. Alternate definitions are dfeqvrel2 34962 and dfeqvrel3 34963. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)) | ||
Definition | df-eleqvrel 34959 |
Define the elementhood equivalence relation predicate. (Read: 𝐴 has
disjoint elements, or, the elementhood equivalence relation on 𝐴.)
We do not use this definition, this is just a placeholder for the sake of the symmetry with ~? df-eldisj . Disjointness of two sets is often defined as no elements in common: we cannot ignore this tradition completely. This is why we need ~? df-eldisj which in our case is a special case of a more general disjointness definition ~? df-disjALTV . We could use a corresponding elementhood equivalence relation (i.e., this definition), but this would change ~? mpet3 to a much less intuitive form. Instead, we defined coelements df-coels 34798 as a special case of cosets df-coss 34797, and use the general equivalence relation definition with these special cosets, i.e., with coelements, which results in the more intuitive ~? mpet3 . (Contributed by Peter Mazsa, 11-Dec-2021.) |
⊢ ( ElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) | ||
Theorem | dfeqvrels2 34960 | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} | ||
Theorem | dfeqvrels3 34961* | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
Theorem | dfeqvrel2 34962 | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfeqvrel3 34963* | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅)) | ||
Theorem | eleqvrels2 34964 | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrels3 34965* | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrelsrel 34966 | 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 | eqvrelrel 34967 | An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.) |
⊢ ( EqvRel 𝑅 → Rel 𝑅) | ||
Theorem | eqvrelrefrel 34968 | An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → RefRel 𝑅) | ||
Theorem | eqvrelsymrel 34969 | An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → SymRel 𝑅) | ||
Theorem | eqvreltrrel 34970 | An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → TrRel 𝑅) | ||
Theorem | eqvrelim 34971 | Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | eqvreleq 34972 | Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvreleqi 34973 | Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆) | ||
Theorem | eqvreleqd 34974 | Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvrelsym 34975 | 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 34976 | 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 34977 | 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 34978 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvreltr4d 34979 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvrelref 34980 | 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 34981 | 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 34982 | 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 34983 | 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 34984 | 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 34985 | 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 | eqvrelcoss 34986 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅) | ||
Theorem | eqvrelcoss3 34987* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eqvrelcoss2 34988 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅) | ||
Theorem | eqvrelcoss4 34989* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Theorem | eqvrelcoels4 34990* | Two ways to express equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.) |
⊢ ( EqvRel ∼ 𝐴 ↔ ∀𝑥∀𝑧(([𝑥] ∼ 𝐴 ∩ [𝑧] ∼ 𝐴) ≠ ∅ → ([𝑥]◡(◡ E ↾ 𝐴) ∩ [𝑧]◡(◡ E ↾ 𝐴)) ≠ ∅)) | ||
Theorem | eqvrelqsel 34991 | 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 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅) | ||
Definition | df-reds 34992* | Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brreds 34995) is equivalent to satisfying the redundancy predicate (df-red 34993). (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ Reds = ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} | ||
Definition | df-red 34993 | Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brreds 34995) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ (𝐴 Red 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) | ||
Definition | df-redp 34994 | Define the redundancy operator for propositions, cf. df-red 34993. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ ( red (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))) | ||
Theorem | brreds 34995 | Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Reds 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))) | ||
Theorem | brredsred 34996 | For sets, binary relation on the class of all redundant sets (brreds 34995) is equivalent to satisfying the redundancy predicate (df-red 34993). (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Reds 〈𝐵, 𝐶〉 ↔ 𝐴 Red 〈𝐵, 𝐶〉)) | ||
Theorem | redss3 34997 | Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐷 ⊆ 𝐶 ⇒ ⊢ (𝐴 Red 〈𝐵, 𝐶〉 → 𝐴 Red 〈𝐵, 𝐷〉) | ||
Theorem | redeq1 34998 | Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐴 = 𝐷 ⇒ ⊢ (𝐴 Red 〈𝐵, 𝐶〉 ↔ 𝐷 Red 〈𝐵, 𝐶〉) | ||
Theorem | redpim3 34999 | Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜃 → 𝜒) ⇒ ⊢ ( red (𝜑, 𝜓, 𝜒) → red (𝜑, 𝜓, 𝜃)) | ||
Theorem | redpbi1 35000 | Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ (𝜑 ↔ 𝜃) ⇒ ⊢ ( red (𝜑, 𝜓, 𝜒) ↔ red (𝜃, 𝜓, 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |