Home | Metamath
Proof Explorer Theorem List (p. 343 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-bj-proj 34201* | Definition of the class projection corresponding to tagged tuples. The expression (𝐴 Proj 𝐵) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})} | ||
Theorem | bj-projeq 34202 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷))) | ||
Theorem | bj-projeq2 34203 | Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶)) | ||
Theorem | bj-projun 34204 | The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶)) | ||
Theorem | bj-projex 34205 | Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V) | ||
Theorem | bj-projval 34206 | Value of the class projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅)) | ||
Syntax | bj-c1upl 34207 | Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.) |
class ⦅𝐴⦆ | ||
Definition | df-bj-1upl 34208 | Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. Note that with this definition, the 0-tuple is the empty set. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 34222, bj-2uplth 34231, bj-2uplex 34232, and the properties of the projections (see df-bj-pr1 34211 and df-bj-pr2 34225). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴) | ||
Theorem | bj-1upleq 34209 | Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆) | ||
Syntax | bj-cpr1 34210 | Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.) |
class pr1 𝐴 | ||
Definition | df-bj-pr1 34211 | Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq 34212, bj-pr11val 34215, bj-pr21val 34223, bj-pr1ex 34216. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
⊢ pr1 𝐴 = (∅ Proj 𝐴) | ||
Theorem | bj-pr1eq 34212 | Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵) | ||
Theorem | bj-pr1un 34213 | The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵) | ||
Theorem | bj-pr1val 34214 | Value of the first projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅) | ||
Theorem | bj-pr11val 34215 | Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr1 ⦅𝐴⦆ = 𝐴 | ||
Theorem | bj-pr1ex 34216 | Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V) | ||
Theorem | bj-1uplth 34217 | The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵) | ||
Theorem | bj-1uplex 34218 | A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.) |
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V) | ||
Theorem | bj-1upln0 34219 | A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ ⦅𝐴⦆ ≠ ∅ | ||
Syntax | bj-c2uple 34220 | Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.) |
class ⦅𝐴, 𝐵⦆ | ||
Definition | df-bj-2upl 34221 | Definition of the Morse couple. See df-bj-1upl 34208. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 34222, bj-2uplth 34231, bj-2uplex 34232, and the properties of the projections (see df-bj-pr1 34211 and df-bj-pr2 34225). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) | ||
Theorem | bj-2upleq 34222 | Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆)) | ||
Theorem | bj-pr21val 34223 | Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴 | ||
Syntax | bj-cpr2 34224 | Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.) |
class pr2 𝐴 | ||
Definition | df-bj-pr2 34225 | Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 34226, bj-pr22val 34229, bj-pr2ex 34230. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ pr2 𝐴 = (1o Proj 𝐴) | ||
Theorem | bj-pr2eq 34226 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) | ||
Theorem | bj-pr2un 34227 | The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵) | ||
Theorem | bj-pr2val 34228 | Value of the second projection. (Contributed by BJ, 6-Apr-2019.) |
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅) | ||
Theorem | bj-pr22val 34229 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 | ||
Theorem | bj-pr2ex 34230 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
Theorem | bj-2uplth 34231 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5360). (Contributed by BJ, 6-Oct-2018.) |
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | bj-2uplex 34232 | 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 34233 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
Theorem | bj-2upln1upl 34234 | 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 34219 and bj-2upln0 34233 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 34235 | Relative version of cleqf 3010. (Contributed by BJ, 27-Dec-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-rcleq 34236* | Relative version of dfcleq 2815. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | bj-reabeq 34237* | Relative form of abeq2 2945. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-disj2r 34238 | Relative version of ssdifin0 4429, allowing a biconditional, and of disj2 4405. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4429 nor disj2 4405. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅) | ||
Theorem | bj-sscon 34239 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4113, which it can shorten, as well as conss2 40655. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4113 nor conss2 40655. (Proof modification is discouraged.) |
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
Miscellaneous theorems of set theory. | ||
Theorem | bj-elpwg 34240 | 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 4543 and elpw2g 5239 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | bj-vjust 34241 | Justification theorem for bj-df-v 34242. See also vjust 3496. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
Theorem | bj-df-v 34242 | Alternate definition of the universal class. Actually, the current definition df-v 3497 should be proved from this one, and vex 3498 should be proved from this proposed definition together with vexw 2805, which would remove from vex 3498 dependency on ax-13 2383 (see also comment of vexw 2805). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ V = {𝑥 ∣ ⊤} | ||
Theorem | bj-df-nul 34243 | Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = {𝑥 ∣ ⊥} | ||
Theorem | bj-nul 34244* | Two formulations of the axiom of the empty set ax-nul 5202. Proposal: place it right before ax-nul 5202. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliota 34245* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 34246. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | bj-nuliotaALT 34246* | Alternate proof of bj-nuliota 34245. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6327). 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 34247 | Alternate proof of vtoclgf 3566. Proof from vtoclgft 3554. (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 34248 | Join of elsng 4573 and elsn2g 4595. (Contributed by BJ, 18-Nov-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-elsnb 34249 | Biconditional version of elsng 4573. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-pwcfsdom 34250 | Remove hypothesis from pwcfsdom 9994. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 9994.) (Contributed by BJ, 14-Sep-2019.) |
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
Theorem | bj-grur1 34251 | Remove hypothesis from grur1 10231. 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 34252* |
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 5195.
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 5198. Relabel ("sepbi"?). |
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) | ||
Theorem | bj-0nelopab 34253 |
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 5690 (this is a very limited reordering). |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | bj-brrelex12ALT 34254 | Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5598. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-epelg 34255 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5463 and closed form of epeli 5462. (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 5602 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | bj-epelb 34256 | 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 5603 available. Check if it is shorter to prove bj-epelg 34255 first or bj-epelb 34256 first. (Contributed by BJ, 14-Jul-2023.) |
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) | ||
Theorem | bj-nsnid 34257 | 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 4647): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴) | ||
This section treats the existing predicate Slot (df-slot 16477) as "evaluation at a class" and for the moment does not introduce new syntax for it. | ||
Theorem | bj-evaleq 34258 | Equality theorem for the Slot construction. This is currently a duplicate of sloteq 16478 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 34259 | The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.) |
⊢ Fun Slot 𝐴 | ||
Theorem | bj-evalfn 34260 | The evaluation at a class is a function on the universal class. (General form of slotfn 16491). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.) |
⊢ Slot 𝐴 Fn V | ||
Theorem | bj-evalval 34261 | Value of the evaluation at a class. (Closed form of strfvnd 16492 and strfvn 16495). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.) |
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | bj-evalid 34262 | The evaluation at a set of the identity function is that set. (General form of ndxarg 16498.) 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 34263 | Proof of ndxarg 16498 from bj-evalid 34262. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | bj-evalidval 34264 | Closed general form of strndxid 16500. Both sides are equal to (𝐹‘𝐴) by bj-evalid 34262 and bj-evalval 34261 respectively, but bj-evalidval 34264 adds something to bj-evalid 34262 and bj-evalval 34261 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
Syntax | celwise 34265 | Syntax for elementwise operations. |
class elwise | ||
Definition | df-elwise 34266* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 10556), 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 16847), topologies (df-top 21432), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 31268), 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 34267 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 16693. (Contributed by BJ, 27-Apr-2021.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | bj-restsn 34268 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 34271 and bj-restsnid 34273. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
Theorem | bj-restsnss 34269 | Special case of bj-restsn 34268. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
Theorem | bj-restsnss2 34270 | Special case of bj-restsn 34268. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
Theorem | bj-restsn0 34271 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 34268 and bj-restsnss2 34270. TODO: this is restsn 21708. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | bj-restsn10 34272 | Special case of bj-restsn 34268, bj-restsnss 34269, and bj-rest10 34274. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 34273 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 34268 and bj-restsnss 34269. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 34274 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 21707 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 34275 | Alternate version of bj-rest10 34274. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 34276 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 34277 | Alternate version of bj-restn0 34276. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 34278 | 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 21716 (which uses distop 21533 and restopn2 21715). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 34279 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 34280 | 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 34281 | 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 34282 | 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 34283 | 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 21700 and restuni2 21705. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 34284 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 21700 and restuni2 21705. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 34285 | 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-intss 34286 | A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋)) | ||
Theorem | bj-raldifsn 34287* | 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 34288* | 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 34289* |
A Moore collection is a set. Therefore, the class Moore of all
Moore sets defined in df-bj-moore 34291 is actually the class of all Moore
collections. This is also illustrated by the lack of sethood condition
in bj-ismoore 34292.
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 7473). 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 5334) , 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 34298. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 34290 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 34291* |
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 34289,
and as illustrated by the lack of sethood condition in bj-ismoore 34292.
This is to df-mre 16847 (defining Moore) what df-top 21432 (defining Top) is to df-topon 21449 (defining TopOn). For the sake of consistency, the function defined at df-mre 16847 should be denoted by "MooreOn". Note: df-mre 16847 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 34288. 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 34289). 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 16847 and df-topon 21449) or the class of all families of that kind, independent of a base set (like df-bj-moore 34291 or df-top 21432). 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 34292* | 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 34289 for the RHS). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) | ||
Theorem | bj-ismoored0 34293 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 34294 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 34295 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 34296* | 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 34297* | Sufficient condition to be a Moore collection (variant of bj-ismooredr 34296 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 34298 | 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 34299 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 34300 |
A singleton is a Moore collection. Since the empty set is not a Moore
collection (bj-0nmoore 34299), we can state the present theorem as a
biconditional.
TODO: A two-element set is a Moore collection if and only if (exactly) one of them is the empty set. That is, ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ∈ Moore ↔ ¬ (𝐴 = ∅ ↔ 𝐵 = ∅))). Because the empty set is not a Moore collection (bj-0nmoore 34299) and a singleton is a Moore collection (bj-snmoore 34300), this can also be stated as ⊢ ({𝐴, 𝐵} ∈ Moore ↔ ¬ (𝐴 ∈ (V ∖ {∅}) ↔ 𝐵 ∈ (V ∖ {∅}))). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ∈ Moore) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |