P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xrneq12d 36501	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 36502*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 36503*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	xrninxp 36504*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 36505*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 36506	Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) ∈ V)
Theorem	inxpxrn 36507	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 36508*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 36509*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 36510*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 36511*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 36512*	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 36513*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 36514	Two ways to express restriction of range Cartesian product, see also xrnres2 36515, xrnres3 36516. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 36515	Two ways to express restriction of range Cartesian product, see also xrnres 36514, xrnres3 36516. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 36516	Two ways to express restriction of range Cartesian product, see also xrnres 36514, xrnres2 36515. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 36517	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 36518	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 36519	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 36520	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 36521	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 36522	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}}))
20.22.4  Cosets by ` R `
Definition	df-coss 36523*	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 36525 and the comment of dfec2 8489). 𝑅 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 ). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 36526) or to the range of a range Cartesian product of classes (cf. dfcoss4 36527), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 36525. Technically, we can define it via composition (dfcoss3 36526) or as the range of a range Cartesian product (dfcoss4 36527), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 36778, df-funALTV 36779) and disjoints (dfdisjs 36805, dfdisjs2 36806, df-disjALTV 36802, dfdisjALTV2 36811) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Definition	df-coels 36524	Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 36539. Possible definitions are the special cases of dfcoss3 36526 and dfcoss4 36527. (Contributed by Peter Mazsa, 20-Nov-2019.)
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)
Theorem	dfcoss2 36525*	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 8489). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)}
Theorem	dfcoss3 36526	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 36523). (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅)
Theorem	dfcoss4 36527	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 36523). (Contributed by Peter Mazsa, 12-Jul-2021.)
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅)
Theorem	cossex 36528	If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V)
Theorem	cosscnvex 36529	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 36530	Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V)
Theorem	1cossxrncnvepresex 36531	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 36532	Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ Rel ≀ 𝑅
Theorem	relcoels 36533	Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ Rel ∼ 𝐴
Theorem	cossss 36534	Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵)
Theorem	cosseq 36535	Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵)
Theorem	cosseqi 36536	Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ≀ 𝐴 = ≀ 𝐵
Theorem	cosseqd 36537	Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵)
Theorem	1cossres 36538*	The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ≀ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Theorem	dfcoels 36539*	Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ∼ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}
Theorem	brcoss 36540*	𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	brcoss2 36541*	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅)))
Theorem	brcoss3 36542	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅))
Theorem	brcosscnvcoss 36543	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 36544*	𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢)))
Theorem	cocossss 36545*	Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧))
Theorem	cnvcosseq 36546	The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ◡ ≀ 𝑅 = ≀ 𝑅
Theorem	br2coss 36547	Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅))
Theorem	br1cossres 36548*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶)))
Theorem	br1cossres2 36549*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅)))
Theorem	relbrcoss 36550*	𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅))))
Theorem	br1cossinres 36551*	𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnres 36552*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossinidres 36553*	𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossincnvepres 36554*	𝐵 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 36555*	⟨𝐵, 𝐶⟩ 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 36556*	⟨𝐵, 𝐶⟩ 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 36557	The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ dom ≀ 𝑅 = dom ◡𝑅
Theorem	dmcoss2 36558	The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ dom ≀ 𝑅 = ran 𝑅
Theorem	rncossdmcoss 36559	The range of cosets is the domain of them (this should be rncoss 5875 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.)
⊢ ran ≀ 𝑅 = dom ≀ 𝑅
Theorem	dm1cosscnvepres 36560	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 36561	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 36562*	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	eldmcoss2 36563	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴))
Theorem	eldm1cossres 36564*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵))
Theorem	eldm1cossres2 36565*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅))
Theorem	refrelcosslem 36566	Lemma for the left side of the refrelcoss3 36567 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.)
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥
Theorem	refrelcoss3 36567*	The class of cosets by 𝑅 is reflexive, see dfrefrel3 36620. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅)
Theorem	refrelcoss2 36568	The class of cosets by 𝑅 is reflexive, see dfrefrel2 36619. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	symrelcoss3 36569	The class of cosets by 𝑅 is symmetric, see dfsymrel3 36650. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅)
Theorem	symrelcoss2 36570	The class of cosets by 𝑅 is symmetric, see dfsymrel2 36649. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	cossssid 36571	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 36572*	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 36573*	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 36574*	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 36575*	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 36576*	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	brcosscnv2 36577	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅))
Theorem	br1cosscnvxrn 36578	𝐴 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 36579	Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵)
Theorem	cosscnvssid3 36580*	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 36581*	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 36582*	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 36583	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 36584	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I
Theorem	cosscnvid 36585	Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ≀ ◡ I = I
Theorem	trcoss 36586*	Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eleccossin 36587	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 36588*	Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.)
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
20.22.5  Relations
Definition	df-rels 36589	Define the relations class. Proper class relations (like I, see reli 5730) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 36591). 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 36591. 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 36614), 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 36589 (see df-refrels 36615 and the resulting dfrefrels2 36617 and dfrefrels3 36618). 3. Finally, in order to be able to work with proper classes (like iprc 7751) as well, we define the predicate of the relation (see df-refrel 36616) so that it is true for the relevant proper classes (see refrelid 36625), and that the element of the class of the required relations (e.g. elrefrels3 36622) and this predicate are the same in case of sets (see elrefrelsrel 36623). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 36590	The element of the relations class (df-rels 36589) and the relation predicate (df-rel 5592) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 36591	The element of the relations class (df-rels 36589) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 36592	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 36593	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 36594	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
Theorem	elrelscnveq3 36595*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	elrelscnveq 36596	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	elrelscnveq2 36597*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	elrelscnveq4 36598*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	cnvelrels 36599	The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels )
Theorem	cosselrels 36600	Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )