P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	coss0 38601	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 38602	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I
Theorem	cosscnvid 38603	Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ≀ ◡ I = I
Theorem	trcoss 38604*	Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eleccossin 38605	Two ways of saying that the coset of 𝐴 and the coset of 𝐶 have the common element 𝐵. (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∈ ([𝐴] ≀ 𝑅 ∩ [𝐶] ≀ 𝑅) ↔ (𝐴 ≀ 𝑅𝐵 ∧ 𝐵 ≀ 𝑅𝐶)))
Theorem	trcoss2 38606*	Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.)
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	cosselrels 38607	Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )
Theorem	cnvelrels 38608	The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels )
Theorem	cosscnvelrels 38609	Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels )
21.26.7  Subset relations
Definition	df-ssr 38610*	Define the subsets class or the class of subset relations. Similar to definitions of epsilon relation (df-eprel 5519) and identity relation (df-id 5514) classes. Subset relation class and Scott Fenton's subset class df-sset 35919 are the same: S = SSet (compare dfssr2 38611 with df-sset 35919), the only reason we do not use dfssr2 38611 as the base definition of the subsets class is the way we defined the epsilon relation and the identity relation classes. The binary relation on the class of subsets and the subclass relationship (df-ss 3915) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 38613. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3915. The only exception (aside from directly investigating the class S e.g. in relssr 38612 or in extssr 38621) is when we have a specific purpose with its usage, like in case of df-refs 38622 versus df-cnvrefs 38637, where we need S to define the class of reflexive sets in order to be able to define the class of converse reflexive sets with the help of the converse of S. The subsets class S has another place in set.mm as well: if we define extensional relation based on the common property in extid 38368, extep 38341 and extssr 38621, then "extrelssr" " |- ExtRel S " is a theorem along with "extrelep" " |- ExtRel E " and "extrelid" " |- ExtRel I " . (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ S = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊆ 𝑦}
Theorem	dfssr2 38611	Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E )))
Theorem	relssr 38612	The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ Rel S
Theorem	brssr 38613	The subset relation and subclass relationship (df-ss 3915) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	brssrid 38614	Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴)
Theorem	issetssr 38615	Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴)
Theorem	brssrres 38616	Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	br1cnvssrres 38617	Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵)))
Theorem	brcnvssr 38618	The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	brcnvssrid 38619	Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.)
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴)
Theorem	br1cossxrncnvssrres 38620*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by range Cartesian product with restricted converse subsets class: a binary relation. (Contributed by Peter Mazsa, 9-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (◡ S ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝐶 ⊆ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐸 ⊆ 𝑢 ∧ 𝑢𝑅𝐷))))
Theorem	extssr 38621	Property of subset relation, see also extid 38368, extep 38341 and the comment of df-ssr 38610. (Contributed by Peter Mazsa, 10-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵))
21.26.8  Reflexivity
Definition	df-refs 38622	Define the class of all reflexive sets. It is used only by df-refrels 38623. We use subset relation S (df-ssr 38610) here to be able to define converse reflexivity (df-cnvrefs 38637), see also the comment of df-ssr 38610. The elements of this class are not necessarily relations (versus df-refrels 38623). Note the similarity of Definitions df-refs 38622, df-syms 38654 and df-trs 38688, cf. comments of dfrefrels2 38625. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-refrels 38623	Define the class of reflexive relations. This is practically dfrefrels2 38625 (which reveals that RefRels can not include proper classes like I as is elements, see comments of dfrefrels2 38625). Another alternative definition is dfrefrels3 38626. The element of this class and the reflexive relation predicate (df-refrel 38624) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 38632. This definition is similar to the definitions of the classes of symmetric (df-symrels 38655) and transitive (df-trrels 38689) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ RefRels = ( Refs ∩ Rels )
Definition	df-refrel 38624	Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 38628. Alternate definitions are dfrefrel2 38627 and dfrefrel3 38628. For sets, being an element of the class of reflexive relations (df-refrels 38623) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 38632. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfrefrels2 38625	Alternate definition of the class of reflexive relations. This is a 0-ary class constant, which is recommended for definitions (see the 1. Guideline at https://us.metamath.org/ileuni/mathbox.html). Proper classes (like I, see iprc 7847) are not elements of this (or any) class: if a class is an element of another class, it is not a proper class but a set, see elex 3458. So if we use 0-ary constant classes as our main definitions, they are valid only for sets, not for proper classes. For proper classes we use predicate-type definitions like df-refrel 38624. See also the comment of df-rels 38484. Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 38625, it keeps restriction of I: this is why the very similar definitions df-refs 38622, df-syms 38654 and df-trs 38688 diverge when we switch from (general) sets to relations in dfrefrels2 38625, dfsymrels2 38657 and dftrrels2 38691. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
Theorem	dfrefrels3 38626*	Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)}
Theorem	dfrefrel2 38627	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dfrefrel3 38628*	Alternate definition of the reflexive relation predicate. A relation is reflexive iff: for all elements on its domain and range, if an element of its domain is the same as an element of its range, then there is the relation between them. Note that this is definitely not the definition we are accustomed to, like e.g. idref 7085 / idrefALT 6064 or df-reflexive 49893 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 38682. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 38705, can we write the traditional form ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 for reflexive relations. For the special case with square Cartesian product when the two forms are equivalent see idinxpssinxp4 38378 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 38643. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))
Theorem	dfrefrel5 38629*	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅))
Theorem	elrefrels2 38630	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elrefrels3 38631*	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elrefrelsrel 38632	For sets, being an element of the class of reflexive relations (df-refrels 38623) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅))
Theorem	refreleq 38633	Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆))
Theorem	refrelid 38634	Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ RefRel I
Theorem	refrelcoss 38635	The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.)
⊢ RefRel ≀ 𝑅
Theorem	refrelressn 38636	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38564) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴}))
21.26.9  Converse reflexivity
Definition	df-cnvrefs 38637	Define the class of all converse reflexive sets, see the comment of df-ssr 38610. It is used only by df-cnvrefrels 38638. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-cnvrefrels 38638	Define the class of converse reflexive relations. This is practically dfcnvrefrels2 38640 (which uses the traditional subclass relation ⊆) : we use converse subset relation (brcnvssr 38618) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 23421), symmetric (df-syms 38654) and transitive (df-trs 38688) sets. We use this concept to define functions (df-funsALTV 38799, df-funALTV 38800) and disjoints (df-disjs 38822, df-disjALTV 38823). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38648. Alternate definitions are dfcnvrefrels2 38640 and dfcnvrefrels3 38641. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ CnvRefRels = ( CnvRefs ∩ Rels )
Definition	df-cnvrefrel 38639	Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38643. Alternate definitions are dfcnvrefrel2 38642 and dfcnvrefrel3 38643. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrels2 38640	Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))}
Theorem	dfcnvrefrels3 38641*	Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)}
Theorem	dfcnvrefrel2 38642	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrel3 38643*	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 38628. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	dfcnvrefrel4 38644	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfcnvrefrel5 38645*	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	elcnvrefrels2 38646	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrels3 38647*	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrelsrel 38648	For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 38638) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅))
Theorem	cnvrefrelcoss2 38649	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 38650	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 38651*	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 38652*	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 38653*	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.26.10  Symmetry
Definition	df-syms 38654	Define the class of all symmetric sets. It is used only by df-symrels 38655. Note the similarity of Definitions df-refs 38622, df-syms 38654 and df-trs 38688, cf. the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 38655	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 38673. Alternate definitions are dfsymrels2 38657, dfsymrels3 38658, dfsymrels4 38663 and dfsymrels5 38664. This definition is similar to the definitions of the classes of reflexive (df-refrels 38623) and transitive (df-trrels 38689) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 38656	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 38655) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 38673. Alternate definitions are dfsymrel2 38665 and dfsymrel3 38666. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfsymrels2 38657	Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
Theorem	dfsymrels3 38658*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)}
Theorem	elrelscnveq3 38659*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	elrelscnveq 38660	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	elrelscnveq2 38661*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	elrelscnveq4 38662*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	dfsymrels4 38663	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟}
Theorem	dfsymrels5 38664*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}
Theorem	dfsymrel2 38665	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 38666*	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 38667	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel5 38668*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	elsymrels2 38669	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels3 38670*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels4 38671	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels5 38672*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrelsrel 38673	For sets, being an element of the class of symmetric relations (df-symrels 38655) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅))
Theorem	symreleq 38674	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 38675	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 38676	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 38677	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 38678	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.26.11  Reflexivity and symmetry
Theorem	symrefref2 38679	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 38680. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 38680*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 38679. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 38681	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 38704) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38625, cf. the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
Theorem	refsymrels3 38682*	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 38705) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 38626, cf. the comment of dfrefrel3 38628. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))}
Theorem	refsymrel2 38683	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 38627, cf. the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	refsymrel3 38684*	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 38628, cf. the comment of dfrefrel3 38628. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅))
Theorem	elrefsymrels2 38685	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 38704) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 38625, cf. the comment of dfrefrels2 38625. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrels3 38686*	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 38705) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 38626, cf. the comment of dfrefrel3 38628. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrelsrel 38687	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.26.12  Transitivity
Definition	df-trs 38688	Define the class of all transitive sets (versus the transitive class defined in df-tr 5201). It is used only by df-trrels 38689. Note the similarity of the definitions of df-refs 38622, df-syms 38654 and df-trs 38688. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-trrels 38689	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 38697. Alternate definitions are dftrrels2 38691 and dftrrels3 38692. This definition is similar to the definitions of the classes of reflexive (df-refrels 38623) and symmetric (df-symrels 38655) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ TrRels = ( Trs ∩ Rels )
Definition	df-trrel 38690	Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 38689) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 38697. Alternate definitions are dftrrel2 38693 and dftrrel3 38694. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dftrrels2 38691	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 5628 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 38533 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 38692*	Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)}
Theorem	dftrrel2 38693	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dftrrel3 38694*	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅))
Theorem	eltrrels2 38695	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	eltrrels3 38696*	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels ))
Theorem	eltrrelsrel 38697	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 38698	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 38699	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38564) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.)
⊢ TrRel (𝑅 ↾ {𝐴})
21.26.13  Equivalence relations
Definition	df-eqvrels 38700	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 38710. Alternate definitions are dfeqvrels2 38704 and dfeqvrels3 38705. (Contributed by Peter Mazsa, 7-Nov-2018.)
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )