Home | Metamath
Proof Explorer Theorem List (p. 342 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-ceqsaltv 34101* | Version of bj-ceqsalt 34100 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2061 and df-clab 2800. Prefer its use over bj-ceqsalt 34100 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg0 34102 | The FOL content of ceqsalg 3530. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg 34103* | Remove from ceqsalg 3530 dependency on ax-ext 2793 (and on df-cleq 2814 and df-v 3497). See also bj-ceqsalgv 34105. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgALT 34104* | Alternate proof of bj-ceqsalg 34103. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgv 34105* | Version of bj-ceqsalg 34103 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2061 and df-clab 2800. Prefer its use over bj-ceqsalg 34103 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgvALT 34106* | Alternate proof of bj-ceqsalgv 34105. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsal 34107* | Remove from ceqsal 3532 dependency on ax-ext 2793 (and on df-cleq 2814, df-v 3497, df-clab 2800, df-sb 2061). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-ceqsalv 34108* | Remove from ceqsalv 3533 dependency on ax-ext 2793 (and on df-cleq 2814, df-v 3497, df-clab 2800, df-sb 2061). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-spcimdv 34109* | Remove from spcimdv 3592 dependency on ax-9 2115, ax-10 2136, ax-11 2151, ax-13 2383, ax-ext 2793, df-cleq 2814 (and df-nfc 2963, df-v 3497, df-or 842, df-tru 1531, df-nf 1776). For an even more economical version, see bj-spcimdvv 34110. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-spcimdvv 34110* | Remove from spcimdv 3592 dependency on ax-7 2006, ax-8 2107, ax-10 2136, ax-11 2151, ax-12 2167 ax-13 2383, ax-ext 2793, df-cleq 2814, df-clab 2800 (and df-nfc 2963, df-v 3497, df-or 842, df-tru 1531, df-nf 1776) at the price of adding a disjoint variable condition on 𝑥, 𝐵 (but in usages, 𝑥 is typically a dummy, hence fresh, variable). For the version without this disjoint variable condition, see bj-spcimdv 34109. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | elelb 34111 | Equivalence between two common ways to characterize elements of a class 𝐵: the LHS says that sets are elements of 𝐵 if and only if they satisfy 𝜑 while the RHS says that classes are elements of 𝐵 if and only if they are sets and satisfy 𝜑. Therefore, the LHS is a characterization among sets while the RHS is a characterization among classes. Note that the LHS is often formulated using a class variable instead of the universe V while this is not possible for the RHS (apart from using 𝐵 itself, which would not be very useful). (Contributed by BJ, 26-Feb-2023.) |
⊢ ((𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜑)) ↔ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜑))) | ||
Theorem | bj-pwvrelb 34112 | Characterization of the elements of the powerclass of the cartesian square of the universal class: they are exactly the sets which are binary relations. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝐴 ∈ 𝒫 (V × V) ↔ (𝐴 ∈ V ∧ Rel 𝐴)) | ||
In this section, we prove the symmetry of the nonfreeness quantifier for classes. | ||
Theorem | bj-nfcsym 34113 | The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5268 with additional axioms; see also nfcv 2977). This could be proved from aecom 2444 and nfcvb 5269 but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid use of eqcomd 2827 instead of equcomd 2017; removing dependency on ax-ext 2793 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2997, eleq2d 2898 (using elequ2 2120), nfcvf 3007, dvelimc 3006, dvelimdc 3005, nfcvf2 3008. (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥) | ||
Note: now that the proposals have been adopted as df-cleq 2814 and df-clel 2893, and that ax9ALT 2817 is in the main section, we only keep bj-ax9 34114 here as a weaker version of ax9ALT 2817 proved without ax-8 2107. | ||
Theorem | bj-ax9 34114* | Proof of ax-9 2115 from Tarski's FOL=, sp 2172, dfcleq 2815 and ax-ext 2793 (with two extra disjoint variable conditions on 𝑥, 𝑧 and 𝑦, 𝑧). See ax9ALT 2817 for a more general version, proved using also ax-8 2107. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | ||
Some useful theorems for dealing with substitutions: sbbi 2309, sbcbig 3822, sbcel1g 4364, sbcel2 4366, sbcel12 4359, sbceqg 4360, csbvarg 4382. | ||
Theorem | bj-sbeqALT 34115* | Substitution in an equality (use the more genereal version bj-sbeq 34116 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbeq 34116 | Distribute proper substitution through an equality relation. (See sbceqg 4360). (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbceqgALT 34117 | Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4360. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4360, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | bj-csbsnlem 34118* | Lemma for bj-csbsn 34119 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-csbsn 34119 | Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-sbel1 34120* | Version of sbcel1g 4364 when substituting a set. (Note: one could have a corresponding version of sbcel12 4359 when substituting a set, but the point here is that the antecedent of sbcel1g 4364 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵) | ||
Theorem | bj-abv 34121 | The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
Theorem | bj-ab0 34122 | The class of sets verifying a falsity is the empty set (closed form of abf 4355). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | bj-abf 34123 | Shorter proof of abf 4355 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | bj-csbprc 34124 | More direct proof of csbprc 4357 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | bj-exlimvmpi 34125* | A Fol lemma (exlimiv 1922 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpi 34126 | Lemma for bj-vtoclg1f1 34131 (an instance of this lemma is a version of bj-vtoclg1f1 34131 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbi 34127 | Lemma for theorems of the vtoclg 3568 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbir 34128 | Lemma for theorems of the vtoclg 3568 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (∃𝑥𝜒 → 𝜑) | ||
Theorem | bj-vtoclf 34129* | Remove dependency on ax-ext 2793, df-clab 2800 and df-cleq 2814 (and df-sb 2061 and df-v 3497) from vtoclf 3559. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtocl 34130* | Remove dependency on ax-ext 2793, df-clab 2800 and df-cleq 2814 (and df-sb 2061 and df-v 3497) from vtocl 3560. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtoclg1f1 34131* | The FOL content of vtoclg1f 3567 (hence not using ax-ext 2793, df-cleq 2814, df-nfc 2963, df-v 3497). 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 2793; as a byproduct, this dispenses with ax-11 2151 and ax-13 2383). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓) | ||
Theorem | bj-vtoclg1f 34132* | Reprove vtoclg1f 3567 from bj-vtoclg1f1 34131. This removes dependency on ax-ext 2793, df-cleq 2814 and df-v 3497. Use bj-vtoclg1fv 34133 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg1fv 34133* | Version of bj-vtoclg1f 34132 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2061 and df-clab 2800. Prefer its use over bj-vtoclg1f 34132 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg 34134* | A version of vtoclg 3568 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2800, see bj-vtoclg1f 34132), which requires fewer axioms (i.e., removes dependency on ax-6 1961, ax-7 2006, ax-9 2115, ax-12 2167, ax-ext 2793, df-clab 2800, df-cleq 2814, df-v 3497). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-rabbida2 34135 | Version of rabbidva2 3477 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqd 34136 | Deduction form of rabeq 3484. Note that contrary to rabeq 3484 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | bj-rabeqbid 34137 | Version of rabeqbidv 3486 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqbida 34138 | Version of rabeqbidva 3487 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 34139* | Version of seex 5512 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 34140* | Version of df-nfc 2963 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 34141* |
General version of zfauscl 5197.
Remark: the comment in zfauscl 5197 is misleading: the essential use of ax-ext 2793 is the one via eleq2 2901 and not the one via vtocl 3560, since the latter can be proved without ax-ext 2793 (see bj-vtoclg 34134). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-unrab 34142* | Generalization of unrab 4273. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 34143 | Generalization of inrab 4274. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 34144 | Shorter proof of inrab 4274. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 34145* | Generalization of dfrab3ss 4280, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 34146* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrALT 34147* | Alternate proof of bj-rabtr 34146. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrAUTO 34148* | Proof of bj-rabtr 34146 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.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
In this subsection, we define restricted nonfreeness (or relative nonfreeness). | ||
Syntax | wrnf 34149 | Syntax for restricted nonfreeness. |
wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
Definition | df-bj-rnf 34150 | 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 its FOL part (bj-ru0 34151) and then two versions (bj-ru1 34152 and bj-ru 34153). Special attention is put on minimizing axiom depencencies. | ||
Theorem | bj-ru0 34151* | The FOL part of Russell's paradox ru 3770 (see also bj-ru1 34152, bj-ru 34153). Use of elequ1 2112, bj-elequ12 33910 (instead of eleq1 2900, eleq12d 2907 as in ru 3770) permits to remove dependency on ax-10 2136, ax-11 2151, ax-12 2167, ax-ext 2793, df-sb 2061, df-clab 2800, df-cleq 2814, df-clel 2893. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥) | ||
Theorem | bj-ru1 34152* | A version of Russell's paradox ru 3770 (see also bj-ru 34153). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
Theorem | bj-ru 34153 | Remove dependency on ax-13 2383 (and df-v 3497) from Russell's paradox ru 3770 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of bj-elissetv 34089 instead of isset 3507 to avoid use of df-v 3497. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 34154* | Lemma for currysetlem 34154, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 34155* | 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 34159. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 34156* | Lemma for currysetALT 34159. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 34157* | Lemma for currysetALT 34159. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 34158* | Lemma for currysetALT 34159. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 34159* | Alternate proof of curryset 34155, 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 34160* | Inference associated with n0 4309. Shortens 2ndcdisj 21994 (2888>2878), notzfaus 5254 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjcsn 34161 | A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 31907 and does not depend on df-ne 3017. (Contributed by BJ, 4-Apr-2019.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bj-disjsn01 34162 | Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34161 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 34163 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 34164 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 34165 | The image of a singleton, general case. [Change and relabel xpimasn 6036 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 34166 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6036 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 34167 | Alternate proof of bj-xpima1sn 34166. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 34168 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6036] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 34169 | 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 7613 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 34170 | Curried (exported) form of xpexg 7461. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 34171 | 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 34172* | 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 34173* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5182. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clex 34174* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 34175 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 34176* | 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 34177 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 34178* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 34179 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 34180 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 34181 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8093). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 34182* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 34183 | 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 34184 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 34185 | 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 34186 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 34187* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 34188 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 34189 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 34190 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 34191 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 34192 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 34193 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 34194 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 34195 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-taginv 34196* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} | ||
Theorem | bj-tagex 34197 | 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 34198 | 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 34199 | 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 34231 and bj-2uplex 34232, and more importantly, bj-pr21val 34223 and bj-pr22val 34229. 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 34232 has advantages: in view of df-br 5059, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5670 (resp. relsnop 5672) would hold without antecedents (resp. hypotheses) thanks to relsnb 5669). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5598 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 16475 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 Kuratowksi definition (df-op 4566) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9070) 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 5610, but here we use "tagged versions" of the factors (see df-bj-tag 34185) 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 2-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 34185) | ||
Syntax | bj-cproj 34200 | Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.) |
class (𝐴 Proj 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |