![]() |
Metamath
Proof Explorer Theorem List (p. 362 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-vtoclg1f 36101* | Reprove vtoclg1f 3557 from bj-vtoclg1f1 36100. This removes dependency on ax-ext 2701, df-cleq 2722 and df-v 3474. Use bj-vtoclg1fv 36102 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg1fv 36102* | Version of bj-vtoclg1f 36101 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2066 and df-clab 2708. Prefer its use over bj-vtoclg1f 36101 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg 36103* | A version of vtoclg 3541 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2708, see bj-vtoclg1f 36101), which requires fewer axioms (i.e., removes dependency on ax-6 1969, ax-7 2009, ax-9 2114, ax-12 2169, ax-ext 2701, df-clab 2708, df-cleq 2722, df-v 3474). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-rabeqbid 36104 | Version of rabeqbidv 3447 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 36105* | Version of seex 5637 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 36106* | Version of df-nfc 2883 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 36107* |
General version of zfauscl 5300.
Remark: the comment in zfauscl 5300 is misleading: the essential use of ax-ext 2701 is the one via eleq2 2820 and not the one via vtocl 3544, since the latter can be proved without ax-ext 2701 (see bj-vtoclg 36103). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-elabd2ALT 36108* | Alternate proof of elabd2 3659 bypassing elab6g 3658 (and using sbiedvw 2094 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓}) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
Theorem | bj-unrab 36109* | Generalization of unrab 4304. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 36110 | Generalization of inrab 4305. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 36111 | Shorter proof of inrab 4305. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 36112* | Generalization of dfrab3ss 4311, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 36113* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrALT 36114* | Alternate proof of bj-rabtr 36113. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrAUTO 36115* | Proof of bj-rabtr 36113 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 36116 | Syntax for generalized class abstractions. |
class {𝐴 ∣ 𝑥 ∣ 𝜑} | ||
Definition | df-bj-gab 36117* | 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 36118 | Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.) |
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓}) | ||
Theorem | bj-gabssd 36119 | Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
Theorem | bj-gabeqd 36120 | Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
Theorem | bj-gabeqis 36121* | Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓} | ||
Theorem | bj-elgab 36122 | Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | bj-gabima 36123 |
Generalized class abstraction as a direct image.
TODO: improve the support lemmas elimag 6062 and fvelima 6956 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 36124 | Syntax for restricted nonfreeness. |
wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
Definition | df-bj-rnf 36125 | 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 36126) and then two versions (bj-ru1 36127 and bj-ru 36128). Special attention is put on minimizing axiom depencencies. | ||
Theorem | bj-ru0 36126* | The FOL part of Russell's paradox ru 3775 (see also bj-ru1 36127, bj-ru 36128). Use of elequ1 2111, bj-elequ12 35859 (instead of eleq1 2819, eleq12d 2825 as in ru 3775) permits to remove dependency on ax-10 2135, ax-11 2152, ax-12 2169, ax-ext 2701, df-sb 2066, df-clab 2708, df-cleq 2722, df-clel 2808. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥) | ||
Theorem | bj-ru1 36127* | A version of Russell's paradox ru 3775 (see also bj-ru 36128). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
Theorem | bj-ru 36128 | Remove dependency on ax-13 2369 (and df-v 3474) from Russell's paradox ru 3775 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2812 instead of isset 3485 to avoid use of df-v 3474. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 36129* | Lemma for currysetlem 36129, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 36130* | 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 36134. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 36131* | Lemma for currysetALT 36134. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 36132* | Lemma for currysetALT 36134. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 36133* | Lemma for currysetALT 36134. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 36134* | Alternate proof of curryset 36130, 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 36135* | Inference associated with n0 4345. Shortens 2ndcdisj 23180 (2888>2878), notzfaus 5360 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjsn01 36136 | Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9601 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 36137 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 36138 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 36139 | The image of a singleton, general case. [Change and relabel xpimasn 6183 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 36140 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6183 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 36141 | Alternate proof of bj-xpima1sn 36140. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 36142 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6183.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 36143 | 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 7913 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 36144 | Curried (exported) form of xpexg 7739. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 36145 | 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 36146* | 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 36147* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5284. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clexab 36148* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 36149 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 36150* | 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 36151 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 36152* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 36153 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 36154 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 36155 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8468). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 36156* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 36157 | 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 36158 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 36159 | 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 36160 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 36161* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 36162 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 36163 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 36164 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 36165 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 36166 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 36167 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 36168 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 36169 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-taginv 36170* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} | ||
Theorem | bj-tagex 36171 | 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 36172 | 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 36173 | 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 36205 and bj-2uplex 36206, and more importantly, bj-pr21val 36197 and bj-pr22val 36203. 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 36206 has advantages: in view of df-br 5148, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5802 (resp. relsnop 5804) would hold without antecedents (resp. hypotheses) thanks to relsnb 5801). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5727 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17084 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 4634) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9615) 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 5739, but here we use "tagged versions" of the factors (see df-bj-tag 36159) 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 36159) | ||
Syntax | bj-cproj 36174 | Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.) |
class (𝐴 Proj 𝐵) | ||
Definition | df-bj-proj 36175* | 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 36176 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷))) | ||
Theorem | bj-projeq2 36177 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶)) | ||
Theorem | bj-projun 36178 | The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶)) | ||
Theorem | bj-projex 36179 | Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V) | ||
Theorem | bj-projval 36180 | Value of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) | ||
Syntax | bj-c1upl 36181 | Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.) |
class ⦅𝐴⦆ | ||
Definition | df-bj-1upl 36182 | 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 36196, bj-2uplth 36205, bj-2uplex 36206, and the properties of the projections (see df-bj-pr1 36185 and df-bj-pr2 36199). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴) | ||
Theorem | bj-1upleq 36183 | Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆) | ||
Syntax | bj-cpr1 36184 | Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.) |
class pr1 𝐴 | ||
Definition | df-bj-pr1 36185 | Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq 36186, bj-pr11val 36189, bj-pr21val 36197, bj-pr1ex 36190. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ pr1 𝐴 = (∅ Proj 𝐴) | ||
Theorem | bj-pr1eq 36186 | Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵) | ||
Theorem | bj-pr1un 36187 | The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵) | ||
Theorem | bj-pr1val 36188 | Value of the first projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅) | ||
Theorem | bj-pr11val 36189 | Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ⦅𝐴⦆ = 𝐴 | ||
Theorem | bj-pr1ex 36190 | Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V) | ||
Theorem | bj-1uplth 36191 | The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵) | ||
Theorem | bj-1uplex 36192 | A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V) | ||
Theorem | bj-1upln0 36193 | A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ ⦅𝐴⦆ ≠ ∅ | ||
Syntax | bj-c2uple 36194 | Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.) |
class ⦅𝐴, 𝐵⦆ | ||
Definition | df-bj-2upl 36195 | Definition of the Morse couple. See df-bj-1upl 36182. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 36196, bj-2uplth 36205, bj-2uplex 36206, and the properties of the projections (see df-bj-pr1 36185 and df-bj-pr2 36199). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) | ||
Theorem | bj-2upleq 36196 | Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆)) | ||
Theorem | bj-pr21val 36197 | Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴 | ||
Syntax | bj-cpr2 36198 | Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.) |
class pr2 𝐴 | ||
Definition | df-bj-pr2 36199 | Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 36200, bj-pr22val 36203, bj-pr2ex 36204. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ pr2 𝐴 = (1o Proj 𝐴) | ||
Theorem | bj-pr2eq 36200 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |