P. 332 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33101-33200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-xtageq 33101	The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 × tag 𝐴) = (𝐶 × tag 𝐵))
Theorem	bj-xtagex 33102	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
20.14.5.13  Tuples of classes This subsection gives a definition of an ordered pair, or couple (2-tuple), which "works" for proper classes, as evidenced by Theorems bj-2uplth 33134 and bj-2uplex 33135 (but more importantly, bj-pr21val 33126 and bj-pr22val 33132). In particular, one can define well-behaved tuples of classes. Note, however, that classes in ZF(C) are only virtual, and in particular they cannot be quantified over. The projections are denoted by pr1 and pr2 and the couple with projections (or coordinates) 𝐴 and 𝐵 is denoted by ⦅𝐴, 𝐵⦆. Note that this definition uses the Kuratowksi definition (df-op 4217) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 8553) without needing the axiom of regularity; it could even bypass this definition by "inlining" it. This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986). Note that this extends in a natural way to tuples. A variation of this definition is justified in opthprc 5201, but here we use "tagged versions" of the factors (see df-bj-tag 33088) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same). A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397. where a recursive definition of tuples is given that avoids the 2-step definition of tuples and that can be adapted to various set theories. Finally, another survey is Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf)
Syntax	bj-cproj 33103	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 33104*	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 33105	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 33106	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 33107	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 33108	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 33109	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 33110	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆
Definition	df-bj-1upl 33111	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 33125, bj-2uplth 33134, bj-2uplex 33135, and the properties of the projections (see df-bj-pr1 33114 and df-bj-pr2 33128). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
Theorem	bj-1upleq 33112	Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆)
Syntax	bj-cpr1 33113	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 𝐴
Definition	df-bj-pr1 33114	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 33115, bj-pr11val 33118, bj-pr21val 33126, bj-pr1ex 33119. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ pr1 𝐴 = (∅ Proj 𝐴)
Theorem	bj-pr1eq 33115	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵)
Theorem	bj-pr1un 33116	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵)
Theorem	bj-pr1val 33117	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅)
Theorem	bj-pr11val 33118	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ⦅𝐴⦆ = 𝐴
Theorem	bj-pr1ex 33119	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V)
Theorem	bj-1uplth 33120	The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵)
Theorem	bj-1uplex 33121	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
Theorem	bj-1upln0 33122	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ ⦅𝐴⦆ ≠ ∅
Syntax	bj-c2uple 33123	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 33124	Definition of the Morse couple. See df-bj-1upl 33111. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 33125, bj-2uplth 33134, bj-2uplex 33135, and the properties of the projections (see df-bj-pr1 33114 and df-bj-pr2 33128). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))
Theorem	bj-2upleq 33125	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 33126	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 33127	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 33128	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 33129, bj-pr22val 33132, bj-pr2ex 33133. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1𝑜 Proj 𝐴)
Theorem	bj-pr2eq 33129	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 33130	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 33131	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1𝑜, 𝐵, ∅)
Theorem	bj-pr22val 33132	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵
Theorem	bj-pr2ex 33133	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V)
Theorem	bj-2uplth 33134	The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 4974). (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	bj-2uplex 33135	A couple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-2upln0 33136	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅
Theorem	bj-2upln1upl 33137	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 33122 and bj-2upln0 33136 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.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆
20.14.5.14  Set theory: miscellaneous Miscellaneous theorems of set theory.
Theorem	bj-disj2r 33138	Relative version of ssdifin0 4083, allowing a biconditional, and of disj2 4057. This proof does not rely, even indirectly, on ssdifin0 4083 nor disj2 4057. (Contributed by BJ, 11-Nov-2021.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 33139	Contraposition law for relative subsets. Relative and generalized version of ssconb 3776, which it can shorten, as well as conss2 38964. (Contributed by BJ, 11-Nov-2021.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
Theorem	bj-vjust2 33140	Justification theorem for bj-df-v 33141. See also vjust 3232 and bj-vjust 32911. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-df-v 33141	Alternate definition of the universal class. Actually, the current definition df-v 3233 should be proved from this one, and vex 3234 should be proved from this proposed definition together with bj-vexwv 32982, which would remove from vex 3234 dependency on ax-13 2282 (see also comment of bj-vexw 32980). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ V = {𝑥 ∣ ⊤}
Theorem	bj-df-nul 33142	Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = {𝑥 ∣ ⊥}
Theorem	bj-nul 33143*	Two formulations of the axiom of the empty set ax-nul 4822. Proposal: place it right before ax-nul 4822. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 33144*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 33145. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 33145*	Alternate proof of bj-nuliota 33144. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 5904). 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 33146	Alternate proof of vtoclgf 3295. Proof from vtoclgft 3285. (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-pwcfsdom 33147	Remove hypothesis from pwcfsdom 9443. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 9443.) (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 33148	Remove hypothesis from grur1 9680. 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)))
20.14.5.15  Evaluation
Theorem	bj-evaleq 33149	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 15909 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 33150	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 33151	The evaluation at a class is a function on the universal class. (General form of slotfn 15922). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalval 33152	Value of the evaluation at a class. (Closed form of strfvnd 15923 and strfvn 15926). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))
Theorem	bj-evalid 33153	The evaluation at a set of the identity function is that set. (General form of ndxarg 15929.) 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 33154	Proof of ndxarg 15929 from bj-evalid 33153. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	bj-ndxid 33155	Proof of ndxid 15930 from ndxarg 15929. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ 𝐸 = Slot (𝐸‘ndx)
Theorem	bj-evalidval 33156	Closed general form of strndxid 15932. Both sides are equal to (𝐹‘𝐴) by bj-evalid 33153 and bj-evalval 33152 respectively, but bj-evalidval 33156 adds something to bj-evalid 33153 and bj-evalval 33152 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹))
20.14.5.16  Elementwise operations
Syntax	celwise 33157	Syntax for elementwise operations.
class elwise
Definition	df-elwise 33158*	Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 10004), 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 ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))
20.14.5.17  Elementwise intersection (families of sets induced on a subset) Many kinds of structures are given by families of subsets of a given set: Moore collections (df-mre 16293), topologies (df-top 20747), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 30299), 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* /J
Theorem	bj-rest00 33159	An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 16137. (Contributed by BJ, 27-Apr-2021.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	bj-restsn 33160	An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 33163 and bj-restsnid 33165. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)})
Theorem	bj-restsnss 33161	Special case of bj-restsn 33160. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴})
Theorem	bj-restsnss2 33162	Special case of bj-restsn 33160. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌})
Theorem	bj-restsn0 33163	An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 33160 and bj-restsnss2 33162. TODO: this is restsn 21022. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	bj-restsn10 33164	Special case of bj-restsn 33160, bj-restsnss 33161, and bj-rest10 33166. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅})
Theorem	bj-restsnid 33165	The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 33160 and bj-restsnss 33161. (Contributed by BJ, 27-Apr-2021.)
⊢ ({𝐴} ↾t 𝐴) = {𝐴}
Theorem	bj-rest10 33166	An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 21021 and could replace it. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅}))
Theorem	bj-rest10b 33167	Alternate version of bj-rest10 33166. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅})
Theorem	bj-restn0 33168	An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅))
Theorem	bj-restn0b 33169	Alternate version of bj-restn0 33168. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅)
Theorem	bj-restpw 33170	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 21030 (which uses distop 20847 and restopn2 21029). (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴))
Theorem	bj-rest0 33171	An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴)))
Theorem	bj-restb 33172	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 33173	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 33174	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 33175	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 21014 and restuni2 21019. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴))
Theorem	bj-restuni2 33176	The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 21014 and restuni2 21019. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴)
Theorem	bj-restreg 33177	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 𝐴))
20.14.5.18  Moore collections (complements)
Theorem	bj-intss 33178	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 33179*	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 33180*	If 𝐴 is a collection of subsets of 𝑋, like a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵 (in typical applications, 𝐴 itself). (Contributed by BJ, 7-Dec-2021.)
⊢ (𝐴 ⊆ 𝒫 𝑋 → ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∩ 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 ∩ ∩ 𝑥) ∈ 𝐵))
Theorem	bj-mooreset 33181*	A Moore collection is a set. That is, if we define a "Moore predicate" by (Moore𝐴 ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴), then any class satisfying that predicate is actually a set. Therefore, the definition df-bj-moore 33183 is sufficient. Note that the closed sets of a topology form a Moore collection, so this remark also applies to topologies and many other families of sets (namely, as soon as the whole set is required to be a closed set, as can be seen from the proof, which relies crucially on uniexr 7014). 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 ∪ 𝒫 𝑋 = 𝑋, making 𝒫 𝑋 a Moore collection in this weaker sense, even if 𝑋 is a proper class, but the addition of this single case does not add anything interesting. (Contributed by BJ, 8-Dec-2021.)
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V)
Syntax	cmoore 33182	Syntax for the class of Moore collections.
class Moore
Definition	df-bj-moore 33183*	Define the class of Moore collections. This is to df-mre 16293 what df-top 20747 is to df-topon 20764. For the sake of consistency, the function defined at df-mre 16293 should be denoted by "MooreOn". Note: df-mre 16293 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 33180. 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 33181). (Contributed by BJ, 27-Apr-2021.)
⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥}
Theorem	bj-ismoore 33184*	Characterization of Moore collections among sets. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
Theorem	bj-ismoorec 33185*	Characterization of Moore collections. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
Theorem	bj-ismoored0 33186	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴)
Theorem	bj-ismoored 33187	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴)
Theorem	bj-ismoored2 33188	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴)
Theorem	bj-ismooredr 33189*	Sufficient condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ Moore)
Theorem	bj-ismooredr2 33190*	Sufficient condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)    &   ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ Moore)
Theorem	bj-discrmoore 33191	The discrete Moore collection on a set. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore)
Theorem	bj-0nmoore 33192	The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ ¬ ∅ ∈ Moore
Theorem	bj-snmoore 33193	A singleton is a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ V ↔ {𝐴} ∈ Moore)
20.14.5.19  Maps-to notation for functions with three arguments
Theorem	bj-0nelmpt 33194	The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.)
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	bj-mptval 33195	Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌)))
Theorem	bj-dfmpt2a 33196*	An equivalent definition of df-mpt2 6695. (Contributed by BJ, 30-Dec-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)}
Theorem	bj-mpt2mptALT 33197*	Alternate proof of mpt2mpt 6794. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Syntax	cmpt3 33198	Extend the definition of a class to include maps-to notation for functions with three arguments.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
Definition	df-bj-mpt3 33199*	Define maps-to notation for functions with three arguments. See df-mpt 4763 and df-mpt2 6695 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpt2a 33196. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
20.14.5.20  Currying Currying and uncurrying. See also df-cur and df-unc 7439. Contrary to these, the definitions in this section are parameterized.
Syntax	csethom 33200	Syntax for the set of set morphisms.
class Set⟶