Home | Metamath
Proof Explorer Theorem List (p. 358 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | relbrcoss 35701* | 𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅)))) | ||
Theorem | br1cossinres 35702* | 𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossxrnres 35703* | 〈𝐵, 𝐶〉 and 〈𝐷, 𝐸〉 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (〈𝐵, 𝐶〉 ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))〈𝐷, 𝐸〉 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷)))) | ||
Theorem | br1cossinidres 35704* | 𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶)))) | ||
Theorem | br1cossincnvepres 35705* | 𝐵 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 35706* | 〈𝐵, 𝐶〉 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 35707* | 〈𝐵, 𝐶〉 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 35708 | The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.) |
⊢ dom ≀ 𝑅 = dom ◡𝑅 | ||
Theorem | dmcoss2 35709 | The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ dom ≀ 𝑅 = ran 𝑅 | ||
Theorem | rncossdmcoss 35710 | The range of cosets is the domain of them (this should be rncoss 5843 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.) |
⊢ ran ≀ 𝑅 = dom ≀ 𝑅 | ||
Theorem | dm1cosscnvepres 35711 | 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 35712 | 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 35713* | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴)) | ||
Theorem | eldmcoss2 35714 | Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴)) | ||
Theorem | eldm1cossres 35715* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵)) | ||
Theorem | eldm1cossres2 35716* | Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅)) | ||
Theorem | refrelcosslem 35717 | Lemma for the left side of the refrelcoss3 35718 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.) |
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥 | ||
Theorem | refrelcoss3 35718* | The class of cosets by 𝑅 is reflexive, see dfrefrel3 35771. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅) | ||
Theorem | refrelcoss2 35719 | The class of cosets by 𝑅 is reflexive, see dfrefrel2 35770. (Contributed by Peter Mazsa, 30-Jul-2019.) |
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss3 35720 | The class of cosets by 𝑅 is symmetric, see dfsymrel3 35801. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅) | ||
Theorem | symrelcoss2 35721 | The class of cosets by 𝑅 is symmetric, see dfsymrel2 35800. (Contributed by Peter Mazsa, 27-Dec-2018.) |
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅) | ||
Theorem | cossssid 35722 | 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 35723* | 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 35724* | 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 35725* | 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 35726* | 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 35727* | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | ||
Theorem | brcosscnv2 35728 | 𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅)) | ||
Theorem | br1cosscnvxrn 35729 | 𝐴 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 35730 | Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵) | ||
Theorem | cosscnvssid3 35731* | 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 35732* | 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 35733* | 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 35734 | Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.) |
⊢ ≀ ∅ = ∅ | ||
Theorem | cossid 35735 | Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.) |
⊢ ≀ I = I | ||
Theorem | cosscnvid 35736 | Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ≀ ◡ I = I | ||
Theorem | trcoss 35737* | Sufficient condition for the transitivity of cosets by 𝑅. (Contributed by Peter Mazsa, 26-Dec-2018.) |
⊢ (∀𝑦∃*𝑢 𝑢𝑅𝑦 → ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eleccossin 35738 | 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 35739* | 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 35740 |
Define the relations class. Proper class relations (like I, see
reli 5698) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 35742).
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 35742. 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 35765), 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 35740 (see df-refrels 35766 and the resulting dfrefrels2 35768 and dfrefrels3 35769). 3. Finally, in order to be able to work with proper classes (like iprc 7618) as well, we define the predicate of the relation (see df-refrel 35767) so that it is true for the relevant proper classes (see refrelid 35776), and that the element of the class of the required relations (e.g. elrefrels3 35773) and this predicate are the same in case of sets (see elrefrelsrel 35774). (Contributed by Peter Mazsa, 13-Jun-2018.) |
⊢ Rels = 𝒫 (V × V) | ||
Theorem | elrels2 35741 | The element of the relations class (df-rels 35740) and the relation predicate (df-rel 5562) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V))) | ||
Theorem | elrelsrel 35742 | The element of the relations class (df-rels 35740) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅)) | ||
Theorem | elrelsrelim 35743 | The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ (𝑅 ∈ Rels → Rel 𝑅) | ||
Theorem | elrels5 35744 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅)) | ||
Theorem | elrels6 35745 | Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅)) | ||
Theorem | elrelscnveq3 35746* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq 35747 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | elrelscnveq2 35748* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | elrelscnveq4 35749* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021.) |
⊢ (𝑅 ∈ Rels → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | cnvelrels 35750 | The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ Rels ) | ||
Theorem | cosselrels 35751 | Cosets of sets are elements of the relations class. Implies ⊢ (𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels ). (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels ) | ||
Theorem | cosscnvelrels 35752 | Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ Rels ) | ||
Definition | df-ssr 35753* |
Define the subsets class or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5465) and identity relation
(df-id 5460) classes. Subset relation class and Scott
Fenton's subset
class df-sset 33317 are the same: S = SSet (compare dfssr2 35754 with
df-sset 33317), the only reason we do not use dfssr2 35754 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 3952) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 35756. Yet in general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for sets, see the comment of df-ss 3952. The only exception (aside from directly investigating the class S e.g. in relssr 35755 or in extssr 35764) is when we have a specific purpose with its usage, like in case of df-refs 35765 versus df-cnvrefs 35778, 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 35583, extep 35555 and extssr 35764, 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 35754 | Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ S = ((V × V) ∖ ran ( E ⋉ (V ∖ E ))) | ||
Theorem | relssr 35755 | The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ Rel S | ||
Theorem | brssr 35756 | The subset relation and subclass relationship (df-ss 3952) are the same, that is, (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set. (Contributed by Peter Mazsa, 31-Jul-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | brssrid 35757 | Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 S 𝐴) | ||
Theorem | issetssr 35758 | Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ V ↔ 𝐴 S 𝐴) | ||
Theorem | brssrres 35759 | Restricted subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵( S ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶))) | ||
Theorem | br1cnvssrres 35760 | Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵◡( S ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐵))) | ||
Theorem | brcnvssr 35761 | The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
Theorem | brcnvssrid 35762 | Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴◡ S 𝐴) | ||
Theorem | br1cossxrncnvssrres 35763* | 〈𝐵, 𝐶〉 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 35764 | Property of subset relation, see also extid 35583, extep 35555 and the comment of df-ssr 35753. (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ S = [𝐵]◡ S ↔ 𝐴 = 𝐵)) | ||
Definition | df-refs 35765 |
Define the class of all reflexive sets. It is used only by df-refrels 35766.
We use subset relation S (df-ssr 35753) here to be able to define
converse reflexivity (df-cnvrefs 35778), see also the comment of df-ssr 35753.
The elements of this class are not necessarily relations (versus
df-refrels 35766).
Note the similarity of the definitions df-refs 35765, df-syms 35793 and df-trs 35823, cf. comments of dfrefrels2 35768. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-refrels 35766 |
Define the class of reflexive relations. This is practically dfrefrels2 35768
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 35768).
Another alternative definition is dfrefrels3 35769. The element of this class and the reflexive relation predicate (df-refrel 35767) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 35774. This definition is similar to the definitions of the classes of symmetric (df-symrels 35794) and transitive (df-trrels 35824) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ RefRels = ( Refs ∩ Rels ) | ||
Definition | df-refrel 35767 | Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 35771. Alternate definitions are dfrefrel2 35770 and dfrefrel3 35771. For sets, being an element of the class of reflexive relations (df-refrels 35766) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 35774. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfrefrels2 35768 |
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 7618)
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 3512. 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 35767. See
also the comment of df-rels 35740.
Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 35768, it keeps restriction of I: this is why the very similar definitions df-refs 35765, df-syms 35793 and df-trs 35823 diverge when we switch from (general) sets to relations in dfrefrels2 35768, dfsymrels2 35796 and dftrrels2 35826. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟} | ||
Theorem | dfrefrels3 35769* | Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)} | ||
Theorem | dfrefrel2 35770 | Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfrefrel3 35771* |
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 6908 / idrefALT 5973 or df-reflexive 44887 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 35817. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 35839, 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 35592 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 35784. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅)) | ||
Theorem | elrefrels2 35772 | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrels3 35773* | Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.) |
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elrefrelsrel 35774 | For sets, being an element of the class of reflexive relations (df-refrels 35766) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅)) | ||
Theorem | refreleq 35775 | Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆)) | ||
Theorem | refrelid 35776 | Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ RefRel I | ||
Theorem | refrelcoss 35777 | The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.) |
⊢ RefRel ≀ 𝑅 | ||
Definition | df-cnvrefs 35778 | Define the class of all converse reflexive sets, see the comment of df-ssr 35753. It is used only by df-cnvrefrels 35779. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-cnvrefrels 35779 |
Define the class of converse reflexive relations. This is practically
dfcnvrefrels2 35781 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 35761) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 22113), symmetric (df-syms 35793) and transitive (df-trs 35823) sets.
We use this concept to define functions (df-funsALTV 35929, df-funALTV 35930) and disjoints (df-disjs 35952, df-disjALTV 35953). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 35787. Alternate definitions are dfcnvrefrels2 35781 and dfcnvrefrels3 35782. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) | ||
Definition | df-cnvrefrel 35780 | Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 35784. Alternate definitions are dfcnvrefrel2 35783 and dfcnvrefrel3 35784. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrels2 35781 | Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 35768. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))} | ||
Theorem | dfcnvrefrels3 35782* | Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.) |
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)} | ||
Theorem | dfcnvrefrel2 35783 | Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.) |
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfcnvrefrel3 35784* | 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 35771. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | elcnvrefrels2 35785 | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrels3 35786* | Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels )) | ||
Theorem | elcnvrefrelsrel 35787 | For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 35779) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅)) | ||
Theorem | cnvrefrelcoss2 35788 | 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 35789 | 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 35790* | 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 35791* | 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 35792* | 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 35793 |
Define the class of all symmetric sets. It is used only by df-symrels 35794.
Note the similarity of the definitions df-refs 35765, df-syms 35793 and df-trs 35823, cf. the comment of dfrefrels2 35768. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} | ||
Definition | df-symrels 35794 |
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 35808. Alternate definitions are
dfsymrels2 35796, dfsymrels3 35797, dfsymrels4 35798 and dfsymrels5 35799.
This definition is similar to the definitions of the classes of reflexive (df-refrels 35766) and transitive (df-trrels 35824) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
⊢ SymRels = ( Syms ∩ Rels ) | ||
Definition | df-symrel 35795 | Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 35794) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 35808. Alternate definitions are dfsymrel2 35800 and dfsymrel3 35801. (Contributed by Peter Mazsa, 16-Jul-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) | ||
Theorem | dfsymrels2 35796 | Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 35768. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟} | ||
Theorem | dfsymrels3 35797* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)} | ||
Theorem | dfsymrels4 35798 | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟} | ||
Theorem | dfsymrels5 35799* | Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.) |
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | ||
Theorem | dfsymrel2 35800 | Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019.) (Revised by Peter Mazsa, 17-Aug-2021.) |
⊢ ( SymRel 𝑅 ↔ (◡𝑅 ⊆ 𝑅 ∧ Rel 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |