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