P. 493 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49201-49300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eufsn 49201*	There is exactly one function into a singleton, assuming ax-rep 5226. See eufsn2 49202 for different axiom requirements. If existence is not needed, use mofsn 49203 or mofsn2 49204 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	eufsn2 49202*	There is exactly one function into a singleton, assuming ax-pow 5312 and ax-un 7690. Variant of eufsn 49201. If existence is not needed, use mofsn 49203 or mofsn2 49204 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn 49203*	There is at most one function into a singleton, with fewer axioms than eufsn 49201 and eufsn2 49202. See also mofsn2 49204. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 ∈ 𝑉 → ∃*𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn2 49204*	There is at most one function into a singleton. An unconditional variant of mofsn 49203, i.e., the singleton could be empty if 𝑌 is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 = {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofsssn 49205*	There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝐵 ⊆ {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofmo 49206*	There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐵 → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofeu 49207*	The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐺 = (𝐴 × 𝐵)    &   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))    &   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹 = 𝐺))
Theorem	elfvne0 49208	If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024.)
⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐹 ≠ ∅)
Theorem	fdomne0 49209	A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ≠ ∅) → (𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅))
Theorem	f1sn2g 49210	A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:{𝐴}⟶𝐵) → 𝐹:{𝐴}–1-1→𝐵)
Theorem	f102g 49211	A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 = ∅ ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f1mo 49212*	A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f002 49213	A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))
Theorem	map0cor 49214*	A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐵 = ∅ → 𝐴 = ∅) ↔ ∃𝑓 𝑓:𝐴⟶𝐵))
Theorem	ffvbr 49215	Relation with function value. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋𝐹(𝐹‘𝑋))
Theorem	xpco2 49216	Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 × 𝐶) ∘ 𝐹) = (𝐴 × 𝐶))
21.49.5.5  Operations
Theorem	ovsng 49217	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsng2 49218	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsn 49219	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶
Theorem	ovsn2 49220	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶
Theorem	fvconstr 49221	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌))
Theorem	fvconstrn0 49222	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅))
Theorem	fvconstr2 49223	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐵)
Theorem	ovmpt4d 49224*	Deduction version of ovmpt4g 7515. (This is the operation analogue of fvmpt2d 6963.) (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = 𝐶)
Theorem	eqfnovd 49225*	Deduction for equality of operations. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝐺 Fn (𝐴 × 𝐵))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.49.6  ZF Set Theory - add the Axiom of Union
21.49.6.1  Relations and functions (cont.)
Theorem	fonex 49226	The domain of a surjection is a proper class if the range is a proper class as well. Can be used to prove that if a structure component extractor restricted to a class maps onto a proper class, then the class is a proper class as well. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐵 ∉ V    &   ⊢ 𝐹:𝐴–onto→𝐵    ⇒   ⊢ 𝐴 ∉ V
21.49.6.2  First and second members of an ordered pair
Theorem	eloprab1st2nd 49227*	Reconstruction of a nested ordered pair in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025.)
⊢ (𝐴 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → 𝐴 = ⟨⟨(1st ‘(1st ‘𝐴)), (2nd ‘(1st ‘𝐴))⟩, (2nd ‘𝐴)⟩)
21.49.6.3  Operations in maps-to notation (continued)
Theorem	fmpodg 49228*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 = (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → 𝐹:𝑅⟶𝑆)
Theorem	fmpod 49229*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)⟶𝑆)
21.49.6.4  Function transposition
Theorem	resinsnlem 49230	Lemma for resinsnALT 49232. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ 𝜒)
Theorem	resinsn 49231	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	resinsnALT 49232	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	dftpos5 49233*	Alternate definition of tpos. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = (𝐹 ∘ ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) ∪ {⟨∅, ∅⟩}))
Theorem	dftpos6 49234*	Alternate definition of tpos. The second half of the right hand side could apply ressn 6251 and become (𝐹 ↾ {∅}). (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = ((𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})) ∪ ({∅} × (𝐹 “ {∅})))
Theorem	dmtposss 49235	The domain of tpos 𝐹 is a subset. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ dom tpos 𝐹 ⊆ ((V × V) ∪ {∅})
Theorem	tposres0 49236	The transposition of a set restricted to the empty set is the set restricted to the empty set. See also ressn 6251 and dftpos6 49234 for an alternate proof. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ {∅}) = (𝐹 ↾ {∅})
Theorem	tposresg 49237	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ 𝑅) = ((tpos 𝐹 ↾ ◡◡𝑅) ∪ (𝐹 ↾ (𝑅 ∩ {∅})))
Theorem	tposrescnv 49238*	The transposition restricted to a converse is the transposition of the restricted class, with the empty set removed from the domain. Note that the right hand side is a more useful form of (tpos (𝐹 ↾ 𝑅) ↾ (V ∖ {∅})) by df-tpos 8178. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ ◡𝑅) = (𝐹 ∘ (𝑥 ∈ ◡dom (𝐹 ↾ 𝑅) ↦ ∪ ◡{𝑥}))
Theorem	tposres2 49239	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = (tpos 𝐹 ↾ ◡◡𝑅))
Theorem	tposres3 49240	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposres 49241	The transposition restricted to a relation. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposresxp 49242	The transposition restricted to a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ (𝐴 × 𝐵)) = tpos (𝐹 ↾ (𝐵 × 𝐴))
Theorem	tposf1o 49243	Condition of a bijective transposition. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–1-1-onto→𝐶)
Theorem	tposid 49244	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝑋tpos I 𝑌) = ⟨𝑌, 𝑋⟩
Theorem	tposidres 49245	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑌tpos ( I ↾ (𝐴 × 𝐵))𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	tposidf1o 49246	The swap function, or the twisting map, is bijective. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ tpos ( I ↾ (𝐴 × 𝐵)):(𝐵 × 𝐴)–1-1-onto→(𝐴 × 𝐵)
Theorem	tposideq 49247*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥}))
Theorem	tposideq2 49248*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ 𝑅 = (𝐴 × 𝐵)    ⇒   ⊢ (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥})
21.49.6.5  Infinite Cartesian products
Theorem	ixpv 49249*	Infinite Cartesian product of the universal class is the set of functions with a fixed domain. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ X𝑥 ∈ 𝐴 V = {𝑓 ∣ 𝑓 Fn 𝐴}
21.49.6.6  Equinumerosity
Theorem	fvconst0ci 49250	A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝑌 = ((𝐴 × {𝐵})‘𝑋)    ⇒   ⊢ (𝑌 = ∅ ∨ 𝑌 = 𝐵)
Theorem	fvconstdomi 49251	A constant function's value is dominated by the constant. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × {𝐵})‘𝑋) ≼ 𝐵
Theorem	f1omo 49252*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi 49251 assuming ax-un 7690 (see f1omoALT 49254). (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoOLD 49253*	Obsolete version of f1omo 49252 as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoALT 49254*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Use f1omo 49252 without assuming ax-un 7690. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
21.49.7  Order sets
21.49.7.1  Real number intervals
Theorem	iccin 49255	Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷)))
Theorem	iccdisj2 49256	If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅)
Theorem	iccdisj 49257	If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅)
21.49.8  Extensible structures
21.49.8.1  Basic definitions
Theorem	slotresfo 49258*	The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex 49226 can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐸 Fn V    &   ⊢ (𝑘 ∈ 𝐴 → (𝐸‘𝑘) ∈ 𝑉)    &   ⊢ (𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴)    &   ⊢ (𝑏 ∈ 𝑉 → 𝑏 = (𝐸‘𝐾))    ⇒   ⊢ (𝐸 ↾ 𝐴):𝐴–onto→𝑉
21.49.9  Moore spaces
Theorem	mreuniss 49259	The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → ∪ 𝑆 ⊆ 𝑋)
21.49.10  Topology Additional contents for topology.
21.49.10.1  Closure and interior
Theorem	clduni 49260	The union of closed sets is the underlying set of the topology (the union of open sets). (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝐽 ∈ Top → ∪ (Clsd‘𝐽) = ∪ 𝐽)
Theorem	opncldeqv 49261*	Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = (∪ 𝐽 ∖ 𝑦)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐽 𝜓 ↔ ∀𝑦 ∈ (Clsd‘𝐽)𝜒))
Theorem	opndisj 49262	Two ways of saying that two open sets are disjoint, if 𝐽 is a topology and 𝑋 is an open set. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ (𝐽 ∩ 𝒫 𝑍) ↔ (𝑌 ∈ 𝐽 ∧ (𝑋 ∩ 𝑌) = ∅)))
Theorem	clddisj 49263	Two ways of saying that two closed sets are disjoint, if 𝐽 is a topology and 𝑋 is a closed set. An alternative proof is similar to that of opndisj 49262 with elssuni 4896 replaced by the combination of cldss 22985 and eqid 2737. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑍) ↔ (𝑌 ∈ (Clsd‘𝐽) ∧ (𝑋 ∩ 𝑌) = ∅)))
21.49.10.2  Neighborhoods
Theorem	neircl 49264	Reverse closure of the neighborhood operation. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by Zhi Wang, 16-Sep-2024.)
⊢ (𝑁 ∈ ((nei‘𝐽)‘𝑆) → 𝐽 ∈ Top)
Theorem	opnneilem 49265*	Lemma factoring out common proof steps of opnneil 49269 and opnneirv 49267. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneir 49266*	If something is true for an open neighborhood, it must be true for a neighborhood. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓))
Theorem	opnneirv 49267*	A variant of opnneir 49266 with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝜒))
Theorem	opnneilv 49268*	The converse of opnneir 49266 with different dummy variables. Note that the second hypothesis could be generalized by adding 𝑦 ∈ 𝐽 to the antecedent. See the proof for details. Although 𝐽 ∈ Top might be redundant here (see neircl 49264), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneil 49269*	A variant of opnneilv 49268. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneieqv 49270*	The equivalence between neighborhood and open neighborhood. See opnneieqvv 49271 for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneieqvv 49271*	The equivalence between neighborhood and open neighborhood. A variant of opnneieqv 49270 with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
21.49.10.3  Subspace topologies
Theorem	restcls2lem 49272	A closed set in a subspace topology is a subset of the subspace. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑌)
Theorem	restcls2 49273	A closed set in a subspace topology is the closure in the original topology intersecting with the subspace. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → 𝑆 = (((cls‘𝐽)‘𝑆) ∩ 𝑌))
Theorem	restclsseplem 49274	Lemma for restclssep 49275. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)
Theorem	restclssep 49275	Two disjoint closed sets in a subspace topology are separated in the original topology. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅))
21.49.10.4  Limits and continuity in topological spaces
Theorem	cnneiima 49276	Given a continuous function, the preimage of a neighborhood is a neighborhood. To be precise, the preimage of a neighborhood of a subset 𝑇 of the codomain of a continuous function is a neighborhood of any subset of the preimage of 𝑇. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑁 ∈ ((nei‘𝐾)‘𝑇))    &   ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝑇))    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝑁) ∈ ((nei‘𝐽)‘𝑆))
21.49.10.5  Topological definitions using the reals
Theorem	iooii 49277	Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴(,)𝐵) ∈ II)
Theorem	icccldii 49278	Closed intervals are closed sets of II. Note that iccss 13342, iccordt 23170, and ordtresticc 23179 are proved from ixxss12 13293, ordtcld3 23155, and ordtrest2 23160, respectively. An alternate proof uses restcldi 23129, dfii2 24843, and icccld 24722. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II))
Theorem	i0oii 49279	(0[,)𝐴) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II)
Theorem	io1ii 49280	(𝐴(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (0 ≤ 𝐴 → (𝐴(,]1) ∈ II)
21.49.10.6  Separated sets
Theorem	sepnsepolem1 49281*	Lemma for sepnsepo 49283. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒)))
Theorem	sepnsepolem2 49282*	Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 49283. Proof could be shortened by 1 step using ssdisjdr 49168. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepnsepo 49283*	Open neighborhood and neighborhood is equivalent regarding disjointness for both sides. Namely, separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝐶)∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepdisj 49284	Separated sets are disjoint. Note that in general separatedness also requires 𝑇 ⊆ ∪ 𝐽 and (𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ as well but they are unnecessary here. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)    ⇒   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)
Theorem	seposep 49285*	If two sets are separated by (open) neighborhoods, then they are separated subsets of the underlying set. Note that separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. See sepnsepo 49283. The relationship between separatedness and closure is also seen in isnrm 23291, isnrm2 23314, isnrm3 23315. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 49286*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 49283 for the equivalence between separatedness by open neighborhoods and separatedness by neighborhoods. Although 𝐽 ∈ Top might be redundant here, it is listed for explicitness. 𝐽 ∈ Top can be obtained from neircl 49264, adantr 480, and rexlimiva 3131. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 49287*	If two sets are separated by a continuous function, then they are separated by closed neighborhoods. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	seppsepf 49288	If two sets are precisely separated by a continuous function, then they are separated by the continuous function. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 = (◡𝑓 “ {0}) ∧ 𝑇 = (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1})))
Theorem	seppcld 49289*	If two sets are precisely separated by a continuous function, then they are closed. An alternate proof involves II ∈ Fre. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 = (◡𝑓 “ {0}) ∧ 𝑇 = (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → (𝑆 ∈ (Clsd‘𝐽) ∧ 𝑇 ∈ (Clsd‘𝐽)))
21.49.10.7  Separated spaces: T0, T1, T2 (Hausdorff) ...
Theorem	isnrm4 49290*	A topological space is normal iff any two disjoint closed sets are separated by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑑 ∈ (Clsd‘𝐽)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝐽)‘𝑐)∃𝑦 ∈ ((nei‘𝐽)‘𝑑)(𝑥 ∩ 𝑦) = ∅)))
Theorem	dfnrm2 49291*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23273. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 49292*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23273. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 49293*	Lemma for iscnrm3 49311. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 49294*	Lemma for iscnrm3 49311 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem4 49295	Lemma for iscnrm3lem5 49296 and iscnrm3r 49307. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 49296*	Lemma for iscnrm3l 49310. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 49297*	Lemma for iscnrm3lem7 49298. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 49298*	Lemma for iscnrm3rlem8 49306 and iscnrm3llem2 49309 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 49299	Lemma for iscnrm3rlem2 49300. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 49300	Lemma for iscnrm3rlem3 49301. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))