Home | Metamath
Proof Explorer Theorem List (p. 360 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfmember2 35901 | Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ ( MembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | dfmember3 35902 | Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
⊢ ( MembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | eqvreldmqs 35903 | Two ways to express membership equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | brerser 35904 | Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴)) | ||
Theorem | erim2 35905 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 36012 in a more convenient form , see also erim 35906). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅)) | ||
Theorem | erim 35906 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 36012 and erim2 35905). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅)) | ||
Definition | df-funss 35907 | Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 35908). It is used only by df-funsALTV 35908. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels } | ||
Definition | df-funsALTV 35908 | Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 35910, ... , dffunsALTV5 35914. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ FunsALTV = ( Funss ∩ Rels ) | ||
Definition | df-funALTV 35909 |
Define the function relation predicate, i.e., the function predicate.
This definition of the function predicate (based on a more general,
converse reflexive, relation) and the original definition of function in
set.mm df-fun 6351, are always the same, that is
( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 35925.
The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 35924. Alternate definitions are dffunALTV2 35915, ... , dffunALTV5 35918. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹)) | ||
Theorem | dffunsALTV 35910 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels } | ||
Theorem | dffunsALTV2 35911 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I } | ||
Theorem | dffunsALTV3 35912* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 )}. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∀𝑥∀𝑦((𝑢𝑓𝑥 ∧ 𝑢𝑓𝑦) → 𝑥 = 𝑦)} | ||
Theorem | dffunsALTV4 35913* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀𝑥1∃*𝑦1𝑥1𝑓𝑦1}. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∃*𝑥 𝑢𝑓𝑥} | ||
Theorem | dffunsALTV5 35914* | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)} | ||
Theorem | dffunALTV2 35915 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 35941. (Contributed by Peter Mazsa, 8-Feb-2018.) |
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
Theorem | dffunALTV3 35916* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 35942. Reproduction of dffun2 6359. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 ) ∧ Rel 𝐹). (Contributed by NM, 29-Dec-1996.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ Rel 𝐹)) | ||
Theorem | dffunALTV4 35917* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 35943. This is dffun6 6364. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀𝑥1∃*𝑦1𝑥1𝐹𝑦1 ∧ Rel 𝐹). (Contributed by NM, 9-Mar-1995.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ Rel 𝐹)) | ||
Theorem | dffunALTV5 35918* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 35944. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) | ||
Theorem | elfunsALTV 35919 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV2 35920 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV3 35921* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV4 35922* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV5 35923* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTVfunALTV 35924 | The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹)) | ||
Theorem | funALTVfun 35925 | Our definition of the function predicate df-funALTV 35909 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6351, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
Theorem | funALTVss 35926 | Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴)) | ||
Theorem | funALTVeq 35927 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Theorem | funALTVeqi 35928 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
Theorem | funALTVeqd 35929 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Definition | df-disjss 35930 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 35931). It is used only by df-disjs 35931. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
Definition | df-disjs 35931 |
Define the disjoint relations class, i.e., the class of disjoints. We
need Disjs for the definition of Parts and Part
for the
Partition-Equivalence Theorems: this need for Parts as disjoint relations
on their domain quotients is the reason why we must define Disjs
instead of simply using converse functions (cf. dfdisjALTV 35940).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 35954. Alternate definitions are dfdisjs 35935, ... , dfdisjs5 35939. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjs = ( Disjss ∩ Rels ) | ||
Definition | df-disjALTV 35932 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 35940,
see the comment of df-disjs 35931 why we need disjoint relations instead of
converse functions anyway.
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 35954. Alternate definitions are dfdisjALTV 35940, ... , dfdisjALTV5 35944. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
Definition | df-eldisjs 35933 | Define the disjoint elementhood relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 35956. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
Definition | df-eldisj 35934 |
Define the disjoint elementhood relation predicate, i.e., the disjoint
elementhood predicate. Read: the elements of 𝐴 are disjoint. The
element of the disjoint elements class and the disjoint elementhood
predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when
𝐴 is a set, see eleldisjseldisj 35956.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 36002 with dfeldisj5 35948. See also the comments of ~? dfmembpart2 and of ~? df-parts . (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
Theorem | dfdisjs 35935 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
Theorem | dfdisjs2 35936 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
Theorem | dfdisjs3 35937* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
Theorem | dfdisjs4 35938* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
Theorem | dfdisjs5 35939* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
Theorem | dfdisjALTV 35940 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 35931 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV2 35941 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 35915. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV3 35942* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 35916. (Contributed by Peter Mazsa, 28-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV4 35943* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 35917. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV5 35944* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 35918. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
Theorem | dfeldisj2 35945 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
Theorem | dfeldisj3 35946* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) | ||
Theorem | dfeldisj4 35947* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
Theorem | dfeldisj5 35948* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
Theorem | eldisjs 35949 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs2 35950 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs3 35951* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs4 35952* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs5 35953* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
Theorem | eldisjsdisj 35954 | The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅)) | ||
Theorem | eleldisjs 35955 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 35956 | The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴)) | ||
Theorem | disjrel 35957 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 35958 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 35959 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 35960 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 35961 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 35962 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 35963 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 35964 | Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 35965 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 35966 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 35967 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 35968 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 35969 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 35970 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjxrn 35971 | Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ( Disj (𝑅 ⋉ 𝑆) ↔ ( ≀ ◡𝑅 ∩ ≀ ◡𝑆) ⊆ I ) | ||
Theorem | disjorimxrn 35972 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (( Disj 𝑅 ∨ Disj 𝑆) → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimxrn 35973 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 35974 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 35975 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 35976 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 35977 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 35978 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 35979 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 35980 | The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ( I ↾ 𝐴) | ||
Theorem | disjALTVinidres 35981 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 35982 | The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj (𝑅 ⋉ ( I ↾ 𝐴)) | ||
Theorem | prtlem60 35983 | Lemma for prter3 36012. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | bicomdd 35984 | Commute two sides of a biconditional in a deduction. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜒))) | ||
Theorem | jca2r 35985 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jca3 35986 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
Theorem | prtlem70 35987 | Lemma for prter3 36012: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
Theorem | ibdr 35988 | Reverse of ibd 271. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | prtlem100 35989 | Lemma for prter3 36012. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | prtlem5 35990* | Lemma for prter1 36009, prter2 36011, prter3 36012 and prtex 36010. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
Theorem | prtlem80 35991 | Lemma for prter2 36011. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
Theorem | brabsb2 35992* | A closed form of brabsb 5410. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)) | ||
Theorem | eqbrrdv2 35993* | Other version of eqbrrdiv 5661. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | prtlem9 35994* | Lemma for prter3 36012. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
Theorem | prtlem10 35995* | Lemma for prter3 36012. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
Theorem | prtlem11 35996 | Lemma for prter2 36011. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
Theorem | prtlem12 35997* | Lemma for prtex 36010 and prter3 36012. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
Theorem | prtlem13 35998* | Lemma for prter1 36009, prter2 36011, prter3 36012 and prtex 36010. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
Theorem | prtlem16 35999* | Lemma for prtex 36010, prter2 36011 and prter3 36012. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
Theorem | prtlem400 36000* | Lemma for prter2 36011 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |