P. 501 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50001-50100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mofeu 50001*	The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐺 = (𝐴 × 𝐵)    &   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))    &   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹 = 𝐺))
Theorem	elfvne0 50002	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 50003	A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ≠ ∅) → (𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅))
Theorem	f1sn2g 50004	A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:{𝐴}⟶𝐵) → 𝐹:{𝐴}–1-1→𝐵)
Theorem	f102g 50005	A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 = ∅ ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f1mo 50006*	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 50007	A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))
Theorem	map0cor 50008*	A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐵 = ∅ → 𝐴 = ∅) ↔ ∃𝑓 𝑓:𝐴⟶𝐵))
Theorem	ffvbr 50009	Relation with function value. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋𝐹(𝐹‘𝑋))
Theorem	xpco2 50010	Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 × 𝐶) ∘ 𝐹) = (𝐴 × 𝐶))
21.53.5.5  Operations
Theorem	ovsng 50011	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsng2 50012	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsn 50013	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 50014	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶
Theorem	ovconstbrd 50015	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌))
Theorem	ovconstbrn0d 50016	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅))
Theorem	elovconstbrd 50017	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐵)
Theorem	ovmpt4d 50018*	Deduction version of ovmpt4g 7567. (This is the operation analogue of fvmpt2d 7007.) (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = 𝐶)
Theorem	eqfnovd 50019*	Deduction for equality of operations. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝐺 Fn (𝐴 × 𝐵))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.53.6  ZF Set Theory - add the Axiom of Union
21.53.6.1  Relations and functions (cont.)
Theorem	fonex 50020	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.53.6.2  First and second members of an ordered pair
Theorem	eloprab1st2nd 50021*	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.53.6.3  Function transposition
Theorem	resinsnlem 50022	Lemma for resinsnALT 50024. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ 𝜒)
Theorem	resinsn 50023	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	resinsnALT 50024	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 50025*	Alternate definition of tpos. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = (𝐹 ∘ ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) ∪ {⟨∅, ∅⟩}))
Theorem	dftpos6 50026*	Alternate definition of tpos. The second half of the right hand side could apply ressn 6288 and become (𝐹 ↾ {∅}). (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = ((𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})) ∪ ({∅} × (𝐹 “ {∅})))
Theorem	dmtposss 50027	The domain of tpos 𝐹 is a subset. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ dom tpos 𝐹 ⊆ ((V × V) ∪ {∅})
Theorem	tposres0 50028	The transposition of a set restricted to the empty set is the set restricted to the empty set. See also ressn 6288 and dftpos6 50026 for an alternate proof. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ {∅}) = (𝐹 ↾ {∅})
Theorem	tposresg 50029	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ 𝑅) = ((tpos 𝐹 ↾ ◡◡𝑅) ∪ (𝐹 ↾ (𝑅 ∩ {∅})))
Theorem	tposrescnv 50030*	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 8243. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ ◡𝑅) = (𝐹 ∘ (𝑥 ∈ ◡dom (𝐹 ↾ 𝑅) ↦ ∪ ◡{𝑥}))
Theorem	tposres2 50031	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = (tpos 𝐹 ↾ ◡◡𝑅))
Theorem	tposres3 50032	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposres 50033	The transposition restricted to a relation. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposresxp 50034	The transposition restricted to a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ (𝐴 × 𝐵)) = tpos (𝐹 ↾ (𝐵 × 𝐴))
Theorem	tposf1o 50035	Condition of a bijective transposition. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–1-1-onto→𝐶)
Theorem	tposid 50036	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝑋tpos I 𝑌) = ⟨𝑌, 𝑋⟩
Theorem	tposidres 50037	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑌tpos ( I ↾ (𝐴 × 𝐵))𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	tposidf1o 50038	The swap function, or the twisting map, is bijective. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ tpos ( I ↾ (𝐴 × 𝐵)):(𝐵 × 𝐴)–1-1-onto→(𝐴 × 𝐵)
Theorem	tposideq 50039*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥}))
Theorem	tposideq2 50040*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ 𝑅 = (𝐴 × 𝐵)    ⇒   ⊢ (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥})
21.53.6.4  Infinite Cartesian products
Theorem	ixpv 50041*	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.53.6.5  Equinumerosity
Theorem	fvconst0ci 50042	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 50043	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 50044*	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 50043 assuming ax-un 7751 (see f1omoALT 50046). (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoOLD 50045*	Obsolete version of f1omo 50044 as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoALT 50046*	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 50044 without assuming ax-un 7751. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
21.53.7  Order sets
21.53.7.1  Real number intervals
Theorem	iccin 50047	Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷)))
Theorem	iccdisj2 50048	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 50049	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.53.8  Extensible structures
21.53.8.1  Basic definitions
Theorem	slotresfo 50050*	The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex 50020 can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐸 Fn V    &   ⊢ (𝑘 ∈ 𝐴 → (𝐸‘𝑘) ∈ 𝑉)    &   ⊢ (𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴)    &   ⊢ (𝑏 ∈ 𝑉 → 𝑏 = (𝐸‘𝐾))    ⇒   ⊢ (𝐸 ↾ 𝐴):𝐴–onto→𝑉
21.53.9  Moore spaces
Theorem	mreuniss 50051	The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → ∪ 𝑆 ⊆ 𝑋)
21.53.10  Topology Additional contents for topology.
21.53.10.1  Closure and interior
Theorem	clduni 50052	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	opncldbid 50053*	Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = (∪ 𝐽 ∖ 𝑦)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐽 𝜓 ↔ ∀𝑦 ∈ (Clsd‘𝐽)𝜒))
Theorem	opndisj 50054	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 50055	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 50054 with elssuni 4898 replaced by the combination of cldss 23347 and eqid 2760. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑍) ↔ (𝑌 ∈ (Clsd‘𝐽) ∧ (𝑋 ∩ 𝑌) = ∅)))
21.53.10.2  Neighborhoods
Theorem	neircl 50056	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 50057*	Lemma factoring out common proof steps of opnneil 50061 and opnneirv 50059. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneir 50058*	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 50059*	A variant of opnneir 50058 with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝜒))
Theorem	opnneilv 50060*	The converse of opnneir 50058 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 50056), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneil 50061*	A variant of opnneilv 50060. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneibid 50062*	The equivalence between neighborhood and open neighborhood. See opnneibid2 50063 for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneibid2 50063*	The equivalence between neighborhood and open neighborhood. A variant of opnneibid 50062 with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
21.53.10.3  Subspace topologies
Theorem	restcls2lem 50064	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 50065	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 50066	Lemma for restclssep 50067. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)
Theorem	restclssep 50067	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.53.10.4  Limits and continuity in topological spaces
Theorem	cnneiima 50068	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.53.10.5  Topological definitions using the reals
Theorem	iooii 50069	Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴(,)𝐵) ∈ II)
Theorem	icccldii 50070	Closed intervals are closed sets of II. Note that iccss 13545, iccordt 23532, and ordtresticc 23541 are proved from ixxss12 13496, ordtcld3 23517, and ordtrest2 23522, respectively. An alternate proof uses restcldi 23491, dfii2 25203, and icccld 25085. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II))
Theorem	i0oii 50071	(0[,)𝐴) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II)
Theorem	io1ii 50072	(𝐴(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (0 ≤ 𝐴 → (𝐴(,]1) ∈ II)
21.53.10.6  Separated sets
Theorem	sepnsepolem1 50073*	Lemma for sepnsepo 50075. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒)))
Theorem	sepnsepolem2 50074*	Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 50075. Proof could be shortened by 1 step using ssdisjdr 49962. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepnsepo 50075*	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 50076	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 50077*	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 50075. The relationship between separatedness and closure is also seen in isnrm 23653, isnrm2 23676, isnrm3 23677. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 50078*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 50075 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 50056, adantr 486, and rexlimiva 3155. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 50079*	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 50080	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 50081*	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.53.10.7  Separated spaces: T0, T1, T2 (Hausdorff) ...
Theorem	isnrm4 50082*	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 50083*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23635. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 50084*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23635. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 50085*	Lemma for iscnrm3 50103. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 50086*	Lemma for iscnrm3 50103 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem4 50087	Lemma for iscnrm3lem5 50088 and iscnrm3r 50099. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 50088*	Lemma for iscnrm3l 50102. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 50089*	Lemma for iscnrm3lem7 50090. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 50090*	Lemma for iscnrm3rlem8 50098 and iscnrm3llem2 50101 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 50091	Lemma for iscnrm3rlem2 50092. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 50092	Lemma for iscnrm3rlem3 50093. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))
Theorem	iscnrm3rlem3 50093	Lemma for iscnrm3r 50099. The designed subspace is a subset of the original set; the two sets are closed sets in the subspace. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽)) → ((∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝒫 ∪ 𝐽 ∧ (((cls‘𝐽)‘𝑆) ∖ ((cls‘𝐽)‘𝑇)) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) ∧ (((cls‘𝐽)‘𝑇) ∖ ((cls‘𝐽)‘𝑆)) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))))))
Theorem	iscnrm3rlem4 50094	Lemma for iscnrm3rlem8 50098. Given two disjoint subsets 𝑆 and 𝑇 of the underlying set of a topology 𝐽, if 𝑁 is a superset of (((cls‘𝐽)‘𝑆) ∖ 𝑇), then it is a superset of 𝑆. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ⊆ 𝑁)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
Theorem	iscnrm3rlem5 50095	Lemma for iscnrm3rlem6 50096. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝐽)
Theorem	iscnrm3rlem6 50096	Lemma for iscnrm3rlem7 50097. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))    ⇒   ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽))
Theorem	iscnrm3rlem7 50097	Lemma for iscnrm3rlem8 50098. Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))))    ⇒   ⊢ (𝜑 → 𝑂 ∈ 𝐽)
Theorem	iscnrm3rlem8 50098*	Lemma for iscnrm3r 50099. Disjoint open neighborhoods in the subspace topology are disjoint open neighborhoods in the original topology given that the subspace is an open set in the original topology. Therefore, given any two sets separated in the original topology and separated by open neighborhoods in the subspace topology, they must be separated by open neighborhoods in the original topology. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)) → (∃𝑙 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))∃𝑘 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))((((cls‘𝐽)‘𝑆) ∖ ((cls‘𝐽)‘𝑇)) ⊆ 𝑙 ∧ (((cls‘𝐽)‘𝑇) ∖ ((cls‘𝐽)‘𝑆)) ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))
Theorem	iscnrm3r 50099*	Lemma for iscnrm3 50103. If all subspaces of a topology are normal, i.e., two disjoint closed sets can be separated by open neighborhoods, then in the original topology two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑧 ∈ 𝒫 ∪ 𝐽∀𝑐 ∈ (Clsd‘(𝐽 ↾t 𝑧))∀𝑑 ∈ (Clsd‘(𝐽 ↾t 𝑧))((𝑐 ∩ 𝑑) = ∅ → ∃𝑙 ∈ (𝐽 ↾t 𝑧)∃𝑘 ∈ (𝐽 ↾t 𝑧)(𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)) → ((𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽) → (((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))))
Theorem	iscnrm3llem1 50100	Lemma for iscnrm3l 50102. Closed sets in the subspace are subsets of the underlying set of the original topology. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (𝐶 ∈ 𝒫 ∪ 𝐽 ∧ 𝐷 ∈ 𝒫 ∪ 𝐽))