![]() |
Metamath
Proof Explorer Theorem List (p. 371 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-pr22val 37001 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 | ||
Theorem | bj-pr2ex 37002 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
Theorem | bj-2uplth 37003 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5486). (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | bj-2uplex 37004 | 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 37005 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
Theorem | bj-2upln1upl 37006 | 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 36991 and bj-2upln0 37005 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 37007 | Relative version of cleqf 2931. (Contributed by BJ, 27-Dec-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-rcleq 37008* | Relative version of dfcleq 2727. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-reabeq 37009* | Relative form of eqabb 2878. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-disj2r 37010 | Relative version of ssdifin0 4491, allowing a biconditional, and of disj2 4463. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4491 nor disj2 4463. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅) | ||
Theorem | bj-sscon 37011 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4151, which it can shorten, as well as conss2 44438. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4151 nor conss2 44438. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
In this section, we introduce the axiom of singleton ax-bj-sn 37015 and the axiom of binary union ax-bj-bun 37019. Both axioms are implied by the standard axioms of unordered pair ax-pr 5437 and of union ax-un 7753 (see snex 5441 and unex 7762). Conversely, the axiom of unordered pair ax-pr 5437 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37021 and bj-prex 37022. The axioms of union ax-un 7753 and of powerset ax-pow 5370 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 5370 and https://mathoverflow.net/questions/48365 5370. 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 5311). The axiom of binary union is useful in theories without the axioms of union ax-un 7753 and of powerset ax-pow 5370. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2705, ax-rep 5284, ax-sep 5301, ax-nul 5311, ax-reg 9629 } 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 37024 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 37028 and conversely how to prove from adjunction singleton (bj-snfromadj 37026) and unordered pair (bj-prfromadj 37027). | ||
Theorem | bj-abex 37012* | 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 37013* | Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-axsn 37014* | Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37015). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)) | ||
Axiom | ax-bj-sn 37015* | Axiom of singleton. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) | ||
Theorem | bj-snexg 37016 | A singleton built on a set is a set. Contrary to bj-snex 37017, this proof is intuitionistically valid and does not require ax-nul 5311. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5441 and prove it from ax-bj-sn 37015. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | bj-snex 37017 | A singleton is a set. See also snex 5441, snexALT 5388. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37015. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴} ∈ V | ||
Theorem | bj-axbun 37018* | Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37019). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))) | ||
Axiom | ax-bj-bun 37019* | Axiom of binary union. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) | ||
Theorem | bj-unexg 37020 | Existence of binary unions of sets, proved from ax-bj-bun 37019. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-prexg 37021 | Existence of unordered pairs formed on sets, proved from ax-bj-sn 37015 and ax-bj-bun 37019. Contrary to bj-prex 37022, this proof is intuitionistically valid and does not require ax-nul 5311. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | bj-prex 37022 | Existence of unordered pairs proved from ax-bj-sn 37015 and ax-bj-bun 37019. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | bj-axadj 37023* | Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37024). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))) | ||
Axiom | ax-bj-adj 37024* | Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)) | ||
Theorem | bj-adjg1 37025 | 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 37026 | Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥} ∈ V | ||
Theorem | bj-prfromadj 37027 | Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | bj-adjfrombun 37028 | Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∪ {𝑦}) ∈ V | ||
Miscellaneous theorems of set theory. | ||
Theorem | eleq2w2ALT 37029 | Alternate proof of eleq2w2 2730 and special instance of eleq2 2827. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-clel3gALT 37030* | Alternate proof of clel3g 3660. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | bj-pw0ALT 37031 | 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 37031 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4816 and biconditional for bj-pw0ALT 37031) to translate the property ss0b 4406 into the wanted result. To translate a biconditional into a class equality, pw0 4816 uses abbii 2806 (which yields an equality of class abstractions), while bj-pw0ALT 37031 uses eqriv 2731 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2806, through its closed form abbi 2804, is proved from eqrdv 2732, which is the deduction form of eqriv 2731. In the other direction, velpw 4609 and velsn 4646 are proved from the definitions of powerclass and singleton using elabg 3676, which is a version of abbii 2806 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 ∅ = {∅} | ||
Theorem | bj-sselpwuni 37032 | Quantitative version of ssexg 5328: 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 37033 | Quantitative version of uniexr 7781: 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 37034 | 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 4607 and elpw2g 5338 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-velpwALT 37035* | This theorem bj-velpwALT 37035 and the next theorem bj-elpwgALT 37036 are alternate proofs of velpw 4609 and elpwg 4607 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3556 instead of proving first the general case using elab2g 3682 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2174. In other cases, that order is better (e.g., vsnex 5439 proved before snexg 5440). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | bj-elpwgALT 37036 | Alternate proof of elpwg 4607. See comment for bj-velpwALT 37035. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-vjust 37037 | Justification theorem for dfv2 3480 if it were the definition. See also vjust 3478. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
Theorem | bj-nul 37038* | Two formulations of the axiom of the empty set ax-nul 5311. Proposal: place it right before ax-nul 5311. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliota 37039* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37040. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliotaALT 37040* | Alternate proof of bj-nuliota 37039. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6540). 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 37041 | Alternate proof of vtoclgf 3568. Proof from vtoclgft 3551. (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 37042 | Join of elsng 4644 and elsn2g 4668. (Contributed by BJ, 18-Nov-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-elsnb 37043 | Biconditional version of elsng 4644. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-pwcfsdom 37044 | Remove hypothesis from pwcfsdom 10620. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 10620.) (Contributed by BJ, 14-Sep-2019.) |
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
Theorem | bj-grur1 37045 | Remove hypothesis from grur1 10857. 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 37046* |
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 5301.
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 after sepexi 5306. Relabel ("sepbi"?). |
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-dfid2ALT 37047 | Alternate version of dfid2 5584. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5582 instead to make the semantics of the construction df-opab 5210 clearer. (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑥〉 ∣ ⊤} | ||
Theorem | bj-0nelopab 37048 |
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 5836 (this is a very limited reordering). |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | bj-brrelex12ALT 37049 | Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5740. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-epelg 37050 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5591 and closed form of epeli 5590. (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 5744 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | bj-epelb 37051 | 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 5745 available. Check if it is shorter to prove bj-epelg 37050 first or bj-epelb 37051 first. (Contributed by BJ, 14-Jul-2023.) |
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) | ||
Theorem | bj-nsnid 37052 | 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 4721): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴) | ||
Theorem | bj-rdg0gALT 37053 | Alternate proof of rdg0g 8465. More direct since it bypasses tz7.44-1 8444 and rdg0 8459 (and vtoclg 3553, vtoclga 3576). (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 17215) as "evaluation at a class" and for the moment does not introduce new syntax for it. | ||
Theorem | bj-evaleq 37054 | Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17216 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 37055 | The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.) |
⊢ Fun Slot 𝐴 | ||
Theorem | bj-evalfn 37056 | The evaluation at a class is a function on the universal class. (General form of slotfn 17217). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.) |
⊢ Slot 𝐴 Fn V | ||
Theorem | bj-evalval 37057 | Value of the evaluation at a class. (Closed form of strfvnd 17218 and strfvn 17219). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.) |
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | bj-evalid 37058 | The evaluation at a set of the identity function is that set. (General form of ndxarg 17229.) 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 37059 | Proof of ndxarg 17229 from bj-evalid 37058. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | bj-evalidval 37060 | Closed general form of strndxid 17231. Both sides are equal to (𝐹‘𝐴) by bj-evalid 37058 and bj-evalval 37057 respectively, but bj-evalidval 37060 adds something to bj-evalid 37058 and bj-evalval 37057 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
Syntax | celwise 37061 | Syntax for elementwise operations. |
class elwise | ||
Definition | df-elwise 37062* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11182), 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 17630), topologies (df-top 22915), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34089), 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 37063 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17475. (Contributed by BJ, 27-Apr-2021.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | bj-restsn 37064 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 37067 and bj-restsnid 37069. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
Theorem | bj-restsnss 37065 | Special case of bj-restsn 37064. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
Theorem | bj-restsnss2 37066 | Special case of bj-restsn 37064. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
Theorem | bj-restsn0 37067 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 37064 and bj-restsnss2 37066. TODO: this is restsn 23193. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | bj-restsn10 37068 | Special case of bj-restsn 37064, bj-restsnss 37065, and bj-rest10 37070. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 37069 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 37064 and bj-restsnss 37065. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 37070 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23192 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 37071 | Alternate version of bj-rest10 37070. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 37072 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 37073 | Alternate version of bj-restn0 37072. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 37074 | 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 23201 (which uses distop 23017 and restopn2 23200). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 37075 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 37076 | 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 37077 | 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 37078 | 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 37079 | 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 23185 and restuni2 23190. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 37080 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 23185 and restuni2 23190. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 37081 | 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 37082* | 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 37083* | 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 37084* |
A Moore collection is a set. Therefore, the class Moore of all
Moore sets defined in df-bj-moore 37086 is actually the class of all Moore
collections. This is also illustrated by the lack of sethood condition
in bj-ismoore 37087.
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 7781). 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 5460), 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 37093. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 37085 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 37086* |
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 37084,
and as illustrated by the lack of sethood condition in bj-ismoore 37087.
This is to df-mre 17630 (defining Moore) what df-top 22915 (defining Top) is to df-topon 22932 (defining TopOn). For the sake of consistency, the function defined at df-mre 17630 should be denoted by "MooreOn". Note: df-mre 17630 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 37083. 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 37084). 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 17630 and df-topon 22932) or the class of all families of that kind, independent of a base set (like df-bj-moore 37086 or df-top 22915). 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 37087* | 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 37084 for the RHS). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) | ||
Theorem | bj-ismoored0 37088 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 37089 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 37090 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 37091* | 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 37092* | Sufficient condition to be a Moore collection (variant of bj-ismooredr 37091 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 37093 | 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 37094 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 37095 | A singleton is a Moore collection. See bj-snmooreb 37096 for a biconditional version. (Contributed by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore) | ||
Theorem | bj-snmooreb 37096 | 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 37097 |
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 37095). 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 37098 | The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.) |
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | bj-mptval 37099 | Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌))) | ||
Theorem | bj-dfmpoa 37100* | An equivalent definition of df-mpo 7435. (Contributed by BJ, 30-Dec-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = 〈𝑥, 𝑦〉 ∧ 𝑡 = 𝐶)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |