![]() |
Metamath
Proof Explorer Theorem List (p. 360 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-pr2ex 35901 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
Theorem | bj-2uplth 35902 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5477). (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | bj-2uplex 35903 | 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 35904 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
Theorem | bj-2upln1upl 35905 | 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 35890 and bj-2upln0 35904 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 35906 | Relative version of cleqf 2935. (Contributed by BJ, 27-Dec-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-rcleq 35907* | Relative version of dfcleq 2726. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-reabeq 35908* | Relative form of eqabb 2874. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-disj2r 35909 | Relative version of ssdifin0 4486, allowing a biconditional, and of disj2 4458. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4486 nor disj2 4458. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅) | ||
Theorem | bj-sscon 35910 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4138, which it can shorten, as well as conss2 43202. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4138 nor conss2 43202. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
In this section, we introduce the axiom of singleton ax-bj-sn 35914 and the axiom of binary union ax-bj-bun 35918. Both axioms are implied by the standard axioms of unordered pair ax-pr 5428 and of union ax-un 7725 (see snex 5432 and unex 7733). Conversely, the axiom of unordered pair ax-pr 5428 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 35920 and bj-prex 35921. The axioms of union ax-un 7725 and of powerset ax-pow 5364 are independent of these axioms: consider respectively the class of pseudo-hereditarily sets of cardinality less than a given singular strong limit cardinal, see Greg Oman, On the axiom of union, Arch. Math. Logic (2010) 49:283--289 (that model does have finite unions), and the class of well-founded hereditarily countable sets (or hereditarily less than a given uncountable regular cardinal). See also https://mathoverflow.net/questions/81815 5364 and https://mathoverflow.net/questions/48365 5364. A proof by finite induction shows that the existence of finite unions is equivalent to the existence of binary unions and of nullary unions (the latter being the axiom of the empty set ax-nul 5307). The axiom of binary union is useful in theories without the axioms of union ax-un 7725 and of powerset ax-pow 5364. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2704, ax-rep 5286, ax-sep 5300, ax-nul 5307, ax-reg 9587 } and the axioms of existence of unordered 𝑚-tuples for all 𝑚 ≤ 𝑛, and in most cases one would like to rule out such models, hence the need for extra axioms, typically variants of powersets or unions. The axiom of adjunction ax-bj-adj 35923 is more widely used, and is an axiom of General Set Theory. We prove how to retrieve it from binary union and singleton in bj-adjfrombun 35927 and conversely how to prove from adjunction singleton (bj-snfromadj 35925) and unordered pair (bj-prfromadj 35926). | ||
Theorem | bj-abex 35911* | Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-clex 35912* | Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-axsn 35913* | Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 35914). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)) | ||
Axiom | ax-bj-sn 35914* | Axiom of singleton. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) | ||
Theorem | bj-snexg 35915 | A singleton built on a set is a set. Contrary to bj-snex 35916, this proof is intuitionistically valid and does not require ax-nul 5307. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5432 and prove it from ax-bj-sn 35914. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | bj-snex 35916 | A singleton is a set. See also snex 5432, snexALT 5382. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 35914. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴} ∈ V | ||
Theorem | bj-axbun 35917* | Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 35918). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))) | ||
Axiom | ax-bj-bun 35918* | Axiom of binary union. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) | ||
Theorem | bj-unexg 35919 | Existence of binary unions of sets, proved from ax-bj-bun 35918. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-prexg 35920 | Existence of unordered pairs formed on sets, proved from ax-bj-sn 35914 and ax-bj-bun 35918. Contrary to bj-prex 35921, this proof is intuitionistically valid and does not require ax-nul 5307. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | bj-prex 35921 | Existence of unordered pairs proved from ax-bj-sn 35914 and ax-bj-bun 35918. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | bj-axadj 35922* | Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 35923). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))) | ||
Axiom | ax-bj-adj 35923* | Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)) | ||
Theorem | bj-adjg1 35924 | Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ {𝑥}) ∈ V) | ||
Theorem | bj-snfromadj 35925 | Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥} ∈ V | ||
Theorem | bj-prfromadj 35926 | Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | bj-adjfrombun 35927 | Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∪ {𝑦}) ∈ V | ||
Miscellaneous theorems of set theory. | ||
Theorem | eleq2w2ALT 35928 | Alternate proof of eleq2w2 2729 and special instance of eleq2 2823. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-clel3gALT 35929* | Alternate proof of clel3g 3651. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | bj-pw0ALT 35930 | Alternate proof of pw0 4816. The proofs have a similar structure: pw0 4816 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 35930 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4816 and biconditional for bj-pw0ALT 35930) to translate the property ss0b 4398 into the wanted result. To translate a biconditional into a class equality, pw0 4816 uses abbii 2803 (which yields an equality of class abstractions), while bj-pw0ALT 35930 uses eqriv 2730 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2803, through its closed form abbi 2801, is proved from eqrdv 2731, which is the deduction form of eqriv 2730. In the other direction, velpw 4608 and velsn 4645 are proved from the definitions of powerclass and singleton using elabg 3667, which is a version of abbii 2803 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 ∅ = {∅} | ||
Theorem | bj-sselpwuni 35931 | Quantitative version of ssexg 5324: 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 35932 | Quantitative version of uniexr 7750: 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 35933 | 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 4606 and elpw2g 5345 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-velpwALT 35934* | This theorem bj-velpwALT 35934 and the next theorem bj-elpwgALT 35935 are alternate proofs of velpw 4608 and elpwg 4606 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3560 instead of proving first the general case using elab2g 3671 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2172. In other cases, that order is better (e.g., vsnex 5430 proved before snexg 5431). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | bj-elpwgALT 35935 | Alternate proof of elpwg 4606. See comment for bj-velpwALT 35934. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-vjust 35936 | Justification theorem for dfv2 3478 if it were the definition. See also vjust 3476. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
Theorem | bj-nul 35937* | Two formulations of the axiom of the empty set ax-nul 5307. Proposal: place it right before ax-nul 5307. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliota 35938* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 35939. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliotaALT 35939* | Alternate proof of bj-nuliota 35938. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6522). 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 35940 | Alternate proof of vtoclgf 3555. Proof from vtoclgft 3541. (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 35941 | Join of elsng 4643 and elsn2g 4667. (Contributed by BJ, 18-Nov-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-elsnb 35942 | Biconditional version of elsng 4643. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-pwcfsdom 35943 | Remove hypothesis from pwcfsdom 10578. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 10578.) (Contributed by BJ, 14-Sep-2019.) |
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
Theorem | bj-grur1 35944 | Remove hypothesis from grur1 10815. Illustration of how to remove a "definitional hypothesis". This makes its uses longer, but the theorem feels more self-contained. It looks preferable when the defined term appears only once in the conclusion. (Contributed by BJ, 14-Sep-2019.) |
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘(𝑈 ∩ On))) | ||
Theorem | bj-bm1.3ii 35945* |
The extension of a predicate (𝜑(𝑧)) is included in a set
(𝑥) if and only if it is a set (𝑦).
Sufficiency is obvious,
and necessity is the content of the axiom of separation ax-sep 5300.
Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by
NM, 21-Jun-1993.) Generalized to a closed form biconditional with
existential quantifications using two different setvars 𝑥, 𝑦 (which
need not be disjoint). (Revised by BJ, 8-Aug-2022.)
TODO: move in place of bm1.3ii 5303. Relabel ("sepbi"?). |
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-dfid2ALT 35946 | Alternate version of dfid2 5577. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5575 instead to make the semantics of the construction df-opab 5212 clearer. (New usage is discouraged.) |
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤} | ||
Theorem | bj-0nelopab 35947 |
The empty set is never an element in an ordered-pair class abstraction.
(Contributed by Alexander van der Vekens, 5-Nov-2017.) (Proof shortened
by BJ, 22-Jul-2023.)
TODO: move to the main section when one can reorder sections so that we can use relopab 5825 (this is a very limited reordering). |
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} | ||
Theorem | bj-brrelex12ALT 35948 | Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5729. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-epelg 35949 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5584 and closed form of epeli 5583. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) TODO: move it to the main section after reordering to have brrelex1i 5733 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | bj-epelb 35950 | Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i 5734 available. Check if it is shorter to prove bj-epelg 35949 first or bj-epelb 35950 first. (Contributed by BJ, 14-Jul-2023.) |
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) | ||
Theorem | bj-nsnid 35951 | A set does not contain the singleton formed on it. More precisely, one can prove that a class contains the singleton formed on it if and only if it is proper and contains the empty set (since it is "the singleton formed on" any proper class, see snprc 4722): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴) | ||
Theorem | bj-rdg0gALT 35952 | Alternate proof of rdg0g 8427. More direct since it bypasses tz7.44-1 8406 and rdg0 8421 (and vtoclg 3557, vtoclga 3566). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | ||
This section treats the existing predicate Slot (df-slot 17115) as "evaluation at a class" and for the moment does not introduce new syntax for it. | ||
Theorem | bj-evaleq 35953 | Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17116 but may diverge from it if/when a token Eval is introduced for evaluation in order to separate it from Slot and any of its possible modifications. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵) | ||
Theorem | bj-evalfun 35954 | The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.) |
⊢ Fun Slot 𝐴 | ||
Theorem | bj-evalfn 35955 | The evaluation at a class is a function on the universal class. (General form of slotfn 17117). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.) |
⊢ Slot 𝐴 Fn V | ||
Theorem | bj-evalval 35956 | Value of the evaluation at a class. (Closed form of strfvnd 17118 and strfvn 17119). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.) |
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | bj-evalid 35957 | The evaluation at a set of the identity function is that set. (General form of ndxarg 17129.) The restriction to a set 𝑉 is necessary since the argument of the function Slot 𝐴 (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (Slot 𝐴‘( I ↾ 𝑉)) = 𝐴) | ||
Theorem | bj-ndxarg 35958 | Proof of ndxarg 17129 from bj-evalid 35957. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | bj-evalidval 35959 | Closed general form of strndxid 17131. Both sides are equal to (𝐹‘𝐴) by bj-evalid 35957 and bj-evalval 35956 respectively, but bj-evalidval 35959 adds something to bj-evalid 35957 and bj-evalval 35956 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
Syntax | celwise 35960 | Syntax for elementwise operations. |
class elwise | ||
Definition | df-elwise 35961* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11140), so if 𝐴 and 𝐵 are sets of complex numbers, then (𝐴(elwise‘ + )𝐵) is the set of numbers of the form (𝑥 + 𝑦) with 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵. The set of odd natural numbers is (({2}(elwise‘ · )ℕ0)(elwise‘ + ){1}), or less formally 2ℕ0 + 1. (Contributed by BJ, 22-Dec-2021.) |
⊢ elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)})) | ||
Many kinds of structures are given by families of subsets of a given set: Moore collections (df-mre 17530), topologies (df-top 22396), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 33107), sigma rings, monotone classes, matroids/independent sets, bornologies, filters. There is a natural notion of structure induced on a subset. It is often given by an elementwise intersection, namely, the family of intersections of sets in the original family with the given subset. In this subsection, we define this notion and prove its main properties. Classical conditions on families of subsets include being nonempty, containing the whole set, containing the empty set, being stable under unions, intersections, subsets, supersets, (relative) complements. Therefore, we prove related properties for the elementwise intersection. We will call (𝑋 ↾t 𝐴) the elementwise intersection on the family 𝑋 by the class 𝐴. REMARK: many theorems are already in set.mm: "MM> SEARCH *rest* / JOIN". | ||
Theorem | bj-rest00 35962 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17375. (Contributed by BJ, 27-Apr-2021.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | bj-restsn 35963 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 35966 and bj-restsnid 35968. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
Theorem | bj-restsnss 35964 | Special case of bj-restsn 35963. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
Theorem | bj-restsnss2 35965 | Special case of bj-restsn 35963. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
Theorem | bj-restsn0 35966 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 35963 and bj-restsnss2 35965. TODO: this is restsn 22674. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | bj-restsn10 35967 | Special case of bj-restsn 35963, bj-restsnss 35964, and bj-rest10 35969. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 35968 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 35963 and bj-restsnss 35964. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 35969 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 22673 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 35970 | Alternate version of bj-rest10 35969. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 35971 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 35972 | Alternate version of bj-restn0 35971. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 35973 | The elementwise intersection on a powerset is the powerset of the intersection. This allows to prove for instance that the topology induced on a subset by the discrete topology is the discrete topology on that subset. See also restdis 22682 (which uses distop 22498 and restopn2 22681). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 35974 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 35975 | An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restv 35976 | An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴)) | ||
Theorem | bj-resta 35977 | An elementwise intersection by a set on a family containing that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝐴 ∈ 𝑋 → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restuni 35978 | The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni 22666 and restuni2 22671. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 35979 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 22666 and restuni2 22671. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 35980 | A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∅ ∈ (𝐴 ↾t 𝐴)) | ||
Theorem | bj-raldifsn 35981* | All elements in a set satisfy a given property if and only if all but one satisfy that property and that one also does. Typically, this can be used for characterizations that are proved using different methods for a given element and for all others, for instance zero and nonzero numbers, or the empty set and nonempty sets. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ 𝜓))) | ||
Theorem | bj-0int 35982* | If 𝐴 is a collection of subsets of 𝑋, like a Moore collection or a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵: the LHS singles out the empty intersection (the empty intersection relative to 𝑋 is 𝑋 and the intersection of a nonempty family of subsets of 𝑋 is included in 𝑋, so there is no need to intersect it with 𝑋). In typical applications, 𝐵 is 𝐴 itself. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∩ 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 ∩ ∩ 𝑥) ∈ 𝐵)) | ||
Theorem | bj-mooreset 35983* |
A Moore collection is a set. Therefore, the class Moore of all
Moore sets defined in df-bj-moore 35985 is actually the class of all Moore
collections. This is also illustrated by the lack of sethood condition
in bj-ismoore 35986.
Note that the closed sets of a topology form a Moore collection, so a topology is a set, and this remark also applies to many other families of sets (namely, as soon as the whole set is required to be a set of the family, then the associated kind of family has no proper classes: that this condition suffices to impose sethood can be seen in this proof, which relies crucially on uniexr 7750). Note: if, in the above predicate, we substitute 𝒫 𝑋 for 𝐴, then the last ∈ 𝒫 𝑋 could be weakened to ⊆ 𝑋, and then the predicate would be obviously satisfied since ⊢ ∪ 𝒫 𝑋 = 𝑋 (unipw 5451), making 𝒫 𝑋 a Moore collection in this weaker sense, for any class 𝑋, even proper, but the addition of this single case does not add anything interesting. Instead, we have the biconditional bj-discrmoore 35992. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 35984 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 35985* |
Define the class of Moore collections. This is indeed the class of all
Moore collections since these all are sets, as proved in bj-mooreset 35983,
and as illustrated by the lack of sethood condition in bj-ismoore 35986.
This is to df-mre 17530 (defining Moore) what df-top 22396 (defining Top) is to df-topon 22413 (defining TopOn). For the sake of consistency, the function defined at df-mre 17530 should be denoted by "MooreOn". Note: df-mre 17530 singles out the empty intersection. This is not necessary. It could be written instead ⊢ Moore = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝒫 𝑥 ∣ ∀𝑧 ∈ 𝒫 𝑦(𝑥 ∩ ∩ 𝑧) ∈ 𝑦}) and the equivalence of both definitions is proved by bj-0int 35982. There is no added generality in defining a "Moore predicate" for arbitrary classes, since a Moore class satisfying such a predicate is automatically a set (see bj-mooreset 35983). TODO: move to the main section. For many families of sets, one can define both the function associating to each set the set of families of that kind on it (like df-mre 17530 and df-topon 22413) or the class of all families of that kind, independent of a base set (like df-bj-moore 35985 or df-top 22396). In general, the former will be more useful and the extra generality of the latter is not necessary. Moore collections, however, are particular in that they are more ubiquitous and are used in a wide variety of applications (for many families of sets, the family of families of a given kind is often a Moore collection, for instance). Therefore, in the case of Moore families, having both definitions is useful. (Contributed by BJ, 27-Apr-2021.) |
⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} | ||
Theorem | bj-ismoore 35986* | Characterization of Moore collections. Note that there is no sethood hypothesis on 𝐴: it is implied by either side (this is obvious for the LHS, and is the content of bj-mooreset 35983 for the RHS). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) | ||
Theorem | bj-ismoored0 35987 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 35988 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 35989 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 35990* | Sufficient condition to be a Moore collection. Note that there is no sethood hypothesis on 𝐴: it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021.) |
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-ismooredr2 35991* | Sufficient condition to be a Moore collection (variant of bj-ismooredr 35990 singling out the empty intersection). Note that there is no sethood hypothesis on 𝐴: it is a consequence of the first hypothesis. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-discrmoore 35992 | The powerclass 𝒫 𝐴 is a Moore collection if and only if 𝐴 is a set. It is then called the discrete Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore) | ||
Theorem | bj-0nmoore 35993 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 35994 | A singleton is a Moore collection. See bj-snmooreb 35995 for a biconditional version. (Contributed by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore) | ||
Theorem | bj-snmooreb 35995 | A singleton is a Moore collection, biconditional version. (Contributed by BJ, 9-Dec-2021.) (Proof shortened by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ∈ Moore) | ||
Theorem | bj-prmoore 35996 |
A pair formed of two nested sets is a Moore collection. (Note that in
the statement, if 𝐵 is a proper class, we are in the
case of
bj-snmoore 35994). A direct consequence is ⊢ {∅, 𝐴} ∈ Moore.
More generally, any nonempty well-ordered chain of sets that is a set is a Moore collection. We also have the biconditional ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → ({𝐴, 𝐵} ∈ Moore ↔ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))). (Contributed by BJ, 11-Apr-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore) | ||
Theorem | bj-0nelmpt 35997 | The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.) |
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | bj-mptval 35998 | Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌))) | ||
Theorem | bj-dfmpoa 35999* | An equivalent definition of df-mpo 7414. (Contributed by BJ, 30-Dec-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)} | ||
Theorem | bj-mpomptALT 36000* | Alternate proof of mpompt 7522. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |