| Metamath
Proof Explorer Theorem List (p. 389 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | disjlem18 38801* | Lemma for disjdmqseq 38806, partim2 38808 and petlem 38813 via disjlem19 38802, (general version of the former prtlem18 38878). (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵)))) | ||
| Theorem | disjlem19 38802* | Lemma for disjdmqseq 38806, partim2 38808 and petlem 38813 via disjdmqs 38805, (general version of the former prtlem19 38879). (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅))) | ||
| Theorem | disjdmqsss 38803 | Lemma for disjdmqseq 38806 via disjdmqs 38805. (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅)) | ||
| Theorem | disjdmqscossss 38804 | Lemma for disjdmqseq 38806 via disjdmqs 38805. (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅)) | ||
| Theorem | disjdmqs 38805 | If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38808 and petlem 38813 via disjdmqseq 38806. (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅)) | ||
| Theorem | disjdmqseq 38806 | If a relation is disjoint, its domain quotient is equal to a class if and only if the domain quotient of the cosets by it is equal to the class. General version of eldisjn0el 38807 (which is the closest theorem to the former prter2 38882). Lemma for partim2 38808 and petlem 38813. (Contributed by Peter Mazsa, 16-Sep-2021.) |
| ⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
| Theorem | eldisjn0el 38807 | Special case of disjdmqseq 38806 (perhaps this is the closest theorem to the former prter2 38882). (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | partim2 38808 | Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 38809. Lemma for petlem 38813. (Contributed by Peter Mazsa, 17-Sep-2021.) |
| ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
| Theorem | partim 38809 | Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 38808. (Contributed by Peter Mazsa, 17-Sep-2021.) |
| ⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴) | ||
| Theorem | partimeq 38810 | Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38680. (Contributed by Peter Mazsa, 25-Dec-2024.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅)) | ||
| Theorem | eldisjlem19 38811* | Special case of disjlem19 38802 (together with membpartlem19 38812, this is former prtlem19 38879). (Contributed by Peter Mazsa, 21-Oct-2021.) |
| ⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
| Theorem | membpartlem19 38812* | Together with disjlem19 38802, this is former prtlem19 38879. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.) |
| ⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
| Theorem | petlem 38813 | If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38834), or converse function (cf. dfdisjALTV 38714), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38851. (Contributed by Peter Mazsa, 18-Sep-2021.) |
| ⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅) ⇒ ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
| Theorem | petlemi 38814 | If you can prove disjointness (e.g. disjALTV0 38755, disjALTVid 38756, disjALTVidres 38757, disjALTVxrnidres 38759, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38714), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. (Contributed by Peter Mazsa, 18-Sep-2021.) |
| ⊢ Disj 𝑅 ⇒ ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
| Theorem | pet02 38815 | Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj ∅ ∧ (dom ∅ / ∅) = 𝐴) ↔ ( EqvRel ≀ ∅ ∧ (dom ≀ ∅ / ≀ ∅) = 𝐴)) | ||
| Theorem | pet0 38816 | Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (∅ Part 𝐴 ↔ ≀ ∅ ErALTV 𝐴) | ||
| Theorem | petid2 38817 | Class 𝐴 is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj I ∧ (dom I / I ) = 𝐴) ↔ ( EqvRel ≀ I ∧ (dom ≀ I / ≀ I ) = 𝐴)) | ||
| Theorem | petid 38818 | A class is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ( I Part 𝐴 ↔ ≀ I ErALTV 𝐴) | ||
| Theorem | petidres2 38819 | Class 𝐴 is a partition by the identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj ( I ↾ 𝐴) ∧ (dom ( I ↾ 𝐴) / ( I ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ≀ ( I ↾ 𝐴) ∧ (dom ≀ ( I ↾ 𝐴) / ≀ ( I ↾ 𝐴)) = 𝐴)) | ||
| Theorem | petidres 38820 | A class is a partition by identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it, cf. eqvrel1cossidres 38791. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴) | ||
| Theorem | petinidres2 38821 | Class 𝐴 is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom (𝑅 ∩ ( I ↾ 𝐴)) / (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ∩ ( I ↾ 𝐴)) / ≀ (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴)) | ||
| Theorem | petinidres 38822 | A class is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. Cf. br1cossinidres 38450, disjALTVinidres 38758 and eqvrel1cossinidres 38792. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
| Theorem | petxrnidres2 38823 | Class 𝐴 is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom (𝑅 ⋉ ( I ↾ 𝐴)) / (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ ( I ↾ 𝐴)) / ≀ (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴)) | ||
| Theorem | petxrnidres 38824 | A class is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. Cf. br1cossxrnidres 38452, disjALTVxrnidres 38759 and eqvrel1cossxrnidres 38793. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
| Theorem | eqvreldisj1 38825* | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 38826, eqvreldisj3 38827). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.) |
| ⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
| Theorem | eqvreldisj2 38826 | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 38827). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅)) | ||
| Theorem | eqvreldisj3 38827 | The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8835). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 20-Jun-2019.) (Revised by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( EqvRel 𝑅 → Disj (◡ E ↾ (𝐴 / 𝑅))) | ||
| Theorem | eqvreldisj4 38828 | Intersection with the converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ( EqvRel 𝑅 → Disj (𝑆 ∩ (◡ E ↾ (𝐵 / 𝑅)))) | ||
| Theorem | eqvreldisj5 38829 | Range Cartesian product with converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
| ⊢ ( EqvRel 𝑅 → Disj (𝑆 ⋉ (◡ E ↾ (𝐵 / 𝑅)))) | ||
| Theorem | eqvrelqseqdisj2 38830 | Implication of eqvreldisj2 38826, lemma for The Main Theorem of Equivalences mainer 38835. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴) | ||
| Theorem | fences3 38831 | Implication of eqvrelqseqdisj2 38830 and n0eldmqseq 38650, see comment of fences 38845. (Contributed by Peter Mazsa, 30-Dec-2024.) |
| ⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
| Theorem | eqvrelqseqdisj3 38832 | Implication of eqvreldisj3 38827, lemma for the Member Partition Equivalence Theorem mpet3 38837. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.) |
| ⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴)) | ||
| Theorem | eqvrelqseqdisj4 38833 | Lemma for petincnvepres2 38849. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴))) | ||
| Theorem | eqvrelqseqdisj5 38834 | Lemma for the Partition-Equivalence Theorem pet2 38851. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
| ⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴))) | ||
| Theorem | mainer 38835 | The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴) | ||
| Theorem | partimcomember 38836 | Partition with general 𝑅 (in addition to the member partition cf. mpet 38840 and mpet2 38841) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.) |
| ⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴) | ||
| Theorem | mpet3 38837 | Member Partition-Equivalence Theorem. Together with mpet 38840 mpet2 38841, mostly in its conventional cpet 38839 and cpet2 38838 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38851 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
| ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | cpet2 38838 | The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet 38839. Together with cpet 38839, mpet 38840 mpet2 38841, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38851 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.) |
| ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | cpet 38839 | The conventional form of Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have been calling disjoint or partition what we call element disjoint or member partition, see also cpet2 38838. Cf. mpet 38840, mpet2 38841 and mpet3 38837 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38852 and pet2 38851 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.) |
| ⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | mpet 38840 | Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 38843. Member partition and comember equivalence relation are the same (or: each element of 𝐴 have equivalent comembers if and only if 𝐴 is a member partition). Together with mpet2 38841, mpet3 38837, and with the conventional cpet 38839 and cpet2 38838, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38851 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.) |
| ⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴) | ||
| Theorem | mpet2 38841 | Member Partition-Equivalence Theorem in a shorter form. Together with mpet 38840 mpet3 38837, mostly in its conventional cpet 38839 and cpet2 38838 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38851 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.) |
| ⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴) | ||
| Theorem | mpets2 38842 | Member Partition-Equivalence Theorem with binary relations, cf. mpet2 38841. (Contributed by Peter Mazsa, 24-Sep-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴)) | ||
| Theorem | mpets 38843 | Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 38852, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.) |
| ⊢ MembParts = CoMembErs | ||
| Theorem | mainpart 38844 | Partition with general 𝑅 also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.) |
| ⊢ (𝑅 Part 𝐴 → MembPart 𝐴) | ||
| Theorem | fences 38845 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 38840) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴) | ||
| Theorem | fences2 38846 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 38837) generate a partition of the members, it alo means that (𝑅 ErALTV 𝐴 → ElDisj 𝐴) and that (𝑅 ErALTV 𝐴 → ¬ ∅ ∈ 𝐴). (Contributed by Peter Mazsa, 15-Oct-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
| Theorem | mainer2 38847 | The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
| Theorem | mainerim 38848 | Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴) | ||
| Theorem | petincnvepres2 38849 | A partition-equivalence theorem with intersection and general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ (( Disj (𝑅 ∩ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ∩ (◡ E ↾ 𝐴)) / (𝑅 ∩ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) / ≀ (𝑅 ∩ (◡ E ↾ 𝐴))) = 𝐴)) | ||
| Theorem | petincnvepres 38850 | The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 38451. Cf. pet 38852. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴) | ||
| Theorem | pet2 38851 | Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 38852 and pets 38853) is the main result of my investigation into set theory, see the comment of pet 38852. (Contributed by Peter Mazsa, 24-May-2021.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴)) | ||
| Theorem | pet 38852 |
Partition-Equivalence Theorem with general 𝑅 while preserving the
restricted converse epsilon relation of mpet2 38841 (as opposed to
petincnvepres 38850). A class is a partition by a range
Cartesian product
with general 𝑅 and the restricted converse element
class if and only
if the cosets by the range Cartesian product are in an equivalence
relation on it. Cf. br1cossxrncnvepres 38453.
This theorem (together with pets 38853 and pet2 38851) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 38840, mpet2 38841 and mpet3 38837 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 38841), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 38841 lacks: 𝑅, which is sufficient for my future application of set theory, for my purpose outside of set theory. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴) | ||
| Theorem | pets 38853 | Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 38852 and pet2 38851) is the main result of my investigation into set theory, cf. the comment of pet 38852. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴)) | ||
| Theorem | prtlem60 38854 | Lemma for prter3 38883. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
| Theorem | bicomdd 38855 | 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 38856 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
| Theorem | jca3 38857 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
| Theorem | prtlem70 38858 | Lemma for prter3 38883: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
| ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
| Theorem | ibdr 38859 | Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
| ⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
| Theorem | prtlem100 38860 | Lemma for prter3 38883. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
| ⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
| Theorem | prtlem5 38861* | Lemma for prter1 38880, prter2 38882, prter3 38883 and prtex 38881. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
| ⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
| Theorem | prtlem80 38862 | Lemma for prter2 38882. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
| ⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
| Theorem | brabsb2 38863* | A closed form of brabsb 5536. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
| Theorem | eqbrrdv2 38864* | Other version of eqbrrdiv 5804. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
| ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
| Theorem | prtlem9 38865* | Lemma for prter3 38883. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
| ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
| Theorem | prtlem10 38866* | Lemma for prter3 38883. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
| Theorem | prtlem11 38867 | Lemma for prter2 38882. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
| ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
| Theorem | prtlem12 38868* | Lemma for prtex 38881 and prter3 38883. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ ( ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
| Theorem | prtlem13 38869* | Lemma for prter1 38880, prter2 38882, prter3 38883 and prtex 38881. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
| Theorem | prtlem16 38870* | Lemma for prtex 38881, prter2 38882 and prter3 38883. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
| Theorem | prtlem400 38871* | Lemma for prter2 38882 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) | ||
| Syntax | wprt 38872 | Extend the definition of a wff to include the partition predicate. |
| wff Prt 𝐴 | ||
| Definition | df-prt 38873* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
| Theorem | erprt 38874 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
| Theorem | prtlem14 38875* | Lemma for prter1 38880, prter2 38882 and prtex 38881. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
| Theorem | prtlem15 38876* | Lemma for prter1 38880 and prtex 38881. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
| ⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
| Theorem | prtlem17 38877* | Lemma for prter2 38882. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
| ⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
| Theorem | prtlem18 38878* | Lemma for prter2 38882. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
| Theorem | prtlem19 38879* | Lemma for prter2 38882. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
| Theorem | prter1 38880* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
| Theorem | prtex 38881* | 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 38882* | 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 38883* | 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 2183, axc7 2317, axc10 2390, axc11 2435, axc11n 2431, axc15 2427, axc9 2387, axc14 2468, and axc16 2261. | ||
| Axiom | ax-c5 38884 |
Axiom of Specialization. A universally quantified wff implies the wff
without the universal quantifier (i.e., an instance, or special case, of
the generalized wff). In other words, if something is true for all
𝑥, then 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 1795. Conditional forms of the converse are given by ax-13 2377, ax-c14 38892, ax-c16 38893, and ax-5 1910. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. In our axiomatization, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution (see stdpc4 2068). An interesting alternate axiomatization uses axc5c711 38919 and ax-c4 38885 in place of ax-c5 38884, ax-4 1809, ax-10 2141, and ax-11 2157. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2183. (Contributed by NM, 3-Jan-1993.) Use sp 2183 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Axiom | ax-c4 38885 |
Axiom of Quantified Implication. This axiom moves a universal 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 2321. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
| ⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
| Axiom | ax-c7 38886 |
Axiom of Quantified Negation. This axiom is used to manipulate negated
quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of
the preprint). An alternate axiomatization could use axc5c711 38919 in place
of ax-c5 38884, ax-c7 38886, and ax-11 2157.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2317. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
| Axiom | ax-c10 38887 |
A variant of ax6 2389. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the
preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc10 2390. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
| Axiom | ax-c11 38888 |
Axiom ax-c11 38888 was the original version of ax-c11n 38889 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 38889 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11 2435. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
| Axiom | ax-c11n 38889 |
Axiom of Quantifier Substitution. One of the equality and substitution
axioms of predicate calculus with equality. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
The original version of this axiom was ax-c11 38888 and was replaced with this shorter ax-c11n 38889 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2435. Conversely, this axiom is proved from ax-c11 38888 as Theorem axc11nfromc11 38927. This axiom was proved redundant in July 2015. See Theorem axc11n 2431. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2431. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
| Axiom | ax-c15 38890 |
Axiom ax-c15 38890 was the original version of ax-12 2177, before it was
discovered (in Jan. 2007) that the shorter ax-12 2177 could replace it. It
appears as Axiom scheme C15' in [Megill]
p. 448 (p. 16 of the preprint).
It is based on Lemma 16 of [Tarski] p. 70
and Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases. To understand this theorem more
easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning
"if
𝑥 and 𝑦 are distinct variables
then..." The antecedent becomes
false if the same variable is substituted for 𝑥 and 𝑦,
ensuring
the theorem is sound whenever this is the case. In some later theorems,
we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor".
Interestingly, if the wff expression substituted for 𝜑 contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of Axiom ax-c15 38890 (from which the ax-12 2177 instance follows by Theorem ax12 2428.) The proof is by induction on formula length, using ax12eq 38942 and ax12el 38943 for the basis steps and ax12indn 38944, ax12indi 38945, and ax12inda 38949 for the induction steps. (This paragraph is true provided we use ax-c11 38888 in place of ax-c11n 38889.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2427, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
| Axiom | ax-c9 38891 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever 𝑧 is distinct from 𝑥 and
𝑦,
and 𝑥 =
𝑦 is true,
then 𝑥 = 𝑦 quantified with 𝑧 is also
true. In other words, 𝑧
is irrelevant to the truth of 𝑥 = 𝑦. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc9 2387. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
| Axiom | ax-c14 38892 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-5 1910; see Theorem axc14 2468. Alternately,
ax-5 1910 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1910.
We retain ax-c14 38892 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1910, which might be easier to study for some
theoretical
purposes.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc14 2468. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
| ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
| Axiom | ax-c16 38893* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1910
to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory (see dtru 5441), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1910; see Theorem axc16 2261. Alternately, ax-5 1910 becomes logically redundant in the presence of this axiom, but without ax-5 1910 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 38893 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1910, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc16 2261. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorems ax12fromc15 38906 and ax13fromc9 38907 require some intermediate theorems that are included in this section. | ||
| Theorem | axc5 38894 | This theorem repeats sp 2183 under the name axc5 38894, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 38884. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2183 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | ax4fromc4 38895 | Rederivation of Axiom ax-4 1809 from ax-c4 38885, ax-c5 38884, ax-gen 1795 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2321 for the derivation of ax-c4 38885 from ax-4 1809. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1809 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
| Theorem | ax10fromc7 38896 | Rederivation of Axiom ax-10 2141 from ax-c7 38886, ax-c4 38885, ax-c5 38884, ax-gen 1795 and propositional calculus. See axc7 2317 for the derivation of ax-c7 38886 from ax-10 2141. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2141 instead. (New usage is discouraged.) |
| ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
| Theorem | ax6fromc10 38897 | Rederivation of Axiom ax-6 1967 from ax-c7 38886, ax-c10 38887, ax-gen 1795 and propositional calculus. See axc10 2390 for the derivation of ax-c10 38887 from ax-6 1967. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1967 instead. (New usage is discouraged.) |
| ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
| Theorem | hba1-o 38898 | The setvar 𝑥 is not free in ∀𝑥𝜑. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
| Theorem | axc4i-o 38899 | Inference version of ax-c4 38885. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
| Theorem | equid1 38900 | Proof of equid 2011 from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 1910; see the proof of equid 2011. See equid1ALT 38926 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑥 = 𝑥 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |