Home | Metamath
Proof Explorer Theorem List (p. 370 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elsymrels2 36901 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels3 36902* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels4 36903 | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrels5 36904* | Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elsymrelsrel 36905 | For sets, being an element of the class of symmetric relations (df-symrels 36891) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅)) | ||
Theorem | symreleq 36906 | Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆)) | ||
Theorem | symrelim 36907 | Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | symrelcoss 36908 | The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.) |
⊢ SymRel ≀ 𝑅 | ||
Theorem | idsymrel 36909 | The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.) |
⊢ SymRel I | ||
Theorem | epnsymrel 36910 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ SymRel E | ||
Theorem | symrefref2 36911 | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 36912. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅)) | ||
Theorem | symrefref3 36912* | Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 36911. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)) | ||
Theorem | refsymrels2 36913 | 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 36936) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 36861, cf. the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)} | ||
Theorem | refsymrels3 36914* | 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 36937) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 36862, cf. the comment of dfrefrel3 36864. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))} | ||
Theorem | refsymrel2 36915 | 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 36863, cf. the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | refsymrel3 36916* | 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 36864, cf. the comment of dfrefrel3 36864. (Contributed by Peter Mazsa, 23-Aug-2021.) |
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅)) | ||
Theorem | elrefsymrels2 36917 | 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 36936) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 36861, cf. the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrels3 36918* | 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 36937) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 36862, cf. the comment of dfrefrel3 36864. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefsymrelsrel 36919 | 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 36920 |
Define the class of all transitive sets (versus the transitive class
defined in df-tr 5222). It is used only by df-trrels 36921.
Note the similarity of the definitions of df-refs 36858, df-syms 36890 and df-trs 36920. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-trrels 36921 |
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 36929. Alternate definitions
are dftrrels2 36923 and dftrrels3 36924.
This definition is similar to the definitions of the classes of reflexive (df-refrels 36859) and symmetric (df-symrels 36891) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ TrRels = ( Trs ∩ Rels ) | ||
Definition | df-trrel 36922 | Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 36921) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 36929. Alternate definitions are dftrrel2 36925 and dftrrel3 36926. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dftrrels2 36923 |
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 5640 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 36759 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 36924* | Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)} | ||
Theorem | dftrrel2 36925 | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dftrrel3 36926* | Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅)) | ||
Theorem | eltrrels2 36927 | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrels3 36928* | Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eltrrelsrel 36929 | 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 36930 | 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 36931 | Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 36790) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.) |
⊢ TrRel (𝑅 ↾ {𝐴}) | ||
Definition | df-eqvrels 36932 | 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 36942. Alternate definitions are dfeqvrels2 36936 and dfeqvrels3 36937. (Contributed by Peter Mazsa, 7-Nov-2018.) |
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | ||
Definition | df-eqvrel 36933 | Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 36932) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 36942. Alternate definitions are dfeqvrel2 36938 and dfeqvrel3 36939. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)) | ||
Definition | df-coeleqvrels 36934 | Define the 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 36944. Alternate definition is dfcoeleqvrels 36969. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels } | ||
Definition | df-coeleqvrel 36935 | Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 36970. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 36944. (Contributed by Peter Mazsa, 11-Dec-2021.) |
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) | ||
Theorem | dfeqvrels2 36936 | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} | ||
Theorem | dfeqvrels3 36937* | Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.) |
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))} | ||
Theorem | dfeqvrel2 36938 | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfeqvrel3 36939* | Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.) |
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅)) | ||
Theorem | eleqvrels2 36940 | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrels3 36941* | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrelsrel 36942 | 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 36943 | Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels )) | ||
Theorem | elcoeleqvrelsrel 36944 | 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 36945 | An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.) |
⊢ ( EqvRel 𝑅 → Rel 𝑅) | ||
Theorem | eqvrelrefrel 36946 | An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → RefRel 𝑅) | ||
Theorem | eqvrelsymrel 36947 | An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → SymRel 𝑅) | ||
Theorem | eqvreltrrel 36948 | An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → TrRel 𝑅) | ||
Theorem | eqvrelim 36949 | Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | eqvreleq 36950 | Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvreleqi 36951 | Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆) | ||
Theorem | eqvreleqd 36952 | Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvrelsym 36953 | 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 36954 | 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 36955 | 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 36956 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvreltr4d 36957 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvrelref 36958 | 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 36959 | 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 36960 | 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 36961 | 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 36962 | 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 36963 | 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 36964 | 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 36965 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅) | ||
Theorem | eqvrelcoss3 36966* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eqvrelcoss2 36967 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅) | ||
Theorem | eqvrelcoss4 36968* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Theorem | dfcoeleqvrels 36969 | Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 36967, eqvrelcoss3 36966 and eqvrelcoss4 36968 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels } | ||
Theorem | dfcoeleqvrel 36970 | Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 36967, eqvrelcoss3 36966 and eqvrelcoss4 36968 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴) | ||
Definition | df-redunds 36971* | Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 36974) is equivalent to satisfying the redundancy predicate (df-redund 36972). (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} | ||
Definition | df-redund 36972 | Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 36974) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) | ||
Definition | df-redundp 36973 | Define the redundancy operator for propositions, cf. df-redund 36972. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))) | ||
Theorem | brredunds 36974 | Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))) | ||
Theorem | brredundsredund 36975 | For sets, binary relation on the class of all redundant sets (brredunds 36974) is equivalent to satisfying the redundancy predicate (df-redund 36972). (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩)) | ||
Theorem | redundss3 36976 | Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐷 ⊆ 𝐶 ⇒ ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩) | ||
Theorem | redundeq1 36977 | Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐴 = 𝐷 ⇒ ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩) | ||
Theorem | redundpim3 36978 | Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜃 → 𝜒) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃)) | ||
Theorem | redundpbi1 36979 | Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ (𝜑 ↔ 𝜃) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒)) | ||
Theorem | refrelsredund4 36980 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 36861) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩ | ||
Theorem | refrelsredund2 36981 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 36861) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩ | ||
Theorem | refrelsredund3 36982* | The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 36862) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩ | ||
Theorem | refrelredund4 36983 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 36863) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅)) | ||
Theorem | refrelredund2 36984 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 36863) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Theorem | refrelredund3 36985* | The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 36864) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Definition | df-dmqss 36986* | Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8588) of the relation on its domain is equal to the set. See comments of df-ers 37011 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.) |
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦} | ||
Definition | df-dmqs 36987 | Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 36995. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴) | ||
Theorem | dmqseq 36988 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqi 36989 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆) | ||
Theorem | dmqseqd 36990 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqeq1 36991 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | dmqseqeq1i 36992 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴) | ||
Theorem | dmqseqeq1d 36993 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | brdmqss 36994 | The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | brdmqssqs 36995 | If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴)) | ||
Theorem | n0eldmqs 36996 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅) | ||
Theorem | n0eldmqseq 36997 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.) |
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴) | ||
Theorem | n0elim 36998 | Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ (¬ ∅ ∈ 𝐴 → (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
Theorem | n0el3 36999 | Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (¬ ∅ ∈ 𝐴 ↔ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
Theorem | cnvepresdmqss 37000 | The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |