P. 378 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfcnvrefrels2 37701	Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))}
Theorem	dfcnvrefrels3 37702*	Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)}
Theorem	dfcnvrefrel2 37703	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrel3 37704*	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 37689. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	dfcnvrefrel4 37705	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfcnvrefrel5 37706*	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	elcnvrefrels2 37707	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrels3 37708*	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrelsrel 37709	For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 37699) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅))
Theorem	cnvrefrelcoss2 37710	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 37711	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 37712*	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 37713*	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 37714*	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 ))
21.24.9  Symmetry
Definition	df-syms 37715	Define the class of all symmetric sets. It is used only by df-symrels 37716. Note the similarity of Definitions df-refs 37683, df-syms 37715 and df-trs 37745, cf. the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 37716	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 37730. Alternate definitions are dfsymrels2 37718, dfsymrels3 37719, dfsymrels4 37720 and dfsymrels5 37721. This definition is similar to the definitions of the classes of reflexive (df-refrels 37684) and transitive (df-trrels 37746) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 37717	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 37716) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 37730. Alternate definitions are dfsymrel2 37722 and dfsymrel3 37723. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfsymrels2 37718	Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
Theorem	dfsymrels3 37719*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)}
Theorem	dfsymrels4 37720	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟}
Theorem	dfsymrels5 37721*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}
Theorem	dfsymrel2 37722	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 37723*	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 37724	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel5 37725*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	elsymrels2 37726	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels3 37727*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels4 37728	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels5 37729*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrelsrel 37730	For sets, being an element of the class of symmetric relations (df-symrels 37716) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅))
Theorem	symreleq 37731	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 37732	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 37733	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 37734	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 37735	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.24.10  Reflexivity and symmetry
Theorem	symrefref2 37736	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 37737. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 37737*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 37736. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 37738	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 37761) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 37686, cf. the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
Theorem	refsymrels3 37739*	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 37762) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 37687, cf. the comment of dfrefrel3 37689. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))}
Theorem	refsymrel2 37740	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 37688, cf. the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	refsymrel3 37741*	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 37689, cf. the comment of dfrefrel3 37689. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅))
Theorem	elrefsymrels2 37742	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 37761) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 37686, cf. the comment of dfrefrels2 37686. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrels3 37743*	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 37762) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 37687, cf. the comment of dfrefrel3 37689. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrelsrel 37744	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 𝑅)))
21.24.11  Transitivity
Definition	df-trs 37745	Define the class of all transitive sets (versus the transitive class defined in df-tr 5265). It is used only by df-trrels 37746. Note the similarity of the definitions of df-refs 37683, df-syms 37715 and df-trs 37745. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-trrels 37746	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 37754. Alternate definitions are dftrrels2 37748 and dftrrels3 37749. This definition is similar to the definitions of the classes of reflexive (df-refrels 37684) and symmetric (df-symrels 37716) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ TrRels = ( Trs ∩ Rels )
Definition	df-trrel 37747	Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 37746) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 37754. Alternate definitions are dftrrel2 37750 and dftrrel3 37751. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dftrrels2 37748	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 5684 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 37584 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 37749*	Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)}
Theorem	dftrrel2 37750	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dftrrel3 37751*	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅))
Theorem	eltrrels2 37752	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	eltrrels3 37753*	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels ))
Theorem	eltrrelsrel 37754	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 37755	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 37756	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 37615) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.)
⊢ TrRel (𝑅 ↾ {𝐴})
21.24.12  Equivalence relations
Definition	df-eqvrels 37757	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 37767. Alternate definitions are dfeqvrels2 37761 and dfeqvrels3 37762. (Contributed by Peter Mazsa, 7-Nov-2018.)
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
Definition	df-eqvrel 37758	Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 37757) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 37767. Alternate definitions are dfeqvrel2 37763 and dfeqvrel3 37764. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
Definition	df-coeleqvrels 37759	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 37769. Alternate definition is dfcoeleqvrels 37794. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels }
Definition	df-coeleqvrel 37760	Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 37795. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 37769. (Contributed by Peter Mazsa, 11-Dec-2021.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴))
Theorem	dfeqvrels2 37761	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}
Theorem	dfeqvrels3 37762*	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Theorem	dfeqvrel2 37763	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	dfeqvrel3 37764*	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅))
Theorem	eleqvrels2 37765	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrels3 37766*	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrelsrel 37767	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 37768	Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels ))
Theorem	elcoeleqvrelsrel 37769	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 37770	An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → Rel 𝑅)
Theorem	eqvrelrefrel 37771	An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → RefRel 𝑅)
Theorem	eqvrelsymrel 37772	An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → SymRel 𝑅)
Theorem	eqvreltrrel 37773	An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → TrRel 𝑅)
Theorem	eqvrelim 37774	Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	eqvreleq 37775	Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvreleqi 37776	Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆)
Theorem	eqvreleqd 37777	Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvrelsym 37778	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 37779	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 37780	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 37781	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvreltr4d 37782	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvrelref 37783	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 37784	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 37785	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 37786	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 37787	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 37788	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 37789	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 37790	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅)
Theorem	eqvrelcoss3 37791*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eqvrelcoss2 37792	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅)
Theorem	eqvrelcoss4 37793*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	dfcoeleqvrels 37794	Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 37792, eqvrelcoss3 37791 and eqvrelcoss4 37793 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels }
Theorem	dfcoeleqvrel 37795	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 37792, eqvrelcoss3 37791 and eqvrelcoss4 37793 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴)
21.24.13  Redundancy
Definition	df-redunds 37796*	Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 37799) is equivalent to satisfying the redundancy predicate (df-redund 37797). (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
Definition	df-redund 37797	Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 37799) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))
Definition	df-redundp 37798	Define the redundancy operator for propositions, cf. df-redund 37797. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))
Theorem	brredunds 37799	Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))))
Theorem	brredundsredund 37800	For sets, binary relation on the class of all redundant sets (brredunds 37799) is equivalent to satisfying the redundancy predicate (df-redund 37797). (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩))