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	trressn 38401	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38398) is transitive, see also trrelressn 38539. (Contributed by Peter Mazsa, 16-Jun-2024.)
⊢ ∀𝑥∀𝑦∀𝑧((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑧) → 𝑥(𝑅 ↾ {𝐴})𝑧)
Theorem	relbrcoss 38402*	𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅))))
Theorem	br1cossinres 38403*	𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnres 38404*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossinidres 38405*	𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossincnvepres 38406*	𝐵 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 38407*	⟨𝐵, 𝐶⟩ 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 38408*	⟨𝐵, 𝐶⟩ 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 38409	The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ dom ≀ 𝑅 = dom ◡𝑅
Theorem	dmcoss2 38410	The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ dom ≀ 𝑅 = ran 𝑅
Theorem	rncossdmcoss 38411	The range of cosets is the domain of them (this should be rncoss 5998 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.)
⊢ ran ≀ 𝑅 = dom ≀ 𝑅
Theorem	dm1cosscnvepres 38412	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 38413	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 38414*	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	eldmcoss2 38415	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴))
Theorem	eldm1cossres 38416*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵))
Theorem	eldm1cossres2 38417*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅))
Theorem	refrelcosslem 38418	Lemma for the left side of the refrelcoss3 38419 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.)
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥
Theorem	refrelcoss3 38419*	The class of cosets by 𝑅 is reflexive, see dfrefrel3 38472. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅)
Theorem	refrelcoss2 38420	The class of cosets by 𝑅 is reflexive, see dfrefrel2 38471. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	symrelcoss3 38421	The class of cosets by 𝑅 is symmetric, see dfsymrel3 38506. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅)
Theorem	symrelcoss2 38422	The class of cosets by 𝑅 is symmetric, see dfsymrel2 38505. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	cossssid 38423	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 38424*	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 38425*	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 38426*	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 38427*	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 38428*	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	brcosscnv2 38429	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅))
Theorem	br1cosscnvxrn 38430	𝐴 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 38431	Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵)
Theorem	cosscnvssid3 38432*	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 38433*	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 38434*	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 38435	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 38436	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I
Theorem	cosscnvid 38437	Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ≀ ◡ I = I
Theorem	trcoss 38438*	Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.)
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eleccossin 38439	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 38440*	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 38441	Define the relations class. Proper class relations (like I, see reli 5850) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 38443). 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 38443. 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 38466), 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 38441 (see df-refrels 38467 and the resulting dfrefrels2 38469 and dfrefrels3 38470). 3. Finally, in order to be able to work with proper classes (like iprc 7951) as well, we define the predicate of the relation (see df-refrel 38468) so that it is true for the relevant proper classes (see refrelid 38478), and that the element of the class of the required relations (e.g. elrefrels3 38475) and this predicate are the same in case of sets (see elrefrelsrel 38476). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 38442	The element of the relations class (df-rels 38441) and the relation predicate (df-rel 5707) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 38443	The element of the relations class (df-rels 38441) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 38444	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 38445	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 38446	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
Theorem	elrelscnveq3 38447*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
Theorem	elrelscnveq 38448	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅))
Theorem	elrelscnveq2 38449*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	elrelscnveq4 38450*	Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))
Theorem	cnvelrels 38451	The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels )
Theorem	cosselrels 38452	Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )
Theorem	cosscnvelrels 38453	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 38454*	Define the subsets class or the class of subset relations. Similar to definitions of epsilon relation (df-eprel 5599) and identity relation (df-id 5593) classes. Subset relation class and Scott Fenton's subset class df-sset 35820 are the same: S = SSet (compare dfssr2 38455 with df-sset 35820), the only reason we do not use dfssr2 38455 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 3993) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 38457. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3993. The only exception (aside from directly investigating the class S e.g. in relssr 38456 or in extssr 38465) is when we have a specific purpose with its usage, like in case of df-refs 38466 versus df-cnvrefs 38481, 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 38266, extep 38239 and extssr 38465, 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 38455	Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E )))
Theorem	relssr 38456	The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ Rel S
Theorem	brssr 38457	The subset relation and subclass relationship (df-ss 3993) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	brssrid 38458	Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴)
Theorem	issetssr 38459	Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴)
Theorem	brssrres 38460	Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	br1cnvssrres 38461	Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵)))
Theorem	brcnvssr 38462	The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	brcnvssrid 38463	Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.)
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴)
Theorem	br1cossxrncnvssrres 38464*	⟨𝐵, 𝐶⟩ 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 38465	Property of subset relation, see also extid 38266, extep 38239 and the comment of df-ssr 38454. (Contributed by Peter Mazsa, 10-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵))
21.26.7  Reflexivity
Definition	df-refs 38466	Define the class of all reflexive sets. It is used only by df-refrels 38467. We use subset relation S (df-ssr 38454) here to be able to define converse reflexivity (df-cnvrefs 38481), see also the comment of df-ssr 38454. The elements of this class are not necessarily relations (versus df-refrels 38467). Note the similarity of Definitions df-refs 38466, df-syms 38498 and df-trs 38528, cf. comments of dfrefrels2 38469. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-refrels 38467	Define the class of reflexive relations. This is practically dfrefrels2 38469 (which reveals that RefRels can not include proper classes like I as is elements, see comments of dfrefrels2 38469). Another alternative definition is dfrefrels3 38470. The element of this class and the reflexive relation predicate (df-refrel 38468) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 38476. This definition is similar to the definitions of the classes of symmetric (df-symrels 38499) and transitive (df-trrels 38529) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ RefRels = ( Refs ∩ Rels )
Definition	df-refrel 38468	Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 38472. Alternate definitions are dfrefrel2 38471 and dfrefrel3 38472. For sets, being an element of the class of reflexive relations (df-refrels 38467) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 38476. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfrefrels2 38469	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 7951) 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 3509. 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 38468. See also the comment of df-rels 38441. Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 38469, it keeps restriction of I: this is why the very similar definitions df-refs 38466, df-syms 38498 and df-trs 38528 diverge when we switch from (general) sets to relations in dfrefrels2 38469, dfsymrels2 38501 and dftrrels2 38531. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
Theorem	dfrefrels3 38470*	Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)}
Theorem	dfrefrel2 38471	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dfrefrel3 38472*	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 7180 / idrefALT 6143 or df-reflexive 48860 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 38522. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 38545, 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 38276 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 38487. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))
Theorem	dfrefrel5 38473*	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅))
Theorem	elrefrels2 38474	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elrefrels3 38475*	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elrefrelsrel 38476	For sets, being an element of the class of reflexive relations (df-refrels 38467) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅))
Theorem	refreleq 38477	Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆))
Theorem	refrelid 38478	Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ RefRel I
Theorem	refrelcoss 38479	The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.)
⊢ RefRel ≀ 𝑅
Theorem	refrelressn 38480	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38398) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴}))
21.26.8  Converse reflexivity
Definition	df-cnvrefs 38481	Define the class of all converse reflexive sets, see the comment of df-ssr 38454. It is used only by df-cnvrefrels 38482. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-cnvrefrels 38482	Define the class of converse reflexive relations. This is practically dfcnvrefrels2 38484 (which uses the traditional subclass relation ⊆) : we use converse subset relation (brcnvssr 38462) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 23534), symmetric (df-syms 38498) and transitive (df-trs 38528) sets. We use this concept to define functions (df-funsALTV 38637, df-funALTV 38638) and disjoints (df-disjs 38660, df-disjALTV 38661). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38492. Alternate definitions are dfcnvrefrels2 38484 and dfcnvrefrels3 38485. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ CnvRefRels = ( CnvRefs ∩ Rels )
Definition	df-cnvrefrel 38483	Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38487. Alternate definitions are dfcnvrefrel2 38486 and dfcnvrefrel3 38487. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrels2 38484	Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 38469. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))}
Theorem	dfcnvrefrels3 38485*	Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)}
Theorem	dfcnvrefrel2 38486	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrel3 38487*	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 38472. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	dfcnvrefrel4 38488	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfcnvrefrel5 38489*	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	elcnvrefrels2 38490	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrels3 38491*	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrelsrel 38492	For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 38482) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅))
Theorem	cnvrefrelcoss2 38493	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 38494	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 38495*	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 38496*	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 38497*	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.9  Symmetry
Definition	df-syms 38498	Define the class of all symmetric sets. It is used only by df-symrels 38499. Note the similarity of Definitions df-refs 38466, df-syms 38498 and df-trs 38528, cf. the comment of dfrefrels2 38469. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 38499	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 38513. Alternate definitions are dfsymrels2 38501, dfsymrels3 38502, dfsymrels4 38503 and dfsymrels5 38504. This definition is similar to the definitions of the classes of reflexive (df-refrels 38467) and transitive (df-trrels 38529) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 38500	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 38499) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 38513. Alternate definitions are dfsymrel2 38505 and dfsymrel3 38506. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))