Home | Metamath
Proof Explorer Theorem List (p. 369 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmcoss3 36801 | The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ dom ≀ 𝑅 = dom ◡𝑅 | ||
Theorem | dmcoss2 36802 | The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ dom ≀ 𝑅 = ran 𝑅 | ||
Theorem | rncossdmcoss 36803 | The range of cosets is the domain of them (this should be rncoss 5924 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.) |
⊢ ran ≀ 𝑅 = dom ≀ 𝑅 | ||
Theorem | dm1cosscnvepres 36804 | 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 36805 | 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 36806* | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | eldmcoss2 36807 | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴)) | ||
Theorem | eldm1cossres 36808* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵)) | ||
Theorem | eldm1cossres2 36809* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅)) | ||
Theorem | refrelcosslem 36810 | Lemma for the left side of the refrelcoss3 36811 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.) |
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥 | ||
Theorem | refrelcoss3 36811* | The class of cosets by 𝑅 is reflexive, see dfrefrel3 36864. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅) | ||
Theorem | refrelcoss2 36812 | The class of cosets by 𝑅 is reflexive, see dfrefrel2 36863. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss3 36813 | The class of cosets by 𝑅 is symmetric, see dfsymrel3 36898. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss2 36814 | The class of cosets by 𝑅 is symmetric, see dfsymrel2 36897. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | cossssid 36815 | 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 36816* | 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 36817* | 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 36818* | 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 36819* | 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 36820* | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
Theorem | brcosscnv2 36821 | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅)) | ||
Theorem | br1cosscnvxrn 36822 | 𝐴 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 36823 | Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵) | ||
Theorem | cosscnvssid3 36824* | 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 36825* | 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 36826* | 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 36827 | Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.) |
⊢ ≀ ∅ = ∅ | ||
Theorem | cossid 36828 | Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.) |
⊢ ≀ I = I | ||
Theorem | cosscnvid 36829 | Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ≀ ◡ I = I | ||
Theorem | trcoss 36830* | Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.) |
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eleccossin 36831 | 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 36832* | Equivalent expressions for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 16-Oct-2021.) |
⊢ (∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧) ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Definition | df-rels 36833 |
Define the relations class. Proper class relations (like I, see
reli 5779) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 36835).
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 36835. 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 36858), 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 36833 (see df-refrels 36859 and the resulting dfrefrels2 36861 and dfrefrels3 36862). 3. Finally, in order to be able to work with proper classes (like iprc 7841) as well, we define the predicate of the relation (see df-refrel 36860) so that it is true for the relevant proper classes (see refrelid 36870), and that the element of the class of the required relations (e.g. elrefrels3 36867) and this predicate are the same in case of sets (see elrefrelsrel 36868). (Contributed by Peter Mazsa, 13-Jun-2018.) |
⊢ Rels = 𝒫 (V × V) | ||
Theorem | elrels2 36834 | The element of the relations class (df-rels 36833) and the relation predicate (df-rel 5638) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V))) | ||
Theorem | elrelsrel 36835 | The element of the relations class (df-rels 36833) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅)) | ||
Theorem | elrelsrelim 36836 | The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ (𝑅 ∈ Rels → Rel 𝑅) | ||
Theorem | elrels5 36837 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅)) | ||
Theorem | elrels6 36838 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)) | ||
Theorem | elrelscnveq3 36839* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq 36840 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | elrelscnveq2 36841* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq4 36842* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | cnvelrels 36843 | The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels ) | ||
Theorem | cosselrels 36844 | Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels ) | ||
Theorem | cosscnvelrels 36845 | Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels ) | ||
Definition | df-ssr 36846* |
Define the subsets class or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5535) and identity relation
(df-id 5529) classes. Subset relation class and Scott
Fenton's subset
class df-sset 34327 are the same: S = SSet (compare dfssr2 36847 with
df-sset 34327), the only reason we do not use dfssr2 36847 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 3926) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 36849. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3926. The only exception (aside from directly investigating the class S e.g. in relssr 36848 or in extssr 36857) is when we have a specific purpose with its usage, like in case of df-refs 36858 versus df-cnvrefs 36873, 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 36657, extep 36629 and extssr 36857, 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 36847 | Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E ))) | ||
Theorem | relssr 36848 | The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ Rel S | ||
Theorem | brssr 36849 | The subset relation and subclass relationship (df-ss 3926) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | brssrid 36850 | Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴) | ||
Theorem | issetssr 36851 | Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴) | ||
Theorem | brssrres 36852 | Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
Theorem | br1cnvssrres 36853 | Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵))) | ||
Theorem | brcnvssr 36854 | The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
Theorem | brcnvssrid 36855 | Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴) | ||
Theorem | br1cossxrncnvssrres 36856* | ⟨𝐵, 𝐶⟩ 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 36857 | Property of subset relation, see also extid 36657, extep 36629 and the comment of df-ssr 36846. (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵)) | ||
Definition | df-refs 36858 |
Define the class of all reflexive sets. It is used only by df-refrels 36859.
We use subset relation S (df-ssr 36846) here to be able to define
converse reflexivity (df-cnvrefs 36873), see also the comment of df-ssr 36846.
The elements of this class are not necessarily relations (versus
df-refrels 36859).
Note the similarity of Definitions df-refs 36858, df-syms 36890 and df-trs 36920, cf. comments of dfrefrels2 36861. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-refrels 36859 |
Define the class of reflexive relations. This is practically dfrefrels2 36861
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 36861).
Another alternative definition is dfrefrels3 36862. The element of this class and the reflexive relation predicate (df-refrel 36860) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 36868. This definition is similar to the definitions of the classes of symmetric (df-symrels 36891) and transitive (df-trrels 36921) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ RefRels = ( Refs ∩ Rels ) | ||
Definition | df-refrel 36860 | Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 36864. Alternate definitions are dfrefrel2 36863 and dfrefrel3 36864. For sets, being an element of the class of reflexive relations (df-refrels 36859) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 36868. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfrefrels2 36861 |
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 7841)
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 3462. 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 36860. See
also the comment of df-rels 36833.
Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 36861, it keeps restriction of I: this is why the very similar definitions df-refs 36858, df-syms 36890 and df-trs 36920 diverge when we switch from (general) sets to relations in dfrefrels2 36861, dfsymrels2 36893 and dftrrels2 36923. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} | ||
Theorem | dfrefrels3 36862* | Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)} | ||
Theorem | dfrefrel2 36863 | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfrefrel3 36864* |
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 7087 / idrefALT 6062 or df-reflexive 46909 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 36914. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 36937, 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 36667 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 36879. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅)) | ||
Theorem | dfrefrel5 36865* | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.) |
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | elrefrels2 36866 | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrels3 36867* | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrelsrel 36868 | For sets, being an element of the class of reflexive relations (df-refrels 36859) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅)) | ||
Theorem | refreleq 36869 | Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆)) | ||
Theorem | refrelid 36870 | Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ RefRel I | ||
Theorem | refrelcoss 36871 | The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.) |
⊢ RefRel ≀ 𝑅 | ||
Theorem | refrelressn 36872 | Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 36790) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴})) | ||
Definition | df-cnvrefs 36873 | Define the class of all converse reflexive sets, see the comment of df-ssr 36846. It is used only by df-cnvrefrels 36874. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-cnvrefrels 36874 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 36876 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 36854) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 22778), symmetric (df-syms 36890) and transitive (df-trs 36920) sets.
We use this concept to define functions (df-funsALTV 37029, df-funALTV 37030) and disjoints (df-disjs 37052, df-disjALTV 37053). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 36884. Alternate definitions are dfcnvrefrels2 36876 and dfcnvrefrels3 36877. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
Definition | df-cnvrefrel 36875 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 36879. Alternate definitions are dfcnvrefrel2 36878 and dfcnvrefrel3 36879. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrels2 36876 | Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
Theorem | dfcnvrefrels3 36877* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
Theorem | dfcnvrefrel2 36878 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel3 36879* | 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 36864. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel4 36880 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel5 36881* | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | elcnvrefrels2 36882 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrels3 36883* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrelsrel 36884 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 36874) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
Theorem | cnvrefrelcoss2 36885 | 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 36886 | 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 36887* | 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 36888* | 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 36889* | 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 )) | ||
Definition | df-syms 36890 |
Define the class of all symmetric sets. It is used only by df-symrels 36891.
Note the similarity of Definitions df-refs 36858, df-syms 36890 and df-trs 36920, cf. the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-symrels 36891 |
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 36905. Alternate definitions are
dfsymrels2 36893, dfsymrels3 36894, dfsymrels4 36895 and dfsymrels5 36896.
This definition is similar to the definitions of the classes of reflexive (df-refrels 36859) and transitive (df-trrels 36921) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ SymRels = ( Syms ∩ Rels ) | ||
Definition | df-symrel 36892 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 36891) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 36905. Alternate definitions are dfsymrel2 36897 and dfsymrel3 36898. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfsymrels2 36893 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 36861. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
Theorem | dfsymrels3 36894* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
Theorem | dfsymrels4 36895 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
Theorem | dfsymrels5 36896* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
Theorem | dfsymrel2 36897 | 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 36898* | 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 36899 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfsymrel5 36900* | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |