![]() |
Metamath
Proof Explorer Theorem List (p. 363 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-pr2eq 36201 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) | ||
Theorem | bj-pr2un 36202 | The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵) | ||
Theorem | bj-pr2val 36203 | Value of the second projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅) | ||
Theorem | bj-pr22val 36204 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 | ||
Theorem | bj-pr2ex 36205 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
Theorem | bj-2uplth 36206 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5477). (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | bj-2uplex 36207 | 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 36208 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
Theorem | bj-2upln1upl 36209 | 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 36194 and bj-2upln0 36208 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 36210 | Relative version of cleqf 2933. (Contributed by BJ, 27-Dec-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-rcleq 36211* | Relative version of dfcleq 2724. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-reabeq 36212* | Relative form of eqabb 2872. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-disj2r 36213 | 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 36214 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4138, which it can shorten, as well as conss2 43505. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4138 nor conss2 43505. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
In this section, we introduce the axiom of singleton ax-bj-sn 36218 and the axiom of binary union ax-bj-bun 36222. Both axioms are implied by the standard axioms of unordered pair ax-pr 5428 and of union ax-un 7728 (see snex 5432 and unex 7736). 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 36224 and bj-prex 36225. The axioms of union ax-un 7728 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 7728 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 2702, ax-rep 5286, ax-sep 5300, ax-nul 5307, ax-reg 9590 } 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 36227 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 36231 and conversely how to prove from adjunction singleton (bj-snfromadj 36229) and unordered pair (bj-prfromadj 36230). | ||
Theorem | bj-abex 36215* | 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 36216* | Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-axsn 36217* | Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 36218). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)) | ||
Axiom | ax-bj-sn 36218* | Axiom of singleton. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) | ||
Theorem | bj-snexg 36219 | A singleton built on a set is a set. Contrary to bj-snex 36220, 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 36218. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | bj-snex 36220 | A singleton is a set. See also snex 5432, snexALT 5382. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 36218. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴} ∈ V | ||
Theorem | bj-axbun 36221* | Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 36222). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))) | ||
Axiom | ax-bj-bun 36222* | Axiom of binary union. (Contributed by BJ, 12-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) | ||
Theorem | bj-unexg 36223 | Existence of binary unions of sets, proved from ax-bj-bun 36222. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-prexg 36224 | Existence of unordered pairs formed on sets, proved from ax-bj-sn 36218 and ax-bj-bun 36222. Contrary to bj-prex 36225, 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 36225 | Existence of unordered pairs proved from ax-bj-sn 36218 and ax-bj-bun 36222. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | bj-axadj 36226* | Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 36227). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))) | ||
Axiom | ax-bj-adj 36227* | Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.) |
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)) | ||
Theorem | bj-adjg1 36228 | 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 36229 | Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥} ∈ V | ||
Theorem | bj-prfromadj 36230 | Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | bj-adjfrombun 36231 | Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
⊢ (𝑥 ∪ {𝑦}) ∈ V | ||
Miscellaneous theorems of set theory. | ||
Theorem | eleq2w2ALT 36232 | Alternate proof of eleq2w2 2727 and special instance of eleq2 2821. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-clel3gALT 36233* | Alternate proof of clel3g 3651. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | bj-pw0ALT 36234 | 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 36234 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4816 and biconditional for bj-pw0ALT 36234) to translate the property ss0b 4398 into the wanted result. To translate a biconditional into a class equality, pw0 4816 uses abbii 2801 (which yields an equality of class abstractions), while bj-pw0ALT 36234 uses eqriv 2728 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2801, through its closed form abbi 2799, is proved from eqrdv 2729, which is the deduction form of eqriv 2728. 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 2801 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 ∅ = {∅} | ||
Theorem | bj-sselpwuni 36235 | 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 36236 | Quantitative version of uniexr 7753: 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 36237 | 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 36238* | This theorem bj-velpwALT 36238 and the next theorem bj-elpwgALT 36239 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 2170. 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 36239 | Alternate proof of elpwg 4606. See comment for bj-velpwALT 36238. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-vjust 36240 | Justification theorem for dfv2 3476 if it were the definition. See also vjust 3474. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
Theorem | bj-nul 36241* | 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 36242* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 36243. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliotaALT 36243* | Alternate proof of bj-nuliota 36242. 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 36244 | Alternate proof of vtoclgf 3555. Proof from vtoclgft 3540. (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 36245 | Join of elsng 4643 and elsn2g 4667. (Contributed by BJ, 18-Nov-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-elsnb 36246 | Biconditional version of elsng 4643. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-pwcfsdom 36247 | Remove hypothesis from pwcfsdom 10581. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 10581.) (Contributed by BJ, 14-Sep-2019.) |
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
Theorem | bj-grur1 36248 | Remove hypothesis from grur1 10818. 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 36249* |
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 36250 | 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 36251 |
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 36252 | 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 36253 | 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 36254 | 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 36253 first or bj-epelb 36254 first. (Contributed by BJ, 14-Jul-2023.) |
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) | ||
Theorem | bj-nsnid 36255 | 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 36256 | Alternate proof of rdg0g 8430. More direct since it bypasses tz7.44-1 8409 and rdg0 8424 (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 17120) as "evaluation at a class" and for the moment does not introduce new syntax for it. | ||
Theorem | bj-evaleq 36257 | Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17121 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 36258 | The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.) |
⊢ Fun Slot 𝐴 | ||
Theorem | bj-evalfn 36259 | The evaluation at a class is a function on the universal class. (General form of slotfn 17122). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.) |
⊢ Slot 𝐴 Fn V | ||
Theorem | bj-evalval 36260 | Value of the evaluation at a class. (Closed form of strfvnd 17123 and strfvn 17124). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.) |
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | bj-evalid 36261 | The evaluation at a set of the identity function is that set. (General form of ndxarg 17134.) 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 36262 | Proof of ndxarg 17134 from bj-evalid 36261. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | bj-evalidval 36263 | Closed general form of strndxid 17136. Both sides are equal to (𝐹‘𝐴) by bj-evalid 36261 and bj-evalval 36260 respectively, but bj-evalidval 36263 adds something to bj-evalid 36261 and bj-evalval 36260 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
Syntax | celwise 36264 | Syntax for elementwise operations. |
class elwise | ||
Definition | df-elwise 36265* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11143), 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 17535), topologies (df-top 22617), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 33402), 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 36266 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17380. (Contributed by BJ, 27-Apr-2021.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | bj-restsn 36267 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 36270 and bj-restsnid 36272. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
Theorem | bj-restsnss 36268 | Special case of bj-restsn 36267. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
Theorem | bj-restsnss2 36269 | Special case of bj-restsn 36267. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
Theorem | bj-restsn0 36270 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 36267 and bj-restsnss2 36269. TODO: this is restsn 22895. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | bj-restsn10 36271 | Special case of bj-restsn 36267, bj-restsnss 36268, and bj-rest10 36273. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 36272 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 36267 and bj-restsnss 36268. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 36273 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 22894 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 36274 | Alternate version of bj-rest10 36273. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 36275 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 36276 | Alternate version of bj-restn0 36275. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 36277 | 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 22903 (which uses distop 22719 and restopn2 22902). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 36278 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 36279 | 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 36280 | 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 36281 | 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 36282 | 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 22887 and restuni2 22892. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 36283 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 22887 and restuni2 22892. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 36284 | 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 36285* | 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 36286* | 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 36287* |
A Moore collection is a set. Therefore, the class Moore of all
Moore sets defined in df-bj-moore 36289 is actually the class of all Moore
collections. This is also illustrated by the lack of sethood condition
in bj-ismoore 36290.
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 7753). 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 36296. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 36288 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 36289* |
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 36287,
and as illustrated by the lack of sethood condition in bj-ismoore 36290.
This is to df-mre 17535 (defining Moore) what df-top 22617 (defining Top) is to df-topon 22634 (defining TopOn). For the sake of consistency, the function defined at df-mre 17535 should be denoted by "MooreOn". Note: df-mre 17535 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 36286. 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 36287). 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 17535 and df-topon 22634) or the class of all families of that kind, independent of a base set (like df-bj-moore 36289 or df-top 22617). 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 36290* | 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 36287 for the RHS). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) | ||
Theorem | bj-ismoored0 36291 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 36292 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 36293 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 36294* | 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 36295* | Sufficient condition to be a Moore collection (variant of bj-ismooredr 36294 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 36296 | 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 36297 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 36298 | A singleton is a Moore collection. See bj-snmooreb 36299 for a biconditional version. (Contributed by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore) | ||
Theorem | bj-snmooreb 36299 | 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 36300 |
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 36298). 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |