Home | Metamath
Proof Explorer Theorem List (p. 359 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dffunALTV2 35801 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 35827. (Contributed by Peter Mazsa, 8-Feb-2018.) |
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
Theorem | dffunALTV3 35802* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 35828. Reproduction of dffun2 6358. 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 35803* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 35829. This is dffun6 6363. 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 35804* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 35830. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) | ||
Theorem | elfunsALTV 35805 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV2 35806 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV3 35807* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV4 35808* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTV5 35809* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTVfunALTV 35810 | 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 35811 | Our definition of the function predicate df-funALTV 35795 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6350, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
Theorem | funALTVss 35812 | 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 35813 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Theorem | funALTVeqi 35814 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
Theorem | funALTVeqd 35815 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Definition | df-disjss 35816 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 35817). It is used only by df-disjs 35817. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
Definition | df-disjs 35817 |
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 35826).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 35840. Alternate definitions are dfdisjs 35821, ... , dfdisjs5 35825. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjs = ( Disjss ∩ Rels ) | ||
Definition | df-disjALTV 35818 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 35826,
see the comment of df-disjs 35817 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 35840. Alternate definitions are dfdisjALTV 35826, ... , dfdisjALTV5 35830. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
Definition | df-eldisjs 35819 | 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 35842. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
Definition | df-eldisj 35820 |
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 35842.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 35888 with dfeldisj5 35834. See also the comments of ~? dfmembpart2 and of ~? df-parts . (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
Theorem | dfdisjs 35821 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
Theorem | dfdisjs2 35822 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
Theorem | dfdisjs3 35823* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
Theorem | dfdisjs4 35824* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
Theorem | dfdisjs5 35825* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
Theorem | dfdisjALTV 35826 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 35817 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV2 35827 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 35801. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV3 35828* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 35802. (Contributed by Peter Mazsa, 28-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV4 35829* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 35803. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV5 35830* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 35804. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
Theorem | dfeldisj2 35831 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
Theorem | dfeldisj3 35832* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) | ||
Theorem | dfeldisj4 35833* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
Theorem | dfeldisj5 35834* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
Theorem | eldisjs 35835 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs2 35836 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs3 35837* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs4 35838* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs5 35839* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
Theorem | eldisjsdisj 35840 | 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 35841 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 35842 | 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 35843 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 35844 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 35845 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 35846 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 35847 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 35848 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 35849 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 35850 | Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 35851 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 35852 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 35853 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 35854 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 35855 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 35856 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjxrn 35857 | 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 35858 | 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 35859 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 35860 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 35861 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 35862 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 35863 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 35864 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 35865 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 35866 | 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 35867 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 35868 | 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 35869 | Lemma for prter3 35898. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | bicomdd 35870 | 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 35871 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jca3 35872 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
Theorem | prtlem70 35873 | Lemma for prter3 35898: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
Theorem | ibdr 35874 | Reverse of ibd 270. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | prtlem100 35875 | Lemma for prter3 35898. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | prtlem5 35876* | Lemma for prter1 35895, prter2 35897, prter3 35898 and prtex 35896. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
Theorem | prtlem80 35877 | Lemma for prter2 35897. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
Theorem | brabsb2 35878* | A closed form of brabsb 5409. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)) | ||
Theorem | eqbrrdv2 35879* | Other version of eqbrrdiv 5660. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | prtlem9 35880* | Lemma for prter3 35898. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
Theorem | prtlem10 35881* | Lemma for prter3 35898. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
Theorem | prtlem11 35882 | Lemma for prter2 35897. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
Theorem | prtlem12 35883* | Lemma for prtex 35896 and prter3 35898. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
Theorem | prtlem13 35884* | Lemma for prter1 35895, prter2 35897, prter3 35898 and prtex 35896. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
Theorem | prtlem16 35885* | Lemma for prtex 35896, prter2 35897 and prter3 35898. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
Theorem | prtlem400 35886* | Lemma for prter2 35897 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) | ||
Syntax | wprt 35887 | Extend the definition of a wff to include the partition predicate. |
wff Prt 𝐴 | ||
Definition | df-prt 35888* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | erprt 35889 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
Theorem | prtlem14 35890* | Lemma for prter1 35895, prter2 35897 and prtex 35896. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
Theorem | prtlem15 35891* | Lemma for prter1 35895 and prtex 35896. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
Theorem | prtlem17 35892* | Lemma for prter2 35897. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
Theorem | prtlem18 35893* | Lemma for prter2 35897. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
Theorem | prtlem19 35894* | Lemma for prter2 35897. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
Theorem | prter1 35895* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
Theorem | prtex 35896* | The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V)) | ||
Theorem | prter2 35897* | The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → (∪ 𝐴 / ∼ ) = (𝐴 ∖ {∅})) | ||
Theorem | prter3 35898* | For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ((𝑆 Er ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆) | ||
We are sad to report the passing of Metamath creator and long-time contributor Norm Megill (1950 - 2021). Norm of course was the author of the Metamath proof language, the specification, all of the early tools (and some of the later ones), and the foundational work in logic and set theory for set.mm. His tools, now at https://github.com/metamath/metamath-exe , include a proof verifier, a proof assistant, a proof minimizer, style checking and reformatting, and tools for searching and displaying proofs. One of his key insights was that formal proofs can exist not only to be verified by computers, but also to be read by humans. Both the specification of the proof format (which stores full proofs, as opposed to the proof templates used by most proof assistants) and the generated web display of Metamath proofs, one of its distinctive features, contribute to this double objective. Metamath innovated both by using a very simple substitution rule (and then using that to build more complicated notions like free and bound variables) and also by taking the axiom schemas found in many theories and taking them to the next level - by making all axioms, theorems and proofs operate in terms of schemas. Not content to create Metamath for his own amusement, he also published it for the world and encouraged the development of a community of people who contributed to it and created their own tools. He was an active participant in the Metamath mailing list and other forums until days before his passing. It is often our custom to supply a quote from someone memorialized in a mathbox entry. And it is difficult to select a quote for someone who has written so much about Metamath over the years. But here is one quote from the Metamath web page which illustrates not just his clear thinking about what Metamath can and cannot do but also his desire to encourage students at all levels: Q: Will Metamath help me learn abstract mathematics? A: Yes, but probably not by itself. In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. Some people find this frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math, in the same way it can be hard to grasp a large computer program just by reading its source code, even though you may understand each individual instruction. However, the Bibliographic Cross-Reference lets you compare informal proofs in math textbooks and see all the implicit missing details "left to the reader." | ||
These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2172, axc7 2327, axc10 2394, axc11 2444, axc11n 2440, axc15 2435, axc9 2391, axc14 2478, and axc16 2252. | ||
Axiom | ax-c5 35899 |
Axiom of Specialization. A quantified wff implies the wff without a
quantifier (i.e. an instance, or special case, of the generalized wff).
In other words if something is true for all 𝑥, it is true for any
specific 𝑥 (that would typically occur as a free
variable in the wff
substituted for 𝜑). (A free variable is one that does
not occur in
the scope of a quantifier: 𝑥 and 𝑦 are both free in 𝑥 = 𝑦,
but only 𝑥 is free in ∀𝑦𝑥 = 𝑦.) Axiom scheme C5' in [Megill]
p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski]
p. 67 (under his system S2, defined in the last paragraph on p. 77).
Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1787. Conditional forms of the converse are given by ax-13 2381, ax-c14 35907, ax-c16 35908, and ax-5 1902. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 2064. An interesting alternate axiomatization uses axc5c711 35934 and ax-c4 35900 in place of ax-c5 35899, ax-4 1801, ax-10 2136, and ax-11 2151. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 2172. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 35900 |
Axiom of Quantified Implication. This axiom moves a quantifier from
outside to inside an implication, quantifying 𝜓. Notice that 𝑥
must not be a free variable in the antecedent of the quantified
implication, and we express this by binding 𝜑 to "protect" the
axiom
from a 𝜑 containing a free 𝑥. Axiom
scheme C4' in [Megill]
p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of
[Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 2331. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |