![]() |
Metamath
Proof Explorer Theorem List (p. 359 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-rabeqbid 35801 | Version of rabeqbidv 3450 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 35802* | Version of seex 5639 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 35803* | Version of df-nfc 2886 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 35804* |
General version of zfauscl 5302.
Remark: the comment in zfauscl 5302 is misleading: the essential use of ax-ext 2704 is the one via eleq2 2823 and not the one via vtocl 3550, since the latter can be proved without ax-ext 2704 (see bj-vtoclg 35800). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-elabd2ALT 35805* | Alternate proof of elabd2 3661 bypassing elab6g 3660 (and using sbiedvw 2097 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓}) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
Theorem | bj-unrab 35806* | Generalization of unrab 4306. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 35807 | Generalization of inrab 4307. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 35808 | Shorter proof of inrab 4307. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 35809* | Generalization of dfrab3ss 4313, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 35810* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrALT 35811* | Alternate proof of bj-rabtr 35810. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrAUTO 35812* | Proof of bj-rabtr 35810 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 35813 | Syntax for generalized class abstractions. |
class {𝐴 ∣ 𝑥 ∣ 𝜑} | ||
Definition | df-bj-gab 35814* | 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 35815 | Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.) |
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓}) | ||
Theorem | bj-gabssd 35816 | Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
Theorem | bj-gabeqd 35817 | Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒}) | ||
Theorem | bj-gabeqis 35818* | Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓} | ||
Theorem | bj-elgab 35819 | Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | bj-gabima 35820 |
Generalized class abstraction as a direct image.
TODO: improve the support lemmas elimag 6064 and fvelima 6958 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 35821 | Syntax for restricted nonfreeness. |
wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
Definition | df-bj-rnf 35822 | 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 35823) and then two versions (bj-ru1 35824 and bj-ru 35825). Special attention is put on minimizing axiom depencencies. | ||
Theorem | bj-ru0 35823* | The FOL part of Russell's paradox ru 3777 (see also bj-ru1 35824, bj-ru 35825). Use of elequ1 2114, bj-elequ12 35556 (instead of eleq1 2822, eleq12d 2828 as in ru 3777) permits to remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-ext 2704, df-sb 2069, df-clab 2711, df-cleq 2725, df-clel 2811. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥) | ||
Theorem | bj-ru1 35824* | A version of Russell's paradox ru 3777 (see also bj-ru 35825). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
Theorem | bj-ru 35825 | Remove dependency on ax-13 2372 (and df-v 3477) from Russell's paradox ru 3777 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2815 instead of isset 3488 to avoid use of df-v 3477. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 35826* | Lemma for currysetlem 35826, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 35827* | 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 35831. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 35828* | Lemma for currysetALT 35831. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 35829* | Lemma for currysetALT 35831. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 35830* | Lemma for currysetALT 35831. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 35831* | Alternate proof of curryset 35827, 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 35832* | Inference associated with n0 4347. Shortens 2ndcdisj 22960 (2888>2878), notzfaus 5362 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjsn01 35833 | Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9599 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 35834 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 35835 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 35836 | The image of a singleton, general case. [Change and relabel xpimasn 6185 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 35837 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6185 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 35838 | Alternate proof of bj-xpima1sn 35837. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 35839 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6185.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 35840 | 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 7911 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 35841 | Curried (exported) form of xpexg 7737. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 35842 | 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 35843* | 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 35844* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5286. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clexab 35845* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 35846 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 35847* | 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 35848 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 35849* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 35850 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 35851 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 35852 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8466). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 35853* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 35854 | 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 35855 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 35856 | 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 35857 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 35858* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 35859 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 35860 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 35861 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 35862 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 35863 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 35864 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 35865 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 35866 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-taginv 35867* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} | ||
Theorem | bj-tagex 35868 | 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 35869 | 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 35870 | 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 35902 and bj-2uplex 35903, and more importantly, bj-pr21val 35894 and bj-pr22val 35900. 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 35903 has advantages: in view of df-br 5150, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5804 (resp. relsnop 5806) would hold without antecedents (resp. hypotheses) thanks to relsnb 5803). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5729 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17080 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 4636) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9613) 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 5741, but here we use "tagged versions" of the factors (see df-bj-tag 35856) 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 35856) | ||
Syntax | bj-cproj 35871 | Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.) |
class (𝐴 Proj 𝐵) | ||
Definition | df-bj-proj 35872* | 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 35873 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷))) | ||
Theorem | bj-projeq2 35874 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶)) | ||
Theorem | bj-projun 35875 | The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶)) | ||
Theorem | bj-projex 35876 | Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V) | ||
Theorem | bj-projval 35877 | Value of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) | ||
Syntax | bj-c1upl 35878 | Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.) |
class ⦅𝐴⦆ | ||
Definition | df-bj-1upl 35879 | 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 35893, bj-2uplth 35902, bj-2uplex 35903, and the properties of the projections (see df-bj-pr1 35882 and df-bj-pr2 35896). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴) | ||
Theorem | bj-1upleq 35880 | Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆) | ||
Syntax | bj-cpr1 35881 | Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.) |
class pr1 𝐴 | ||
Definition | df-bj-pr1 35882 | 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 35883, bj-pr11val 35886, bj-pr21val 35894, bj-pr1ex 35887. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ pr1 𝐴 = (∅ Proj 𝐴) | ||
Theorem | bj-pr1eq 35883 | Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵) | ||
Theorem | bj-pr1un 35884 | The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵) | ||
Theorem | bj-pr1val 35885 | Value of the first projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅) | ||
Theorem | bj-pr11val 35886 | Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ⦅𝐴⦆ = 𝐴 | ||
Theorem | bj-pr1ex 35887 | Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V) | ||
Theorem | bj-1uplth 35888 | The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵) | ||
Theorem | bj-1uplex 35889 | A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V) | ||
Theorem | bj-1upln0 35890 | A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ ⦅𝐴⦆ ≠ ∅ | ||
Syntax | bj-c2uple 35891 | Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.) |
class ⦅𝐴, 𝐵⦆ | ||
Definition | df-bj-2upl 35892 | Definition of the Morse couple. See df-bj-1upl 35879. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 35893, bj-2uplth 35902, bj-2uplex 35903, and the properties of the projections (see df-bj-pr1 35882 and df-bj-pr2 35896). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) | ||
Theorem | bj-2upleq 35893 | Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆)) | ||
Theorem | bj-pr21val 35894 | Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴 | ||
Syntax | bj-cpr2 35895 | Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.) |
class pr2 𝐴 | ||
Definition | df-bj-pr2 35896 | 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 35897, bj-pr22val 35900, bj-pr2ex 35901. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ pr2 𝐴 = (1o Proj 𝐴) | ||
Theorem | bj-pr2eq 35897 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) | ||
Theorem | bj-pr2un 35898 | The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵) | ||
Theorem | bj-pr2val 35899 | Value of the second projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅) | ||
Theorem | bj-pr22val 35900 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |