P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-axadj 37401*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37402). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37402*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37403	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 37404	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 37405	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 37406	Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∪ {𝑦}) ∈ V
21.19.5.18  Set theory: miscellaneous Miscellaneous theorems of set theory.
Theorem	eleq2w2ALT 37407	Alternate proof of eleq2w2 2736 and special instance of eleq2 2829. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-clel3gALT 37408*	Alternate proof of clel3g 3606. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 37409	Alternate proof of pw0 4750. The proofs have a similar structure: pw0 4750 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37409 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4750 and biconditional for bj-pw0ALT 37409) to translate the property ss0b 4336 into the wanted result. To translate a biconditional into a class equality, pw0 4750 uses abbii 2807 (which yields an equality of class abstractions), while bj-pw0ALT 37409 uses eqriv 2737 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2807, through its closed form abbi 2805, is proved from eqrdv 2738, which is the deduction form of eqriv 2737. In the other direction, velpw 4541 and velsn 4578 are proved from the definitions of powerclass and singleton using elabg 3621, which is a version of abbii 2807 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝒫 ∅ = {∅}
Theorem	bj-sselpwuni 37410	Quantitative version of ssexg 5258: 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 37411	Quantitative version of uniexr 7713: 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 37412	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 4539 and elpw2g 5268 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 37413*	This theorem bj-velpwALT 37413 and the next theorem bj-elpwgALT 37414 are alternate proofs of velpw 4541 and elpwg 4539 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3505 instead of proving first the general case using elab2g 3625 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2189. In other cases, that order is better (e.g., vsnex 5371 proved before snexg 5376). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 37414	Alternate proof of elpwg 4539. See comment for bj-velpwALT 37413. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 37415	Justification theorem for dfv2 3435 if it were the definition. See also vjust 3433. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 37416*	Two formulations of the axiom of the empty set ax-nul 5235. Proposal: place it right before ax-nul 5235. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 37417*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37418. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 37418*	Alternate proof of bj-nuliota 37417. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6472). 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 37419	Alternate proof of vtoclgf 3516. Proof from vtoclgft 3500. (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 37420	Join of elsng 4576 and elsn2g 4603. (Contributed by BJ, 18-Nov-2023.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-elsnb 37421	Biconditional version of elsng 4576. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-pwcfsdom 37422	Remove hypothesis from pwcfsdom 10504. Illustration of how to remove a "proof-facilitating hypothesis". Shortens theorems using pwcfsdom 10504. (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 37423	Remove hypothesis from grur1 10741. 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 37424*	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 5225. 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 5230. Relabel ("sepbi"?).
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-dfid2ALT 37425	Alternate version of dfid2 5522. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5520 instead to make the semantics of the construction df-opab 5142 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
Theorem	bj-0nelopab 37426	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 5774 (this is a very limited reordering).
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	bj-brrelex12ALT 37427	Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5677. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-epelg 37428	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5528 and closed form of epeli 5527. (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 5681 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	bj-epelb 37429	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 5682 available. Check if it is shorter to prove bj-epelg 37428 first or bj-epelb 37429 first. (Contributed by BJ, 14-Jul-2023.)
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
Theorem	bj-nsnid 37430	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 4656): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.)
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴)
Theorem	bj-rdg0gALT 37431	Alternate proof of rdg0g 8363. More direct since it bypasses tz7.44-1 8342 and rdg0 8357 (and vtoclg 3502, vtoclga 3523). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
21.19.5.19  Axioms of separation and replacement This section proves basic relations among some standard axioms of set theory, in particular the axiom of separation (the universal closure of ax-sep 5225) and the version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function, bj-rep 37433. These axioms often appear (as specific instances) in the hypotheses of the theorems in this section.
Theorem	bj-axnul 37432*	Over the base theory ax-1 6-- ax-5 1917, the axiom of separation implies the weak emptyset axiom. By "weak emptyset axiom", we mean the axiom asserting existence of an empty set (which can be called "the" empty set when the axiom of extensionality ax-ext 2712 is posited) provided existence of a set (the True truth constant existentially quantified over a fresh variable, extru 1982). This is the conclusion of bj-axnul 37432. Note that the weak emptyset axiom implies ⊢ (∃𝑥⊤ → ∃𝑦⊤) without DV conditions hence also the same statement as the weak emptyset axiom without DV conditions on 𝑥, but only on 𝑦, 𝑧. By "axiom of separation", we mean the universal closure of ax-sep 5225, simulated here by its instance with ⊥ substituted for 𝜑 (and with the variable used to assert existence in the weak emptyset axiom substituted for the containing set) as the hypothesis of bj-axnul 37432. In particular, the axiom of existence extru 1982 and the axiom of separation together imply the emptyset axiom (and conversely, the emptyset axiom implies the axiom of existence). Note: this theorem does not require a disjointness condition on 𝑦, 𝑧, although both axioms should be stated with all variables disjoint. This proof only uses an instance of the axiom of separation with a bounded formula, so is valid in a constructive setting (see the CZF section in the "Intuitionistic Logic Explorer" iset.mm). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥))    ⇒   ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
Theorem	bj-rep 37433*	Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5206 (in the form of axrep6 5215). (Contributed by BJ, 14-Mar-2026.) The proof proves the statement without the DV condition on 𝑥, 𝜑, but the DV condition is added to this statement to show that this weaker version is sufficient. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
Theorem	bj-axseprep 37434*	Axiom of separation (universal closure of ax-sep 5225) from a weak form of the axiom of replacement requiring that the functional relation in it be a (total) function and the weak emptyset axiom (existence of an empty set provided existence of a set), as written in the theorem's hypotheses. This result shows that the weak emptyset axiom is not only the result of a cheap way to avoid an axiom redundancy (in this case, the existence axiom extru 1982) by adding it as an antecedent, but also permits to prove nontrivial results that hold in nonnecessarily nonempty universes. This proof is by cases so is not intuitionistic. The statement does not require a nonempty universe; most of the proof does not either, and the parts that do (e.g., near sb8ef 2363 and sbequ12r 2264 and eueq2 3658) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1934. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)    &   ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))    &   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))    ⇒   ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
Theorem	bj-axreprepsep 37435*	Strong axiom of replacement (universal closure of ax-rep 5206) from the axioms of separation and replacement as written in the theorem's hypotheses. The statement does not require a nonempty universe; most of the proof does not either, except for the use of 19.8a 2193, which could be removed by reworking the proof, since it is applied in a subexpression bound by the variable it introduces. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1934. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))    &   ⊢ ∀𝑠(∀𝑦 ∈ 𝑠 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))    ⇒   ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
21.19.5.20  Evaluation at a class This section treats the existing predicate Slot (df-slot 17150) as "evaluation at a class" and for the moment does not introduce new syntax for it.
Theorem	bj-evaleq 37436	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17151 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 37437	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 37438	The evaluation at a class is a function on the universal class. (General form of slotfn 17152). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalf 37439	The evaluation at a class is a function from the universal class into the universal class. (Contributed by BJ, 17-Mar-2026.)
⊢ Slot 𝐴:V⟶V
Theorem	bj-evalval 37440	Value of the evaluation at a class. Closed form of strfvnd 17153 and strfvn 17154. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))
Theorem	bj-evalid 37441	The evaluation at a set of the identity function is that set. General form of ndxarg 17164. 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 37442	Proof of ndxarg 17164 from bj-evalid 37441. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	bj-evalidval 37443	Closed general form of strndxid 17166. Both sides are equal to (𝐹‘𝐴) by bj-evalid 37441 and bj-evalval 37440 respectively, but bj-evalidval 37443 adds something to bj-evalid 37441 and bj-evalval 37440 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹))
21.19.5.21  Elementwise operations
Syntax	celwise 37444	Syntax for elementwise operations.
class elwise
Definition	df-elwise 37445*	Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11066), 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 ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))
21.19.5.22  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 17546), topologies (df-top 22884), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34300), 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 37446	An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17390. (Contributed by BJ, 27-Apr-2021.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	bj-restsn 37447	An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 37450 and bj-restsnid 37452. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)})
Theorem	bj-restsnss 37448	Special case of bj-restsn 37447. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴})
Theorem	bj-restsnss2 37449	Special case of bj-restsn 37447. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌})
Theorem	bj-restsn0 37450	An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 37447 and bj-restsnss2 37449. TODO: this is restsn 23160. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	bj-restsn10 37451	Special case of bj-restsn 37447, bj-restsnss 37448, and bj-rest10 37453. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅})
Theorem	bj-restsnid 37452	The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 37447 and bj-restsnss 37448. (Contributed by BJ, 27-Apr-2021.)
⊢ ({𝐴} ↾t 𝐴) = {𝐴}
Theorem	bj-rest10 37453	An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23159 and could replace it. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅}))
Theorem	bj-rest10b 37454	Alternate version of bj-rest10 37453. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅})
Theorem	bj-restn0 37455	An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅))
Theorem	bj-restn0b 37456	Alternate version of bj-restn0 37455. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅)
Theorem	bj-restpw 37457	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 23168 (which uses distop 22985 and restopn2 23167). (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴))
Theorem	bj-rest0 37458	An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴)))
Theorem	bj-restb 37459	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 37460	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 37461	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 37462	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 23152 and restuni2 23157. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴))
Theorem	bj-restuni2 37463	The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 23152 and restuni2 23157. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴)
Theorem	bj-restreg 37464	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 𝐴))
21.19.5.23  Moore collections (complements)
Theorem	bj-raldifsn 37465*	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 37466*	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 37467*	A Moore collection is a set. Therefore, the class Moore of all Moore sets defined in df-bj-moore 37469 is actually the class of all Moore collections. This is also illustrated by the lack of sethood condition in bj-ismoore 37470. 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 7713). 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 5396), 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 37476. (Contributed by BJ, 8-Dec-2021.)
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V)
Syntax	cmoore 37468	Syntax for the class of Moore collections.
class Moore
Definition	df-bj-moore 37469*	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 37467, and as illustrated by the lack of sethood condition in bj-ismoore 37470. This is to df-mre 17546 (defining Moore) what df-top 22884 (defining Top) is to df-topon 22901 (defining TopOn). For the sake of consistency, the function defined at df-mre 17546 should be denoted by "MooreOn". Note: df-mre 17546 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 37466. 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 37467). 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 17546 and df-topon 22901) or the class of all families of that kind, independent of a base set (like df-bj-moore 37469 or df-top 22884). 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 37470*	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 37467 for the RHS). (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
Theorem	bj-ismoored0 37471	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴)
Theorem	bj-ismoored 37472	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴)
Theorem	bj-ismoored2 37473	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴)
Theorem	bj-ismooredr 37474*	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 37475*	Sufficient condition to be a Moore collection (variant of bj-ismooredr 37474 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 37476	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 37477	The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ ¬ ∅ ∈ Moore
Theorem	bj-snmoore 37478	A singleton is a Moore collection. See bj-snmooreb 37479 for a biconditional version. (Contributed by BJ, 10-Apr-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
Theorem	bj-snmooreb 37479	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 37480	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 37478). 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)
21.19.5.24  Maps-to notation for functions with three arguments
Theorem	bj-0nelmpt 37481	The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.)
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	bj-mptval 37482	Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌)))
Theorem	bj-dfmpoa 37483*	An equivalent definition of df-mpo 7368. (Contributed by BJ, 30-Dec-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)}
Theorem	bj-mpomptALT 37484*	Alternate proof of mpompt 7477. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Syntax	cmpt3 37485	Syntax for maps-to notation for functions with three arguments.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
Definition	df-bj-mpt3 37486*	Define maps-to notation for functions with three arguments. See df-mpt 5161 and df-mpo 7368 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37483. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
21.19.5.25  Currying Currying and uncurrying. See also df-cur 8214 and df-unc 8215. Contrary to these, the definitions in this section are parameterized.
Syntax	csethom 37487	Syntax for the set of set morphisms.
class Set⟶
Definition	df-bj-sethom 37488*	Define the set of functions (morphisms of sets) between two sets. Same as df-map 8772 with arguments swapped. TODO: prove the same staple lemmas as for ↑m. Remark: one may define Set⟶ = (𝑥 ∈ dom Struct , 𝑦 ∈ dom Struct ↦ {𝑓 ∣ 𝑓:(Base‘𝑥)⟶(Base‘𝑦)}) so that for morphisms between other structures, one could write ... = {𝑓 ∈ (𝑥 Set⟶ 𝑦) ∣ ...}. (Contributed by BJ, 11-Apr-2020.)
⊢ Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦})
Syntax	ctophom 37489	Syntax for the set of topological morphisms.
class Top⟶
Definition	df-bj-tophom 37490*	Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 23217 (which is in terms of topologies instead of topological spaces). (Contributed by BJ, 10-Feb-2022.)
⊢ Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})
Syntax	cmgmhom 37491	Syntax for the set of magma morphisms.
class Mgm⟶
Definition	df-bj-mgmhom 37492*	Define the set of magma morphisms between two magmas. If domain and codomain are semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. (Contributed by BJ, 10-Feb-2022.)
⊢ Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
Syntax	ctopmgmhom 37493	Syntax for the set of topological magma morphisms.
class TopMgm⟶
Definition	df-bj-topmgmhom 37494*	Define the set of topological magma morphisms (continuous magma morphisms) between two topological magmas. If domain and codomain are topological semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. This definition is currently stated with topological monoid domain and codomain, since topological magmas are currently not defined in set.mm. (Contributed by BJ, 10-Feb-2022.)
⊢ TopMgm⟶ = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦)))
Syntax	ccur- 37495	Syntax for the parameterized currying function.
class curry_
Definition	df-bj-cur 37496*	Define currying. See also df-cur 8214. (Contributed by BJ, 11-Apr-2020.)
⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
Syntax	cunc- 37497	Notation for the parameterized uncurrying function.
class uncurry_
Definition	df-bj-unc 37498*	Define uncurrying. See also df-unc 8215. (Contributed by BJ, 11-Apr-2020.)
⊢ uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))))
21.19.5.26  Setting components of extensible structures Groundwork for changing the definition, syntax and token for component-setting in extensible structures. See https://github.com/metamath/set.mm/issues/2401
Syntax	cstrset 37499	Syntax for component-setting in extensible structures.
class [𝐵 / 𝐴]struct𝑆
Definition	df-strset 37500	Component-setting in extensible structures. Define the extensible structure [𝐵 / 𝐴]struct𝑆, which is like the extensible structure 𝑆 except that the value 𝐵 has been put in the slot 𝐴 (replacing the current value if there was already one). In such expressions, 𝐴 is generally substituted for slot mnemonics like Base or +g or dist. The V in this definition was chosen to be closer to df-sets 17132, but since extensible structures are functions on ℕ, it will be more natural to replace it with ℕ when df-strset 37500 becomes the main definition. (Contributed by BJ, 13-Feb-2022.)
⊢ [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})