Home | Metamath
Proof Explorer Theorem List (p. 350 of 463) | < 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-29028) |
Hilbert Space Explorer
(29029-30551) |
Users' Mathboxes
(30552-46213) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-ru 34901 | Remove dependency on ax-13 2373 (and df-v 3424) from Russell's paradox ru 3709 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2820 instead of isset 3435 to avoid use of df-v 3424. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 34902* | Lemma for currysetlem 34902, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 34903* | 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 34907. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 34904* | Lemma for currysetALT 34907. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 34905* | Lemma for currysetALT 34907. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 34906* | Lemma for currysetALT 34907. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 34907* | Alternate proof of curryset 34903, 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 34908* | Inference associated with n0 4277. Shortens 2ndcdisj 22382 (2888>2878), notzfaus 5270 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjcsn 34909 | A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 32457 and does not depend on df-ne 2943. (Contributed by BJ, 4-Apr-2019.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bj-disjsn01 34910 | Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34909 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 34911 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 34912 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 34913 | The image of a singleton, general case. [Change and relabel xpimasn 6065 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 34914 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6065 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 34915 | Alternate proof of bj-xpima1sn 34914. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 34916 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6065.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 34917 | 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 7719 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 34918 | Curried (exported) form of xpexg 7556. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 34919 | 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 34920* | 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 34921* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5195. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clex 34922* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 34923 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 34924* | 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 34925 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 34926* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 34927 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 34928 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 34929 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8225). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 34930* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 34931 | 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 34932 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 34933 | 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 34934 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 34935* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 34936 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 34937 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 34938 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 34939 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 34940 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 34941 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 34942 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 34943 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-taginv 34944* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} | ||
Theorem | bj-tagex 34945 | 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 34946 | 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 34947 | 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 34979 and bj-2uplex 34980, and more importantly, bj-pr21val 34971 and bj-pr22val 34977. 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 34980 has advantages: in view of df-br 5070, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5690 (resp. relsnop 5692) would hold without antecedents (resp. hypotheses) thanks to relsnb 5689). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5618 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 16730 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 4564) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9260) 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 5630, but here we use "tagged versions" of the factors (see df-bj-tag 34933) 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 34933) | ||
Syntax | bj-cproj 34948 | Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.) |
class (𝐴 Proj 𝐵) | ||
Definition | df-bj-proj 34949* | 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 34950 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷))) | ||
Theorem | bj-projeq2 34951 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶)) | ||
Theorem | bj-projun 34952 | The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶)) | ||
Theorem | bj-projex 34953 | Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V) | ||
Theorem | bj-projval 34954 | Value of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) | ||
Syntax | bj-c1upl 34955 | Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.) |
class ⦅𝐴⦆ | ||
Definition | df-bj-1upl 34956 | 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 34970, bj-2uplth 34979, bj-2uplex 34980, and the properties of the projections (see df-bj-pr1 34959 and df-bj-pr2 34973). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴) | ||
Theorem | bj-1upleq 34957 | Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆) | ||
Syntax | bj-cpr1 34958 | Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.) |
class pr1 𝐴 | ||
Definition | df-bj-pr1 34959 | 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 34960, bj-pr11val 34963, bj-pr21val 34971, bj-pr1ex 34964. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ pr1 𝐴 = (∅ Proj 𝐴) | ||
Theorem | bj-pr1eq 34960 | Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵) | ||
Theorem | bj-pr1un 34961 | The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵) | ||
Theorem | bj-pr1val 34962 | Value of the first projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅) | ||
Theorem | bj-pr11val 34963 | Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ⦅𝐴⦆ = 𝐴 | ||
Theorem | bj-pr1ex 34964 | Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V) | ||
Theorem | bj-1uplth 34965 | The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵) | ||
Theorem | bj-1uplex 34966 | A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V) | ||
Theorem | bj-1upln0 34967 | A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ ⦅𝐴⦆ ≠ ∅ | ||
Syntax | bj-c2uple 34968 | Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.) |
class ⦅𝐴, 𝐵⦆ | ||
Definition | df-bj-2upl 34969 | Definition of the Morse couple. See df-bj-1upl 34956. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 34970, bj-2uplth 34979, bj-2uplex 34980, and the properties of the projections (see df-bj-pr1 34959 and df-bj-pr2 34973). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) | ||
Theorem | bj-2upleq 34970 | Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆)) | ||
Theorem | bj-pr21val 34971 | Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴 | ||
Syntax | bj-cpr2 34972 | Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.) |
class pr2 𝐴 | ||
Definition | df-bj-pr2 34973 | 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 34974, bj-pr22val 34977, bj-pr2ex 34978. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ pr2 𝐴 = (1o Proj 𝐴) | ||
Theorem | bj-pr2eq 34974 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) | ||
Theorem | bj-pr2un 34975 | The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵) | ||
Theorem | bj-pr2val 34976 | Value of the second projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅) | ||
Theorem | bj-pr22val 34977 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 | ||
Theorem | bj-pr2ex 34978 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
Theorem | bj-2uplth 34979 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5376). (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | bj-2uplex 34980 | A couple is a set if and only if its coordinates are sets. For the advantages offered by the reverse closure property, see the section head comment. (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-2upln0 34981 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
Theorem | bj-2upln1upl 34982 | A couple is never equal to a monuple. It is in order to have this "non-clashing" result that tagging was used. Without tagging, we would have ⦅𝐴, ∅⦆ = ⦅𝐴⦆. Note that in the context of Morse tuples, it is natural to define the 0-tuple as the empty set. Therefore, the present theorem together with bj-1upln0 34967 and bj-2upln0 34981 tell us that an m-tuple may equal an n-tuple only when m = n, at least for m, n <= 2, but this result would extend as soon as we define n-tuples for higher values of n. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆ | ||
Some elementary set-theoretic operations "relative to a universe" (by which is merely meant some given class considered as a universe). | ||
Theorem | bj-rcleqf 34983 | Relative version of cleqf 2937. (Contributed by BJ, 27-Dec-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-rcleq 34984* | Relative version of dfcleq 2732. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-reabeq 34985* | Relative form of abeq2 2871. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-disj2r 34986 | Relative version of ssdifin0 4413, allowing a biconditional, and of disj2 4388. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4413 nor disj2 4388. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅) | ||
Theorem | bj-sscon 34987 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4068, which it can shorten, as well as conss2 41769. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4068 nor conss2 41769. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
Miscellaneous theorems of set theory. | ||
Theorem | eleq2w2ALT 34988 | Alternate proof of eleq2w2 2735 and special instance of eleq2 2828. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-clel3gALT 34989* | Alternate proof of clel3g 3583. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | bj-pw0ALT 34990 | Alternate proof of pw0 4741. The proofs have a similar structure: pw0 4741 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 34990 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4741 and biconditional for bj-pw0ALT 34990) to translate the property ss0b 4328 into the wanted result. To translate a biconditional into a class equality, pw0 4741 uses abbii 2810 (which yields an equality of class abstractions), while bj-pw0ALT 34990 uses eqriv 2736 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2810, through its closed form abbi1 2808, is proved from eqrdv 2737, which is the deduction form of eqriv 2736. In the other direction, velpw 4534 and velsn 4573 are proved from the definitions of powerclass and singleton using elabg 3599, which is a version of abbii 2810 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 ∅ = {∅} | ||
Theorem | bj-sselpwuni 34991 | Quantitative version of ssexg 5232: a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 ∪ 𝑉) | ||
Theorem | bj-unirel 34992 | Quantitative version of uniexr 7569: if the union of a class is an element of a class, then that class is an element of the double powerclass of the union of this class. (Contributed by BJ, 6-Apr-2024.) |
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉) | ||
Theorem | bj-elpwg 34993 | If the intersection of two classes is a set, then inclusion among these classes is equivalent to membership in the powerclass. Common generalization of elpwg 4532 and elpw2g 5253 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-vjust 34994 | Justification theorem for dfv2 3425 if it were the definition. See also vjust 3423. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
Theorem | bj-nul 34995* | Two formulations of the axiom of the empty set ax-nul 5215. Proposal: place it right before ax-nul 5215. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliota 34996* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 34997. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliotaALT 34997* | Alternate proof of bj-nuliota 34996. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6378). This is an implementation detail of the encoding currently used in set.mm and should be avoided. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-vtoclgfALT 34998 | Alternate proof of vtoclgf 3493. Proof from vtoclgft 3482. (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-elsn12g 34999 | Join of elsng 4571 and elsn2g 4595. (Contributed by BJ, 18-Nov-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-elsnb 35000 | Biconditional version of elsng 4571. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |