| Metamath
Proof Explorer Theorem List (p. 370 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 | ||
Some useful theorems for dealing with substitutions: sbbi 2308, sbcbig 3840, sbcel1g 4416, sbcel2 4418, sbcel12 4411, sbceqg 4412, csbvarg 4434. | ||
| Theorem | bj-sbeqALT 36901* | Substitution in an equality (use the more general version bj-sbeq 36902 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
| Theorem | bj-sbeq 36902 | Distribute proper substitution through an equality relation. (See sbceqg 4412). (Contributed by BJ, 6-Oct-2018.) |
| ⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
| Theorem | bj-sbceqgALT 36903 | Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4412. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4412, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
| Theorem | bj-csbsnlem 36904* | Lemma for bj-csbsn 36905 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
| ⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
| Theorem | bj-csbsn 36905 | Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
| Theorem | bj-sbel1 36906* | Version of sbcel1g 4416 when substituting a set. (Note: one could have a corresponding version of sbcel12 4411 when substituting a set, but the point here is that the antecedent of sbcel1g 4416 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.) |
| ⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵) | ||
| Theorem | bj-abv 36907 | The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
| Theorem | bj-abvALT 36908 | Alternate version of bj-abv 36907; shorter but uses ax-8 2110. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
| Theorem | bj-ab0 36909 | The class of sets verifying a falsity is the empty set (closed form of abf 4406). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅) | ||
| Theorem | bj-abf 36910 | Shorter proof of abf 4406 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
| Theorem | bj-csbprc 36911 | More direct proof of csbprc 4409 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
| ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
| Theorem | bj-exlimvmpi 36912* | A Fol lemma (exlimiv 1930 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
| ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
| Theorem | bj-exlimmpi 36913 | Lemma for bj-vtoclg1f1 36918 (an instance of this lemma is a version of bj-vtoclg1f1 36918 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
| Theorem | bj-exlimmpbi 36914 | Lemma for theorems of the vtoclg 3554 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
| Theorem | bj-exlimmpbir 36915 | Lemma for theorems of the vtoclg 3554 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (∃𝑥𝜒 → 𝜑) | ||
| Theorem | bj-vtoclf 36916* | Remove dependency on ax-ext 2708, df-clab 2715 and df-cleq 2729 (and df-sb 2065 and df-v 3482) from vtoclf 3564. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
| Theorem | bj-vtocl 36917* | Remove dependency on ax-ext 2708, df-clab 2715 and df-cleq 2729 (and df-sb 2065 and df-v 3482) from vtocl 3558. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
| Theorem | bj-vtoclg1f1 36918* | The FOL content of vtoclg1f 3570 (hence not using ax-ext 2708, df-cleq 2729, df-nfc 2892, df-v 3482). Note the weakened "major" hypothesis and the disjoint variable condition between 𝑥 and 𝐴 (needed since the nonfreeness quantifier for classes is not available without ax-ext 2708; as a byproduct, this dispenses with ax-11 2157 and ax-13 2377). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓) | ||
| Theorem | bj-vtoclg1f 36919* | Reprove vtoclg1f 3570 from bj-vtoclg1f1 36918. This removes dependency on ax-ext 2708, df-cleq 2729 and df-v 3482. Use bj-vtoclg1fv 36920 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
| Theorem | bj-vtoclg1fv 36920* | Version of bj-vtoclg1f 36919 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2065 and df-clab 2715. Prefer its use over bj-vtoclg1f 36919 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
| Theorem | bj-vtoclg 36921* | A version of vtoclg 3554 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2715, see bj-vtoclg1f 36919), which requires fewer axioms (i.e., removes dependency on ax-6 1967, ax-7 2007, ax-9 2118, ax-12 2177, ax-ext 2708, df-clab 2715, df-cleq 2729, df-v 3482). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
| Theorem | bj-rabeqbid 36922 | Version of rabeqbidv 3455 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | bj-seex 36923* | Version of seex 5644 with a disjoint variable condition replaced by a nonfreeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.) |
| ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V) | ||
| Theorem | bj-nfcf 36924* | Version of df-nfc 2892 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
| ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
| Theorem | bj-zfauscl 36925* |
General version of zfauscl 5298.
Remark: the comment in zfauscl 5298 is misleading: the essential use of ax-ext 2708 is the one via eleq2 2830 and not the one via vtocl 3558, since the latter can be proved without ax-ext 2708 (see bj-vtoclg 36921). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
| Theorem | bj-elabd2ALT 36926* | Alternate proof of elabd2 3670 bypassing elab6g 3669 (and using sbiedvw 2095 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓}) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
| Theorem | bj-unrab 36927* | Generalization of unrab 4315. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
| Theorem | bj-inrab 36928 | Generalization of inrab 4316. (Contributed by BJ, 21-Apr-2019.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | bj-inrab2 36929 | Shorter proof of inrab 4316. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | bj-inrab3 36930* | Generalization of dfrab3ss 4323, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
| ⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
| Theorem | bj-rabtr 36931* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
| Theorem | bj-rabtrALT 36932* | Alternate proof of bj-rabtr 36931. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
| Theorem | bj-rabtrAUTO 36933* | Proof of bj-rabtr 36931 found automatically by the Metamath program "MM-PA> IMPROVE ALL / DEPTH 3 / 3" command followed by "MM-PA> MINIMIZE_WITH *". (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
| Syntax | bj-cgab 36934 | Syntax for generalized class abstractions. |
| class {𝐴 ∣ 𝑥 ∣ 𝜑} | ||
| Definition | df-bj-gab 36935* | Definition of generalized class abstractions: typically, 𝑥 is a bound variable in 𝐴 and 𝜑 and {𝐴 ∣ 𝑥 ∣ 𝜑} denotes "the class of 𝐴(𝑥)'s such that 𝜑(𝑥)". (Contributed by BJ, 4-Oct-2024.) |
| ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)} | ||
| Theorem | bj-gabss 36936 | Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓}) | ||
| Theorem | bj-gabssd 36937 | Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
| Theorem | bj-gabeqd 36938 | Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
| Theorem | bj-gabeqis 36939* | Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓} | ||
| Theorem | bj-elgab 36940 | Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒)) | ||
| Theorem | bj-gabima 36941 |
Generalized class abstraction as a direct image.
TODO: improve the support lemmas elimag 6082 and fvelima 6974 to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝐹) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓})) | ||
In this subsection, we define restricted nonfreeness (or relative nonfreeness). | ||
| Syntax | wrnf 36942 | Syntax for restricted nonfreeness. |
| wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
| Definition | df-bj-rnf 36943 | Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.) |
| ⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
A few results around Russell's paradox. For clarity, we prove separately a FOL statement (now in the main part as ru0 2127) and then two versions (bj-ru1 36944 and bj-ru 36945). Special attention is put on minimizing axiom depencencies. | ||
| Theorem | bj-ru1 36944* | A version of Russell's paradox ru 3786 not mentioning the universal class. (see also bj-ru 36945). (Contributed by BJ, 12-Oct-2019.) Remove usage of ax-10 2141, ax-11 2157, ax-12 2177 by using eqabbw 2815 following BTernaryTau's similar revision of ru 3786. (Revised by BJ, 28-Jun-2025.) (Proof modification is discouraged.) |
| ⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
| Theorem | bj-ru 36945 | Remove dependency on ax-13 2377 (and df-v 3482) from Russell's paradox ru 3786 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2822 instead of isset 3494 to avoid use of df-v 3482. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
| ⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
| Theorem | currysetlem 36946* | Lemma for currysetlem 36946, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
| ⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
| Theorem | curryset 36947* | Curry's paradox in set theory. This can be seen as a generalization of Russell's paradox, which corresponds to the case where 𝜑 is ⊥. See alternate exposal of basically the same proof currysetALT 36951. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
| ⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
| Theorem | currysetlem1 36948* | Lemma for currysetALT 36951. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
| ⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
| Theorem | currysetlem2 36949* | Lemma for currysetALT 36951. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
| ⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
| Theorem | currysetlem3 36950* | Lemma for currysetALT 36951. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
| ⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
| Theorem | currysetALT 36951* | Alternate proof of curryset 36947, or more precisely alternate exposal of the same proof. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
A few utility theorems on disjointness of classes. | ||
| Theorem | bj-n0i 36952* | Inference associated with n0 4353. Shortens 2ndcdisj 23464 (2888>2878), notzfaus 5363 (264>253). (Contributed by BJ, 22-Apr-2019.) |
| ⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
| Theorem | bj-disjsn01 36953 | Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9644 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
| ⊢ ({∅} ∩ {1o}) = ∅ | ||
| Theorem | bj-0nel1 36954 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ ∅ ∉ {1o} | ||
| Theorem | bj-1nel0 36955 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
| Theorem | bj-xpimasn 36956 | The image of a singleton, general case. [Change and relabel xpimasn 6205 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
| ⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
| Theorem | bj-xpima1sn 36957 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6205 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
| Theorem | bj-xpima1snALT 36958 | Alternate proof of bj-xpima1sn 36957. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
| Theorem | bj-xpima2sn 36959 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6205.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
| ⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
| Theorem | bj-xpnzex 36960 | If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv 7942 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
| Theorem | bj-xpexg2 36961 | Curried (exported) form of xpexg 7770. (Contributed by BJ, 2-Apr-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
| Theorem | bj-xpnzexb 36962 | If the first factor of a product is a nonempty set, then the product is a set if and only if the second factor is a set. (Contributed by BJ, 2-Apr-2019.) |
| ⊢ (𝐴 ∈ (𝑉 ∖ {∅}) → (𝐵 ∈ V ↔ (𝐴 × 𝐵) ∈ V)) | ||
| Theorem | bj-cleq 36963* | Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.) |
| ⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)}) | ||
This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes. | ||
| Theorem | bj-snsetex 36964* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5279. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
| Theorem | bj-clexab 36965* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
| Syntax | bj-csngl 36966 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
| class sngl 𝐴 | ||
| Definition | df-bj-sngl 36967* | Definition of "singletonization". The class sngl 𝐴 is isomorphic to 𝐴 and since it contains only singletons, it can be easily be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ sngl 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = {𝑦}} | ||
| Theorem | bj-sngleq 36968 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
| Theorem | bj-elsngl 36969* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
| Theorem | bj-snglc 36970 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
| Theorem | bj-snglss 36971 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
| Theorem | bj-0nelsngl 36972 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8506). (Contributed by BJ, 6-Oct-2018.) |
| ⊢ ∅ ∉ sngl 𝐴 | ||
| Theorem | bj-snglinv 36973* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
| Theorem | bj-snglex 36974 | A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ V ↔ sngl 𝐴 ∈ V) | ||
| Syntax | bj-ctag 36975 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
| class tag 𝐴 | ||
| Definition | df-bj-tag 36976 | Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ tag 𝐴 = (sngl 𝐴 ∪ {∅}) | ||
| Theorem | bj-tageq 36977 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
| Theorem | bj-eltag 36978* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
| Theorem | bj-0eltag 36979 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ ∅ ∈ tag 𝐴 | ||
| Theorem | bj-tagn0 36980 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ tag 𝐴 ≠ ∅ | ||
| Theorem | bj-tagss 36981 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
| Theorem | bj-snglsstag 36982 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
| Theorem | bj-sngltagi 36983 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
| Theorem | bj-sngltag 36984 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
| Theorem | bj-tagci 36985 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
| Theorem | bj-tagcg 36986 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
| Theorem | bj-taginv 36987* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} | ||
| Theorem | bj-tagex 36988 | A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ V ↔ tag 𝐴 ∈ V) | ||
| Theorem | bj-xtageq 36989 | The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 × tag 𝐴) = (𝐶 × tag 𝐵)) | ||
| Theorem | bj-xtagex 36990 | The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V)) | ||
This subsection gives a definition of an ordered pair, or couple (2-tuple), that "works" for proper classes, as evidenced by Theorems bj-2uplth 37022 and bj-2uplex 37023, and more importantly, bj-pr21val 37014 and bj-pr22val 37020. In particular, one can define well-behaved tuples of classes. Classes in ZF(C) are only virtual, and in particular they cannot be quantified over. Theorem bj-2uplex 37023 has advantages: in view of df-br 5144, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5813 (resp. relsnop 5815) would hold without antecedents (resp. hypotheses) thanks to relsnb 5812). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5737 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17184 could be simplified by removing the exception currently made for the empty set. The projections are denoted by pr1 and pr2 and the couple with projections (or coordinates) 𝐴 and 𝐵 is denoted by ⦅𝐴, 𝐵⦆. Note that this definition uses the Kuratowski definition (df-op 4633) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9658) without needing the axiom of regularity; it could even bypass this definition by "inlining" it. This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986). Note that this extends in a natural way to tuples. A variation of this definition is justified in opthprc 5749, but here we use "tagged versions" of the factors (see df-bj-tag 36976) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same). A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397. where a recursive definition of tuples is given that avoids the two-step definition of tuples and that can be adapted to various set theories. Finally, another survey is Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf 36976) | ||
| Syntax | bj-cproj 36991 | Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.) |
| class (𝐴 Proj 𝐵) | ||
| Definition | df-bj-proj 36992* | Definition of the class projection corresponding to tagged tuples. The expression (𝐴 Proj 𝐵) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
| ⊢ (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})} | ||
| Theorem | bj-projeq 36993 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷))) | ||
| Theorem | bj-projeq2 36994 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶)) | ||
| Theorem | bj-projun 36995 | The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶)) | ||
| Theorem | bj-projex 36996 | Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V) | ||
| Theorem | bj-projval 36997 | Value of the class projection. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) | ||
| Syntax | bj-c1upl 36998 | Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.) |
| class ⦅𝐴⦆ | ||
| Definition | df-bj-1upl 36999 | Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. Note that with this definition, the 0-tuple is the empty set. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37013, bj-2uplth 37022, bj-2uplex 37023, and the properties of the projections (see df-bj-pr1 37002 and df-bj-pr2 37016). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
| ⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴) | ||
| Theorem | bj-1upleq 37000 | Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |