P. 385 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38401-38500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rnxrncnvepres 38401*	Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ (◡ E ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 𝑢 ∧ 𝑢𝑅𝑥)}
Theorem	rnxrnidres 38402*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 38403	Two ways to express restriction of range Cartesian product, see also xrnres2 38404, xrnres3 38405. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 38404	Two ways to express restriction of range Cartesian product, see also xrnres 38403, xrnres3 38405. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 38405	Two ways to express restriction of range Cartesian product, see also xrnres 38403, xrnres2 38404. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38406	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38407	Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 7-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ (𝑆 ↾ 𝐴) ∈ 𝑋) → (𝑅 ⋉ (𝑆 ↾ 𝐴)) ∈ V)
Theorem	xrnidresex 38408	Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ ( I ↾ 𝐴)) ∈ V)
Theorem	xrncnvepresex 38409	Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	brin2 38410	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐵⟩))
Theorem	brin3 38411	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}}))
21.26.4  Cosets by ` R `
Definition	df-coss 38412*	Define the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑢𝑅𝑥 and 𝑢𝑅𝑦 hold, i.e., both 𝑥 and 𝑦 are are elements of the 𝑅 -coset of 𝑢 (see dfcoss2 38414 and the comment of dfec2 8748). 𝑅 is usually a relation. This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to 𝑅, the right side relate to ≀ 𝑅 (see e.g. pet 38852). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38415) or to the range of a range Cartesian product of classes (cf. dfcoss4 38416), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38414. Technically, we can define it via composition (dfcoss3 38415) or as the range of a range Cartesian product (dfcoss4 38416), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 38682, df-funALTV 38683) and disjoints (dfdisjs 38709, dfdisjs2 38710, df-disjALTV 38706, dfdisjALTV2 38715) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Definition	df-coels 38413	Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38431. Possible definitions are the special cases of dfcoss3 38415 and dfcoss4 38416. (Contributed by Peter Mazsa, 20-Nov-2019.)
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)
Theorem	dfcoss2 38414*	Alternate definition of the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑥 and 𝑦 are are elements of the 𝑅-coset of 𝑢 (see also the comment of dfec2 8748). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)}
Theorem	dfcoss3 38415	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38412). (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅)
Theorem	dfcoss4 38416	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38412). (Contributed by Peter Mazsa, 12-Jul-2021.)
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅)
Theorem	cosscnv 38417*	Class of cosets by the converse of 𝑅 (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ ≀ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)}
Theorem	coss1cnvres 38418*	Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))}
Theorem	coss2cnvepres 38419*	Special case of coss1cnvres 38418. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(◡ E ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))}
Theorem	cossex 38420	If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V)
Theorem	cosscnvex 38421	If 𝐴 is a set then the class of cosets by the converse of 𝐴 is a set. (Contributed by Peter Mazsa, 18-Oct-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ V)
Theorem	1cosscnvepresex 38422	Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V)
Theorem	1cossxrncnvepresex 38423	Sufficient condition for a restricted converse epsilon range Cartesian product to be a set. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	relcoss 38424	Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ Rel ≀ 𝑅
Theorem	relcoels 38425	Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ Rel ∼ 𝐴
Theorem	cossss 38426	Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵)
Theorem	cosseq 38427	Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵)
Theorem	cosseqi 38428	Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ≀ 𝐴 = ≀ 𝐵
Theorem	cosseqd 38429	Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵)
Theorem	1cossres 38430*	The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ≀ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Theorem	dfcoels 38431*	Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ∼ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}
Theorem	brcoss 38432*	𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	brcoss2 38433*	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅)))
Theorem	brcoss3 38434	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅))
Theorem	brcosscnvcoss 38435	For sets, the 𝐴 and 𝐵 cosets by 𝑅 binary relation and the 𝐵 and 𝐴 cosets by 𝑅 binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ 𝐵 ≀ 𝑅𝐴))
Theorem	brcoels 38436*	𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢)))
Theorem	cocossss 38437*	Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧))
Theorem	cnvcosseq 38438	The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ◡ ≀ 𝑅 = ≀ 𝑅
Theorem	br2coss 38439	Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅))
Theorem	br1cossres 38440*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶)))
Theorem	br1cossres2 38441*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅)))
Theorem	brressn 38442	Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(𝑅 ↾ {𝐴})𝐶 ↔ (𝐵 = 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	ressn2 38443*	A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024.)
⊢ (𝑅 ↾ {𝐴}) = {⟨𝑎, 𝑢⟩ ∣ (𝑎 = 𝐴 ∧ 𝐴𝑅𝑢)}
Theorem	refressn 38444*	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38443) is reflexive, see also refrelressn 38525. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ (dom (𝑅 ↾ {𝐴}) ∩ ran (𝑅 ↾ {𝐴}))𝑥(𝑅 ↾ {𝐴})𝑥)
Theorem	antisymressn 38445	Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38443) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024.)
⊢ ∀𝑥∀𝑦((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑥) → 𝑥 = 𝑦)
Theorem	trressn 38446	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38443) is transitive, see also trrelressn 38584. (Contributed by Peter Mazsa, 16-Jun-2024.)
⊢ ∀𝑥∀𝑦∀𝑧((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑧) → 𝑥(𝑅 ↾ {𝐴})𝑧)
Theorem	relbrcoss 38447*	𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅))))
Theorem	br1cossinres 38448*	𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnres 38449*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossinidres 38450*	𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossincnvepres 38451*	𝐵 and 𝐶 are cosets by an intersection with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (◡ E ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝐵 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnidres 38452*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by a range Cartesian product with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ ( I ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossxrncnvepres 38453*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by a range Cartesian product with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 12-May-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐸 ∈ 𝑢 ∧ 𝑢𝑅𝐷))))
Theorem	dmcoss3 38454	The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ dom ≀ 𝑅 = dom ◡𝑅
Theorem	dmcoss2 38455	The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ dom ≀ 𝑅 = ran 𝑅
Theorem	rncossdmcoss 38456	The range of cosets is the domain of them (this should be rncoss 5986 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.)
⊢ ran ≀ 𝑅 = dom ≀ 𝑅
Theorem	dm1cosscnvepres 38457	The domain of cosets of the restricted converse epsilon relation is the union of the restriction. (Contributed by Peter Mazsa, 18-May-2019.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ dom ≀ (◡ E ↾ 𝐴) = ∪ 𝐴
Theorem	dmcoels 38458	The domain of coelements in 𝐴 is the union of 𝐴. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Peter Mazsa, 5-Apr-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ dom ∼ 𝐴 = ∪ 𝐴
Theorem	eldmcoss 38459*	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	eldmcoss2 38460	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴))
Theorem	eldm1cossres 38461*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵))
Theorem	eldm1cossres2 38462*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅))
Theorem	refrelcosslem 38463	Lemma for the left side of the refrelcoss3 38464 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.)
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥
Theorem	refrelcoss3 38464*	The class of cosets by 𝑅 is reflexive, see dfrefrel3 38517. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅)
Theorem	refrelcoss2 38465	The class of cosets by 𝑅 is reflexive, see dfrefrel2 38516. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	symrelcoss3 38466	The class of cosets by 𝑅 is symmetric, see dfsymrel3 38551. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅)
Theorem	symrelcoss2 38467	The class of cosets by 𝑅 is symmetric, see dfsymrel2 38550. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	cossssid 38468	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 38469*	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 38470*	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 38471*	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 38472*	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 38473*	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	brcosscnv2 38474	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅))
Theorem	br1cosscnvxrn 38475	𝐴 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 38476	Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵)
Theorem	cosscnvssid3 38477*	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 38478*	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 38479*	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 38480	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 38481	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I
Theorem	cosscnvid 38482	Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ≀ ◡ I = I
Theorem	trcoss 38483*	Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eleccossin 38484	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 38485*	Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.)
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
21.26.5  Relations
Definition	df-rels 38486	Define the relations class. Proper class relations (like I, see reli 5836) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 38488). 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 38488. 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 38511), 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 38486 (see df-refrels 38512 and the resulting dfrefrels2 38514 and dfrefrels3 38515). 3. Finally, in order to be able to work with proper classes (like iprc 7933) as well, we define the predicate of the relation (see df-refrel 38513) so that it is true for the relevant proper classes (see refrelid 38523), and that the element of the class of the required relations (e.g. elrefrels3 38520) and this predicate are the same in case of sets (see elrefrelsrel 38521). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 38487	The element of the relations class (df-rels 38486) and the relation predicate (df-rel 5692) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 38488	The element of the relations class (df-rels 38486) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 38489	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 38490	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 38491	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
Theorem	elrelscnveq3 38492*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	elrelscnveq 38493	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	elrelscnveq2 38494*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	elrelscnveq4 38495*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	cnvelrels 38496	The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels )
Theorem	cosselrels 38497	Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )
Theorem	cosscnvelrels 38498	Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels )
21.26.6  Subset relations
Definition	df-ssr 38499*	Define the subsets class or the class of subset relations. Similar to definitions of epsilon relation (df-eprel 5584) and identity relation (df-id 5578) classes. Subset relation class and Scott Fenton's subset class df-sset 35857 are the same: S = SSet (compare dfssr2 38500 with df-sset 35857), the only reason we do not use dfssr2 38500 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 3968) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 38502. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3968. The only exception (aside from directly investigating the class S e.g. in relssr 38501 or in extssr 38510) is when we have a specific purpose with its usage, like in case of df-refs 38511 versus df-cnvrefs 38526, 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 38311, extep 38284 and extssr 38510, 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 38500	Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E )))