P. 378 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-bj-bun 37701*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 37702	Existence of binary unions of sets, proved from ax-bj-bun 37701. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 37703	Existence of unordered pairs formed on sets, proved from ax-bj-sn 37697 and ax-bj-bun 37701. Contrary to bj-prex 37704, this proof is intuitionistically valid and does not require ax-nul 5268. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 37704	Existence of unordered pairs proved from ax-bj-sn 37697 and ax-bj-bun 37701. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 37705*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37706). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37706*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37707	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 37708	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 37709	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 37710	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 37711	Alternate proof of eleq2w2 2758 and special instance of eleq2 2851. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-clel3gALT 37712*	Alternate proof of clel3g 3619. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 37713	Alternate proof of pw0 4777. The proofs have a similar structure: pw0 4777 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37713 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4777 and biconditional for bj-pw0ALT 37713) to translate the property ss0b 4357 into the wanted result. To translate a biconditional into a class equality, pw0 4777 uses abbii 2829 (which yields an equality of class abstractions), while bj-pw0ALT 37713 uses eqriv 2759 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2829, through its closed form abbi 2827, is proved from eqrdv 2760, which is the deduction form of eqriv 2759. In the other direction, velpw 4566 and velsn 4604 are proved from the definitions of powerclass and singleton using elabg 3634, which is a version of abbii 2829 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝒫 ∅ = {∅}
Theorem	bj-sselpwuni 37714	Quantitative version of ssexg 5289: 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 37715	Quantitative version of uniexr 7760: 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 37716	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 4564 and elpw2g 5303 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 37717*	This theorem bj-velpwALT 37717 and the next theorem bj-elpwgALT 37718 are alternate proofs of velpw 4566 and elpwg 4564 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3523 instead of proving first the general case using elab2g 3638 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2212. In other cases, that order is better (e.g., vsnex 5405 proved before snexg 5410). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 37718	Alternate proof of elpwg 4564. See comment for bj-velpwALT 37717. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 37719	Justification theorem for dfv2 3457 if it were the definition. See also vjust 3455. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 37720*	Two formulations of the axiom of the empty set ax-nul 5268. Proposal: place it right before ax-nul 5268. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 37721*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37722. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 37722*	Alternate proof of bj-nuliota 37721. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6516). 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 37723	Alternate proof of vtoclgf 3533. Proof from vtoclgft 3519. (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 37724	Join of elsng 4602 and elsn2g 4629. (Contributed by BJ, 18-Nov-2023.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-elsnb 37725	Biconditional version of elsng 4602. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-pwcfsdom 37726	Remove hypothesis from pwcfsdom 10574. Illustration of how to remove a "proof-facilitating hypothesis". Shortens theorems using pwcfsdom 10574. (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 37727	Remove hypothesis from grur1 10811. 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 37728*	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 5256. 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 5263. Relabel ("sepbi"?).
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-dfid2ALT 37729	Alternate version of dfid2 5557. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5555 instead to make the semantics of the construction df-opab 5173 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
Theorem	bj-0nelopab 37730	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 5810 (this is a very limited reordering).
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	bj-brrelex12ALT 37731	Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5712. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-epelg 37732	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5563 and closed form of epeli 5562. (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 5716 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	bj-epelb 37733	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 5717 available. Check if it is shorter to prove bj-epelg 37732 first or bj-epelb 37733 first. (Contributed by BJ, 14-Jul-2023.)
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
Theorem	bj-nsnid 37734	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 4682): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.)
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴)
Theorem	bj-rdg0gALT 37735	Alternate proof of rdg0g 8412. More direct since it bypasses tz7.44-1 8391 and rdg0 8406 (and vtoclg 3521, vtoclga 3540). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	bj-vn0ALT 37736	Alternate proof of vn0 4297 which does not use eqabbw 2835 (and is shorter than vn0 4297 when eqabbw 2835 is inlined). (Contributed by BJ, 12-Jul-2026.) Using the same dummy variable for 𝑦 and 𝑧 slightly reduces the proof size. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ V ≠ ∅
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 5256) and the version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function, bj-rep 37738. These axioms often appear (as specific instances) in the hypotheses of the theorems in this section.
Theorem	bj-axnul 37737*	Over the base theory ax-1 6-- ax-5 1939, 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 2734 is posited) provided existence of a set (the True truth constant existentially quantified over a fresh variable, extru 2004). This is the conclusion of bj-axnul 37737. 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 5256, 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 37737. In particular, the axiom of existence extru 2004 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 37738*	Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5237 (in the form of axrep6 5246). (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 37739*	Axiom of separation (universal closure of ax-sep 5256) 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 2004) 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 2386 and sbequ12r 2287 and eueq2 3672) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1956. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)    &   ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))    &   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))    ⇒   ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
Theorem	bj-axreprepsep 37740*	Strong axiom of replacement (universal closure of ax-rep 5237) 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 2216, 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 1956. (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 17248) as "evaluation at a class" and for the moment does not introduce new syntax for it.
Theorem	bj-evaleq 37741	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17249 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 37742	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 37743	The evaluation at a class is a function on the universal class. (General form of slotfn 17250). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalf 37744	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 37745	Value of the evaluation at a class. Closed form of strfvnd 17251 and strfvn 17252. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))
Theorem	bj-evalid 37746	The evaluation at a set of the identity function is that set. General form of ndxarg 17262. 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 37747	Proof of ndxarg 17262 from bj-evalid 37746. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	bj-evalidval 37748	Closed general form of strndxid 17264. Both sides are equal to (𝐹‘𝐴) by bj-evalid 37746 and bj-evalval 37745 respectively, but bj-evalidval 37748 adds something to bj-evalid 37746 and bj-evalval 37745 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹))
21.19.5.21  Elementwise operations
Syntax	celwise 37749	Syntax for elementwise operations.
class elwise
Definition	df-elwise 37750*	Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11136), 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 17644), topologies (df-top 23062), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34508), 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 37751	An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17488. (Contributed by BJ, 27-Apr-2021.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	bj-restsn 37752	An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 37755 and bj-restsnid 37757. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)})
Theorem	bj-restsnss 37753	Special case of bj-restsn 37752. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴})
Theorem	bj-restsnss2 37754	Special case of bj-restsn 37752. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌})
Theorem	bj-restsn0 37755	An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 37752 and bj-restsnss2 37754. TODO: this is restsn 23338. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	bj-restsn10 37756	Special case of bj-restsn 37752, bj-restsnss 37753, and bj-rest10 37758. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅})
Theorem	bj-restsnid 37757	The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 37752 and bj-restsnss 37753. (Contributed by BJ, 27-Apr-2021.)
⊢ ({𝐴} ↾t 𝐴) = {𝐴}
Theorem	bj-rest10 37758	An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23337 and could replace it. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅}))
Theorem	bj-rest10b 37759	Alternate version of bj-rest10 37758. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅})
Theorem	bj-restn0 37760	An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅))
Theorem	bj-restn0b 37761	Alternate version of bj-restn0 37760. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅)
Theorem	bj-restpw 37762	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 23346 (which uses distop 23163 and restopn2 23345). (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴))
Theorem	bj-rest0 37763	An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴)))
Theorem	bj-restb 37764	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 37765	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 37766	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 37767	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 23330 and restuni2 23335. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴))
Theorem	bj-restuni2 37768	The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 23330 and restuni2 23335. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴)
Theorem	bj-restreg 37769	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 37770*	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 37771*	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 37772*	A Moore collection is a set. Therefore, the class Moore of all Moore sets defined in df-bj-moore 37774 is actually the class of all Moore collections. This is also illustrated by the lack of sethood condition in bj-ismoore 37775. 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 7760). 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 5430), 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 37781. (Contributed by BJ, 8-Dec-2021.)
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V)
Syntax	cmoore 37773	Syntax for the class of Moore collections.
class Moore
Definition	df-bj-moore 37774*	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 37772, and as illustrated by the lack of sethood condition in bj-ismoore 37775. This is to df-mre 17644 (defining Moore) what df-top 23062 (defining Top) is to df-topon 23079 (defining TopOn). For the sake of consistency, the function defined at df-mre 17644 should be denoted by "MooreOn". Note: df-mre 17644 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 37771. 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 37772). 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 17644 and df-topon 23079) or the class of all families of that kind, independent of a base set (like df-bj-moore 37774 or df-top 23062). 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 37775*	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 37772 for the RHS). (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
Theorem	bj-ismoored0 37776	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴)
Theorem	bj-ismoored 37777	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴)
Theorem	bj-ismoored2 37778	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴)
Theorem	bj-ismooredr 37779*	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 37780*	Sufficient condition to be a Moore collection (variant of bj-ismooredr 37779 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 37781	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 37782	The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ ¬ ∅ ∈ Moore
Theorem	bj-snmoore 37783	A singleton is a Moore collection. See bj-snmooreb 37784 for a biconditional version. (Contributed by BJ, 10-Apr-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
Theorem	bj-snmooreb 37784	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 37785	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 37783). 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 37786	The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.)
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	bj-mptval 37787	Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌)))
Theorem	bj-dfmpoa 37788*	An equivalent definition of df-mpo 7417. (Contributed by BJ, 30-Dec-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)}
Theorem	bj-mpomptALT 37789*	Alternate proof of mpompt 7526. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Syntax	cmpt3 37790	Syntax for maps-to notation for functions with three arguments.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
Definition	df-bj-mpt3 37791*	Define maps-to notation for functions with three arguments. See df-mpt 5192 and df-mpo 7417 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37788. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
21.19.5.25  Currying Currying and uncurrying. See also df-cur 8261 and df-unc 8262. Contrary to these, the definitions in this section are parameterized.
Syntax	csethom 37792	Syntax for the set of set morphisms.
class Set⟶
Definition	df-bj-sethom 37793*	Define the set of functions (morphisms of sets) between two sets. Same as df-map 8824 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 37794	Syntax for the set of topological morphisms.
class Top⟶
Definition	df-bj-tophom 37795*	Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 23395 (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 37796	Syntax for the set of magma morphisms.
class Mgm⟶
Definition	df-bj-mgmhom 37797*	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 37798	Syntax for the set of topological magma morphisms.
class TopMgm⟶
Definition	df-bj-topmgmhom 37799*	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- 37800	Syntax for the parameterized currying function.
class curry_