P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-disj2r 37001	Relative version of ssdifin0 4439, allowing a biconditional, and of disj2 4411. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4439 nor disj2 4411. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 37002	Contraposition law for relative subclasses. Relative and generalized version of ssconb 4095, which it can shorten, as well as conss2 44416. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4095 nor conss2 44416. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
21.19.5.17  Axioms for finite unions In this section, we introduce the axiom of singleton ax-bj-sn 37006 and the axiom of binary union ax-bj-bun 37010. Both axioms are implied by the standard axioms of unordered pair ax-pr 5374 and of union ax-un 7675 (see snex 5378 and unex 7684). Conversely, the axiom of unordered pair ax-pr 5374 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37012 and bj-prex 37013. The axioms of union ax-un 7675 and of powerset ax-pow 5307 are independent of these axioms: consider respectively the class of pseudo-hereditarily sets of cardinality less than a given singular strong limit cardinal, see Greg Oman, On the axiom of union, Arch. Math. Logic (2010) 49:283--289 (that model does have finite unions), and the class of well-founded hereditarily countable sets (or hereditarily less than a given uncountable regular cardinal). See also https://mathoverflow.net/questions/81815 5307 and https://mathoverflow.net/questions/48365 5307. A proof by finite induction shows that the existence of finite unions is equivalent to the existence of binary unions and of nullary unions (the latter being the axiom of the empty set ax-nul 5248). The axiom of binary union is useful in theories without the axioms of union ax-un 7675 and of powerset ax-pow 5307. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2701, ax-rep 5221, ax-sep 5238, ax-nul 5248, ax-reg 9503 } and the axioms of existence of unordered 𝑚-tuples for all 𝑚 ≤ 𝑛, and in most cases one would like to rule out such models, hence the need for extra axioms, typically variants of powersets or unions. The axiom of adjunction ax-bj-adj 37015 is more widely used, and is an axiom of General Set Theory. We prove how to retrieve it from binary union and singleton in bj-adjfrombun 37019 and conversely how to prove from adjunction singleton (bj-snfromadj 37017) and unordered pair (bj-prfromadj 37018).
Theorem	bj-abex 37003*	Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-clex 37004*	Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-axsn 37005*	Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37006). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥))
Axiom	ax-bj-sn 37006*	Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
Theorem	bj-snexg 37007	A singleton built on a set is a set. Contrary to bj-snex 37008, this proof is intuitionistically valid and does not require ax-nul 5248. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5378 and prove it from ax-bj-sn 37006. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 37008	A singleton is a set. See also snex 5378, snexALT 5325. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37006. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴} ∈ V
Theorem	bj-axbun 37009*	Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37010). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)))
Axiom	ax-bj-bun 37010*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 37011	Existence of binary unions of sets, proved from ax-bj-bun 37010. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 37012	Existence of unordered pairs formed on sets, proved from ax-bj-sn 37006 and ax-bj-bun 37010. Contrary to bj-prex 37013, this proof is intuitionistically valid and does not require ax-nul 5248. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 37013	Existence of unordered pairs proved from ax-bj-sn 37006 and ax-bj-bun 37010. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 37014*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37015). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37015*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37016	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 37017	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 37018	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 37019	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 37020	Alternate proof of eleq2w2 2725 and special instance of eleq2 2817. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-clel3gALT 37021*	Alternate proof of clel3g 3618. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 37022	Alternate proof of pw0 4766. The proofs have a similar structure: pw0 4766 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37022 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4766 and biconditional for bj-pw0ALT 37022) to translate the property ss0b 4354 into the wanted result. To translate a biconditional into a class equality, pw0 4766 uses abbii 2796 (which yields an equality of class abstractions), while bj-pw0ALT 37022 uses eqriv 2726 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2796, through its closed form abbi 2794, is proved from eqrdv 2727, which is the deduction form of eqriv 2726. In the other direction, velpw 4558 and velsn 4595 are proved from the definitions of powerclass and singleton using elabg 3634, which is a version of abbii 2796 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝒫 ∅ = {∅}
Theorem	bj-sselpwuni 37023	Quantitative version of ssexg 5265: 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 37024	Quantitative version of uniexr 7703: 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 37025	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 4556 and elpw2g 5275 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 37026*	This theorem bj-velpwALT 37026 and the next theorem bj-elpwgALT 37027 are alternate proofs of velpw 4558 and elpwg 4556 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3514 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 2178. In other cases, that order is better (e.g., vsnex 5376 proved before snexg 5377). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 37027	Alternate proof of elpwg 4556. See comment for bj-velpwALT 37026. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 37028	Justification theorem for dfv2 3441 if it were the definition. See also vjust 3439. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 37029*	Two formulations of the axiom of the empty set ax-nul 5248. Proposal: place it right before ax-nul 5248. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 37030*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37031. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 37031*	Alternate proof of bj-nuliota 37030. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6466). 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 37032	Alternate proof of vtoclgf 3526. Proof from vtoclgft 3509. (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 37033	Join of elsng 4593 and elsn2g 4618. (Contributed by BJ, 18-Nov-2023.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-elsnb 37034	Biconditional version of elsng 4593. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-pwcfsdom 37035	Remove hypothesis from pwcfsdom 10496. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 10496.) (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 37036	Remove hypothesis from grur1 10733. 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 37037*	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 5238. 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 5243. Relabel ("sepbi"?).
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-dfid2ALT 37038	Alternate version of dfid2 5520. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5518 instead to make the semantics of the construction df-opab 5158 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
Theorem	bj-0nelopab 37039	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 5771 (this is a very limited reordering).
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	bj-brrelex12ALT 37040	Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5675. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-epelg 37041	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5526 and closed form of epeli 5525. (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 5679 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	bj-epelb 37042	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 5680 available. Check if it is shorter to prove bj-epelg 37041 first or bj-epelb 37042 first. (Contributed by BJ, 14-Jul-2023.)
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
Theorem	bj-nsnid 37043	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 4671): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.)
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴)
Theorem	bj-rdg0gALT 37044	Alternate proof of rdg0g 8356. More direct since it bypasses tz7.44-1 8335 and rdg0 8350 (and vtoclg 3511, vtoclga 3534). (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  Evaluation at a class This section treats the existing predicate Slot (df-slot 17111) as "evaluation at a class" and for the moment does not introduce new syntax for it.
Theorem	bj-evaleq 37045	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17112 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 37046	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 37047	The evaluation at a class is a function on the universal class. (General form of slotfn 17113). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalval 37048	Value of the evaluation at a class. (Closed form of strfvnd 17114 and strfvn 17115). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))
Theorem	bj-evalid 37049	The evaluation at a set of the identity function is that set. (General form of ndxarg 17125.) 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 37050	Proof of ndxarg 17125 from bj-evalid 37049. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	bj-evalidval 37051	Closed general form of strndxid 17127. Both sides are equal to (𝐹‘𝐴) by bj-evalid 37049 and bj-evalval 37048 respectively, but bj-evalidval 37051 adds something to bj-evalid 37049 and bj-evalval 37048 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹))
21.19.5.20  Elementwise operations
Syntax	celwise 37052	Syntax for elementwise operations.
class elwise
Definition	df-elwise 37053*	Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11058), 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.21  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 17506), topologies (df-top 22797), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34075), 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 37054	An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17351. (Contributed by BJ, 27-Apr-2021.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	bj-restsn 37055	An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 37058 and bj-restsnid 37060. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)})
Theorem	bj-restsnss 37056	Special case of bj-restsn 37055. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴})
Theorem	bj-restsnss2 37057	Special case of bj-restsn 37055. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌})
Theorem	bj-restsn0 37058	An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 37055 and bj-restsnss2 37057. TODO: this is restsn 23073. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	bj-restsn10 37059	Special case of bj-restsn 37055, bj-restsnss 37056, and bj-rest10 37061. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅})
Theorem	bj-restsnid 37060	The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 37055 and bj-restsnss 37056. (Contributed by BJ, 27-Apr-2021.)
⊢ ({𝐴} ↾t 𝐴) = {𝐴}
Theorem	bj-rest10 37061	An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23072 and could replace it. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅}))
Theorem	bj-rest10b 37062	Alternate version of bj-rest10 37061. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅})
Theorem	bj-restn0 37063	An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅))
Theorem	bj-restn0b 37064	Alternate version of bj-restn0 37063. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅)
Theorem	bj-restpw 37065	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 23081 (which uses distop 22898 and restopn2 23080). (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴))
Theorem	bj-rest0 37066	An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴)))
Theorem	bj-restb 37067	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 37068	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 37069	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 37070	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 23065 and restuni2 23070. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴))
Theorem	bj-restuni2 37071	The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 23065 and restuni2 23070. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴)
Theorem	bj-restreg 37072	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.22  Moore collections (complements)
Theorem	bj-raldifsn 37073*	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 37074*	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 37075*	A Moore collection is a set. Therefore, the class Moore of all Moore sets defined in df-bj-moore 37077 is actually the class of all Moore collections. This is also illustrated by the lack of sethood condition in bj-ismoore 37078. 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 7703). 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 5397), 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 37084. (Contributed by BJ, 8-Dec-2021.)
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V)
Syntax	cmoore 37076	Syntax for the class of Moore collections.
class Moore
Definition	df-bj-moore 37077*	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 37075, and as illustrated by the lack of sethood condition in bj-ismoore 37078. This is to df-mre 17506 (defining Moore) what df-top 22797 (defining Top) is to df-topon 22814 (defining TopOn). For the sake of consistency, the function defined at df-mre 17506 should be denoted by "MooreOn". Note: df-mre 17506 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 37074. 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 37075). 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 17506 and df-topon 22814) or the class of all families of that kind, independent of a base set (like df-bj-moore 37077 or df-top 22797). 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 37078*	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 37075 for the RHS). (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
Theorem	bj-ismoored0 37079	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴)
Theorem	bj-ismoored 37080	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴)
Theorem	bj-ismoored2 37081	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴)
Theorem	bj-ismooredr 37082*	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 37083*	Sufficient condition to be a Moore collection (variant of bj-ismooredr 37082 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 37084	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 37085	The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ ¬ ∅ ∈ Moore
Theorem	bj-snmoore 37086	A singleton is a Moore collection. See bj-snmooreb 37087 for a biconditional version. (Contributed by BJ, 10-Apr-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
Theorem	bj-snmooreb 37087	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 37088	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 37086). 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.23  Maps-to notation for functions with three arguments
Theorem	bj-0nelmpt 37089	The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.)
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	bj-mptval 37090	Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌)))
Theorem	bj-dfmpoa 37091*	An equivalent definition of df-mpo 7358. (Contributed by BJ, 30-Dec-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)}
Theorem	bj-mpomptALT 37092*	Alternate proof of mpompt 7467. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Syntax	cmpt3 37093	Syntax for maps-to notation for functions with three arguments.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
Definition	df-bj-mpt3 37094*	Define maps-to notation for functions with three arguments. See df-mpt 5177 and df-mpo 7358 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37091. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
21.19.5.24  Currying Currying and uncurrying. See also df-cur 8207 and df-unc 8208. Contrary to these, the definitions in this section are parameterized.
Syntax	csethom 37095	Syntax for the set of set morphisms.
class Set⟶
Definition	df-bj-sethom 37096*	Define the set of functions (morphisms of sets) between two sets. Same as df-map 8762 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 37097	Syntax for the set of topological morphisms.
class Top⟶
Definition	df-bj-tophom 37098*	Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 23130 (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 37099	Syntax for the set of magma morphisms.
class Mgm⟶
Definition	df-bj-mgmhom 37100*	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‘𝑦)(𝑓‘𝑣))})