P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	symrelcoss2 37001	The class of cosets by 𝑅 is symmetric, see dfsymrel2 37084. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	cossssid 37002	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)))
Theorem	cossssid2 37003*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥∀𝑦(∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦))
Theorem	cossssid3 37004*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∀𝑥∀𝑦((𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦))
Theorem	cossssid4 37005*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∃*𝑥 𝑢𝑅𝑥)
Theorem	cossssid5 37006*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥 ∈ ran 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 ∨ ([𝑥]◡𝑅 ∩ [𝑦]◡𝑅) = ∅))
Theorem	brcosscnv 37007*	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	brcosscnv2 37008	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅))
Theorem	br1cosscnvxrn 37009	𝐴 and 𝐵 are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡(𝑅 ⋉ 𝑆)𝐵 ↔ (𝐴 ≀ ◡𝑅𝐵 ∧ 𝐴 ≀ ◡𝑆𝐵)))
Theorem	1cosscnvxrn 37010	Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵)
Theorem	cosscnvssid3 37011*	Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣))
Theorem	cosscnvssid4 37012*	Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥)
Theorem	cosscnvssid5 37013*	Equivalent expressions for the class of cosets by the converse of the relation 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅) ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	coss0 37014	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 37015	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I
Theorem	cosscnvid 37016	Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ≀ ◡ I = I
Theorem	trcoss 37017*	Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eleccossin 37018	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 37019*	Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.)
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
21.22.5  Relations
Definition	df-rels 37020	Define the relations class. Proper class relations (like I, see reli 5787) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 37022). The class of relations is a great tool we can use when we define classes of different relations as nullary class constants as required by the 2. point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 37022. When we want to define a specific class of relations as a nullary class constant, the appropriate method is the following: 1. We define the specific nullary class constant for general sets (see e.g. df-refs 37045), then 2. we get the required class of relations by the intersection of the class of general sets above with the class of relations df-rels 37020 (see df-refrels 37046 and the resulting dfrefrels2 37048 and dfrefrels3 37049). 3. Finally, in order to be able to work with proper classes (like iprc 7855) as well, we define the predicate of the relation (see df-refrel 37047) so that it is true for the relevant proper classes (see refrelid 37057), and that the element of the class of the required relations (e.g. elrefrels3 37054) and this predicate are the same in case of sets (see elrefrelsrel 37055). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 37021	The element of the relations class (df-rels 37020) and the relation predicate (df-rel 5645) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 37022	The element of the relations class (df-rels 37020) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 37023	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 37024	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 37025	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
Theorem	elrelscnveq3 37026*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	elrelscnveq 37027	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	elrelscnveq2 37028*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	elrelscnveq4 37029*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	cnvelrels 37030	The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels )
Theorem	cosselrels 37031	Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )
Theorem	cosscnvelrels 37032	Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels )
21.22.6  Subset relations
Definition	df-ssr 37033*	Define the subsets class or the class of subset relations. Similar to definitions of epsilon relation (df-eprel 5542) and identity relation (df-id 5536) classes. Subset relation class and Scott Fenton's subset class df-sset 34517 are the same: S = SSet (compare dfssr2 37034 with df-sset 34517), the only reason we do not use dfssr2 37034 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 3930) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 37036. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3930. The only exception (aside from directly investigating the class S e.g. in relssr 37035 or in extssr 37044) is when we have a specific purpose with its usage, like in case of df-refs 37045 versus df-cnvrefs 37060, 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 36844, extep 36816 and extssr 37044, 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 37034	Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E )))
Theorem	relssr 37035	The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ Rel S
Theorem	brssr 37036	The subset relation and subclass relationship (df-ss 3930) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	brssrid 37037	Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴)
Theorem	issetssr 37038	Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴)
Theorem	brssrres 37039	Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	br1cnvssrres 37040	Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵)))
Theorem	brcnvssr 37041	The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	brcnvssrid 37042	Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.)
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴)
Theorem	br1cossxrncnvssrres 37043*	⟨𝐵, 𝐶⟩ 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 37044	Property of subset relation, see also extid 36844, extep 36816 and the comment of df-ssr 37033. (Contributed by Peter Mazsa, 10-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵))
21.22.7  Reflexivity
Definition	df-refs 37045	Define the class of all reflexive sets. It is used only by df-refrels 37046. We use subset relation S (df-ssr 37033) here to be able to define converse reflexivity (df-cnvrefs 37060), see also the comment of df-ssr 37033. The elements of this class are not necessarily relations (versus df-refrels 37046). Note the similarity of Definitions df-refs 37045, df-syms 37077 and df-trs 37107, cf. comments of dfrefrels2 37048. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-refrels 37046	Define the class of reflexive relations. This is practically dfrefrels2 37048 (which reveals that RefRels can not include proper classes like I as is elements, see comments of dfrefrels2 37048). Another alternative definition is dfrefrels3 37049. The element of this class and the reflexive relation predicate (df-refrel 37047) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 37055. This definition is similar to the definitions of the classes of symmetric (df-symrels 37078) and transitive (df-trrels 37108) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ RefRels = ( Refs ∩ Rels )
Definition	df-refrel 37047	Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 37051. Alternate definitions are dfrefrel2 37050 and dfrefrel3 37051. For sets, being an element of the class of reflexive relations (df-refrels 37046) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 37055. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfrefrels2 37048	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 7855) 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 3464. 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 37047. See also the comment of df-rels 37020. Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 37048, it keeps restriction of I: this is why the very similar definitions df-refs 37045, df-syms 37077 and df-trs 37107 diverge when we switch from (general) sets to relations in dfrefrels2 37048, dfsymrels2 37080 and dftrrels2 37110. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
Theorem	dfrefrels3 37049*	Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)}
Theorem	dfrefrel2 37050	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dfrefrel3 37051*	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 7097 / idrefALT 6070 or df-reflexive 47333 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 37101. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 37124, 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 36854 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 37066. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))
Theorem	dfrefrel5 37052*	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅))
Theorem	elrefrels2 37053	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elrefrels3 37054*	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elrefrelsrel 37055	For sets, being an element of the class of reflexive relations (df-refrels 37046) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅))
Theorem	refreleq 37056	Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆))
Theorem	refrelid 37057	Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ RefRel I
Theorem	refrelcoss 37058	The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.)
⊢ RefRel ≀ 𝑅
Theorem	refrelressn 37059	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 36977) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴}))
21.22.8  Converse reflexivity
Definition	df-cnvrefs 37060	Define the class of all converse reflexive sets, see the comment of df-ssr 37033. It is used only by df-cnvrefrels 37061. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-cnvrefrels 37061	Define the class of converse reflexive relations. This is practically dfcnvrefrels2 37063 (which uses the traditional subclass relation ⊆) : we use converse subset relation (brcnvssr 37041) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 22893), symmetric (df-syms 37077) and transitive (df-trs 37107) sets. We use this concept to define functions (df-funsALTV 37216, df-funALTV 37217) and disjoints (df-disjs 37239, df-disjALTV 37240). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 37071. Alternate definitions are dfcnvrefrels2 37063 and dfcnvrefrels3 37064. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ CnvRefRels = ( CnvRefs ∩ Rels )
Definition	df-cnvrefrel 37062	Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 37066. Alternate definitions are dfcnvrefrel2 37065 and dfcnvrefrel3 37066. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrels2 37063	Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 37048. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))}
Theorem	dfcnvrefrels3 37064*	Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)}
Theorem	dfcnvrefrel2 37065	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrel3 37066*	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 37051. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	dfcnvrefrel4 37067	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfcnvrefrel5 37068*	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	elcnvrefrels2 37069	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrels3 37070*	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrelsrel 37071	For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 37061) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅))
Theorem	cnvrefrelcoss2 37072	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 37073	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 37074*	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 37075*	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 37076*	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.22.9  Symmetry
Definition	df-syms 37077	Define the class of all symmetric sets. It is used only by df-symrels 37078. Note the similarity of Definitions df-refs 37045, df-syms 37077 and df-trs 37107, cf. the comment of dfrefrels2 37048. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 37078	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 37092. Alternate definitions are dfsymrels2 37080, dfsymrels3 37081, dfsymrels4 37082 and dfsymrels5 37083. This definition is similar to the definitions of the classes of reflexive (df-refrels 37046) and transitive (df-trrels 37108) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 37079	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 37078) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 37092. Alternate definitions are dfsymrel2 37084 and dfsymrel3 37085. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfsymrels2 37080	Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 37048. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
Theorem	dfsymrels3 37081*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)}
Theorem	dfsymrels4 37082	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟}
Theorem	dfsymrels5 37083*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}
Theorem	dfsymrel2 37084	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 37085*	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 37086	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel5 37087*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	elsymrels2 37088	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels3 37089*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels4 37090	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels5 37091*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrelsrel 37092	For sets, being an element of the class of symmetric relations (df-symrels 37078) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅))
Theorem	symreleq 37093	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 37094	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 37095	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 37096	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 37097	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.22.10  Reflexivity and symmetry
Theorem	symrefref2 37098	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 37099. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 37099*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 37098. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 37100	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 37123) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 37048, cf. the comment of dfrefrels2 37048. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}