P. 420 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41901-42000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ntrclsk3 41901*	The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
Theorem	ntrclsk13 41902*	The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
Theorem	ntrclsk4 41903*	Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)))
Theorem	ntrneibex 41904*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the base set exists. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	ntrneircomplex 41905*	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	ntrneif1o 41906*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐹:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	ntrneiiex 41907*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the interior function exists. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
Theorem	ntrneinex 41908*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the neighborhood function exists. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	ntrneicnv 41909*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then converse of 𝐹 is known. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ◡𝐹 = (𝐵𝑂𝒫 𝐵))
Theorem	ntrneifv1 41910*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the function value of 𝐹 is the neighborhood function. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (𝐹‘𝐼) = 𝑁)
Theorem	ntrneifv2 41911*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then the function value of converse of 𝐹 is the interior function. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (◡𝐹‘𝑁) = 𝐼)
Theorem	ntrneiel 41912*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋)))
Theorem	ntrneifv3 41913*	The value of the neighbors (convergents) expressed in terms of the interior (closure) function. (Contributed by RP, 26-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑠)})
Theorem	ntrneineine0lem 41914*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵𝑋 ∈ (𝐼‘𝑠) ↔ (𝑁‘𝑋) ≠ ∅))
Theorem	ntrneineine1lem 41915*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ (𝐼‘𝑠) ↔ (𝑁‘𝑋) ≠ 𝒫 𝐵))
Theorem	ntrneifv4 41916*	The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑆) = {𝑥 ∈ 𝐵 ∣ 𝑆 ∈ (𝑁‘𝑥)})
Theorem	ntrneiel2 41917*	Membership in iterated interior of a set is equivalent to there existing a particular neighborhood of that member such that points are members of that neighborhood if and only if the set is a neighborhood of each of those points. (Contributed by RP, 11-Jul-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐼‘𝑆)) ↔ ∃𝑢 ∈ (𝑁‘𝑋)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑆 ∈ (𝑁‘𝑦))))
Theorem	ntrneineine0 41918*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅))
Theorem	ntrneineine1 41919*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ 𝒫 𝐵))
Theorem	ntrneicls00 41920*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 2-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ((𝐼‘𝐵) = 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥)))
Theorem	ntrneicls11 41921*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the interior of the empty set is the empty set hold equally. (Contributed by RP, 2-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → ((𝐼‘∅) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ ∅ ∈ (𝑁‘𝑥)))
Theorem	ntrneiiso 41922*	If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then conditions equal to claiming that the interior function is isotonic hold equally. (Contributed by RP, 3-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))))
Theorem	ntrneik2 41923*	An interior function is contracting if and only if all the neighborhoods of a point contain that point. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) → 𝑥 ∈ 𝑠)))
Theorem	ntrneix2 41924*	An interior (closure) function is expansive if and only if all subsets which contain a point are neighborhoods (convergents) of that point. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑥 ∈ 𝑠 → 𝑠 ∈ (𝑁‘𝑥))))
Theorem	ntrneikb 41925*	The interiors of disjoint sets are disjoint if and only if the neighborhoods of every point contain no disjoint sets. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)))
Theorem	ntrneixb 41926*	The interiors (closures) of sets that span the base set also span the base set if and only if the neighborhoods (convergents) of every point contain at least one of every pair of sets that span the base set. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) = 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))
Theorem	ntrneik3 41927*	The intersection of interiors of any pair is a subset of the interior of the intersection if and only if the intersection of any two neighborhoods of a point is also a neighborhood. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥))))
Theorem	ntrneix3 41928*	The closure of the union of any pair is a subset of the union of closures if and only if the union of any pair belonging to the convergents of a point implies at least one of the pair belongs to the the convergents of that point. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∪ 𝑡)) ⊆ ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) ∈ (𝑁‘𝑥) → (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))
Theorem	ntrneik13 41929*	The interior of the intersection of any pair equals intersection of interiors if and only if the intersection of any pair belonging to the neighborhood of a point is equivalent to both of the pair belonging to the neighborhood of that point. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))))
Theorem	ntrneix13 41930*	The closure of the union of any pair is equal to the union of closures if and only if the union of any pair belonging to the convergents of a point if equivalent to at least one of the pain belonging to the convergents of that point. (Contributed by RP, 19-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∪ 𝑡)) = ((𝐼‘𝑠) ∪ (𝐼‘𝑡)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) ∈ (𝑁‘𝑥) ↔ (𝑠 ∈ (𝑁‘𝑥) ∨ 𝑡 ∈ (𝑁‘𝑥)))))
Theorem	ntrneik4w 41931*	Idempotence of the interior function is equivalent to saying a set is a neighborhood of a point if and only if the interior of the set is a neighborhood of a point. (Contributed by RP, 11-Jul-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ↔ (𝐼‘𝑠) ∈ (𝑁‘𝑥))))
Theorem	ntrneik4 41932*	Idempotence of the interior function is equivalent to stating a set, 𝑠, is a neighborhood of a point, 𝑥 is equivalent to there existing a special neighborhood, 𝑢, of 𝑥 such that a point is an element of the special neighborhood if and only if 𝑠 is also a neighborhood of the point. (Contributed by RP, 11-Jul-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ (𝜑 → 𝐼𝐹𝑁)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑢 ∈ (𝑁‘𝑥)∀𝑦 ∈ 𝐵 (𝑦 ∈ 𝑢 ↔ 𝑠 ∈ (𝑁‘𝑦)))))
Theorem	clsneibex 41933	If (pseudo-)closure and (pseudo-)neighborhood functions are related by the composite operator, 𝐻, then the base set exists. (Contributed by RP, 4-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	clsneircomplex 41934	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	clsneif1o 41935*	If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then the operator is a one-to-one, onto mapping. (Contributed by RP, 5-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝐻:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	clsneicnv 41936*	If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then the converse of the operator is known. (Contributed by RP, 5-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → ◡𝐻 = (𝐷 ∘ (𝐵𝑂𝒫 𝐵)))
Theorem	clsneikex 41937*	If closure and neighborhoods functions are related, the closure function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
Theorem	clsneinex 41938*	If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	clsneiel1 41939*	If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then membership in the closure of a subset is equivalent to the complement of the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝑆) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋)))
Theorem	clsneiel2 41940*	If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the 𝐻 operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆)) ↔ ¬ 𝑆 ∈ (𝑁‘𝑋)))
Theorem	clsneifv3 41941*	Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑠))})
Theorem	clsneifv4 41942*	Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘𝑆) = {𝑥 ∈ 𝐵 ∣ ¬ (𝐵 ∖ 𝑆) ∈ (𝑁‘𝑥)})
Theorem	neicvgbex 41943	If (pseudo-)neighborhood and (pseudo-)convergent functions are related by the composite operator, 𝐻, then the base set exists. (Contributed by RP, 4-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	neicvgrcomplex 41944	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	neicvgf1o 41945*	If neighborhood and convergent functions are related by operator 𝐻, it is a one-to-one onto relation. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝐻:(𝒫 𝒫 𝐵 ↑m 𝐵)–1-1-onto→(𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgnvo 41946*	If neighborhood and convergent functions are related by operator 𝐻, it is its own converse function. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → ◡𝐻 = 𝐻)
Theorem	neicvgnvor 41947*	If neighborhood and convergent functions are related by operator 𝐻, the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑀𝐻𝑁)
Theorem	neicvgmex 41948*	If the neighborhoods and convergents functions are related, the convergents function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgnex 41949*	If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))
Theorem	neicvgel1 41950*	A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑆 ∈ (𝑁‘𝑋) ↔ ¬ (𝐵 ∖ 𝑆) ∈ (𝑀‘𝑋)))
Theorem	neicvgel2 41951*	The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐵 ∖ 𝑆) ∈ (𝑁‘𝑋) ↔ ¬ 𝑆 ∈ (𝑀‘𝑋)))
Theorem	neicvgfv 41952*	The value of the neighborhoods (convergents) in terms of the the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)})
Theorem	ntrrn 41953	The range of the interior function of a topology a subset of the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → ran 𝐼 ⊆ 𝐽)
Theorem	ntrf 41954	The interior function of a topology is a map from the powerset of the base set to the open sets of the topology. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝐽)
Theorem	ntrf2 41955	The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼:𝒫 𝑋⟶𝒫 𝑋)
Theorem	ntrelmap 41956	The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐼 = (int‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋))
Theorem	clsf2 41957	The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 22271. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)
Theorem	clselmap 41958	The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 ∈ (𝒫 𝑋 ↑m 𝒫 𝑋))
Theorem	dssmapntrcls 41959*	The interior and closure operators on a topology are duals of each other. See also kur14lem2 33274. (Contributed by RP, 21-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾))
Theorem	dssmapclsntr 41960*	The closure and interior operators on a topology are duals of each other. See also kur14lem2 33274. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 = (𝐷‘𝐼))
21.31.5.3  Generic Neighborhood Spaces Any neighborhood space is an open set topology and any open set topology is a neighborhood space. Seifert and Threlfall define a generic neighborhood space which is a superset of what is now generally used and related concepts and the following will show that those definitions apply to elements of Top. Seifert and Threlfall do not allow neighborhood spaces on the empty set while sn0top 22221 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.
Theorem	gneispa 41961*	Each point 𝑝 of the neighborhood space has at least one neighborhood; each neighborhood of 𝑝 contains 𝑝. Axiom A of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ∀𝑝 ∈ 𝑋 (((nei‘𝐽)‘{𝑝}) ≠ ∅ ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑝})𝑝 ∈ 𝑛))
Theorem	gneispb 41962*	Given a neighborhood 𝑁 of 𝑃, each subset of the neighborhood space containing this neighborhood is also a neighborhood of 𝑃. Axiom B of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∀𝑠 ∈ 𝒫 𝑋(𝑁 ⊆ 𝑠 → 𝑠 ∈ ((nei‘𝐽)‘{𝑃})))
Theorem	gneispace2 41963*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
Theorem	gneispace3 41964*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
Theorem	gneispace 41965*	The predicate that 𝐹 is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))))
Theorem	gneispacef 41966*	A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
Theorem	gneispacef2 41967*	A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → 𝐹:dom 𝐹⟶𝒫 𝒫 dom 𝐹)
Theorem	gneispacefun 41968*	A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹)
Theorem	gneispacern 41969*	A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
Theorem	gneispacern2 41970*	A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
Theorem	gneispace0nelrn 41971*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)
Theorem	gneispace0nelrn2 41972*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) → (𝐹‘𝑃) ≠ ∅)
Theorem	gneispace0nelrn3 41973*	A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ¬ ∅ ∈ ran 𝐹)
Theorem	gneispaceel 41974*	Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)𝑝 ∈ 𝑛)
Theorem	gneispaceel2 41975*	Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ∧ 𝑁 ∈ (𝐹‘𝑃)) → 𝑃 ∈ 𝑁)
Theorem	gneispacess 41976*	All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))
Theorem	gneispacess2 41977*	All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) ∧ (𝑁 ∈ (𝐹‘𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃))
21.31.6  Exploring Higher Homotopy via Kerodon See https://kerodon.net/ for a work in progress by Jacob Lurie.
21.31.6.1  Simplicial Sets See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension 𝑁.
Theorem	k0004lem1 41978	Application of ssin 4175 to range of a function. (Contributed by RP, 1-Apr-2021.)
⊢ (𝐷 = (𝐵 ∩ 𝐶) → ((𝐹:𝐴⟶𝐵 ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹:𝐴⟶𝐷))
Theorem	k0004lem2 41979	A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m 𝐴) ∧ (𝐹 “ 𝐴) ⊆ 𝐶) ↔ 𝐹 ∈ (𝐶 ↑m 𝐴)))
Theorem	k0004lem3 41980	When the value of a mapping on a singleton is known, the mapping is a completely known singleton. (Contributed by RP, 2-Apr-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ 𝐹 = {⟨𝐴, 𝐶⟩}))
Theorem	k0004val 41981*	The topological simplex of dimension 𝑁 is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) = {𝑡 ∈ ((0[,]1) ↑m (1...(𝑁 + 1))) ∣ Σ𝑘 ∈ (1...(𝑁 + 1))(𝑡‘𝑘) = 1})
Theorem	k0004ss1 41982*	The topological simplex of dimension 𝑁 is a subset of the real vectors of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (ℝ ↑m (1...(𝑁 + 1))))
Theorem	k0004ss2 41983*	The topological simplex of dimension 𝑁 is a subset of the base set of a real vector space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(ℝ^‘(1...(𝑁 + 1)))))
Theorem	k0004ss3 41984*	The topological simplex of dimension 𝑁 is a subset of the base set of Euclidean space of dimension (𝑁 + 1). (Contributed by RP, 29-Mar-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴‘𝑁) ⊆ (Base‘(𝔼hil‘(𝑁 + 1))))
Theorem	k0004val0 41985*	The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.)
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1) ↑m (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1})    ⇒   ⊢ (𝐴‘0) = {{⟨1, 1⟩}}
21.32  Mathbox for Stanislas Polu
Theorem	inductionexd 41986	Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝑁 ∈ ℕ → 3 ∥ ((4↑𝑁) + 5))
21.32.1  IMO Problems
21.32.1.1  IMO 1972 B2
Theorem	wwlemuld 41987	Natural deduction form of lemul2d 12889. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	leeq1d 41988	Specialization of breq1d 5097 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐶)
Theorem	leeq2d 41989	Specialization of breq2d 5099 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐷)
Theorem	absmulrposd 41990	Specialization of absmuld with absidd 15206. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵)))
Theorem	imadisjld 41991	Natural dduction form of one side of imadisj 6005. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅)
Theorem	imadisjlnd 41992	Natural deduction form of one negated side of imadisj 6005. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) ≠ ∅)
Theorem	wnefimgd 41993	The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅)
Theorem	fco2d 41994	Natural deduction form of fco2 6664. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	wfximgfd 41995	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴))
Theorem	extoimad 41996*	If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝐶)
Theorem	imo72b2lem0 41997*	Lemma for imo72b2 42004. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵))))    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1)    ⇒   ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
Theorem	suprleubrd 41998*	Natural deduction form of specialized suprleub 12014. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵)
Theorem	imo72b2lem2 41999*	Lemma for imo72b2 42004. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶)    ⇒   ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶)
Theorem	suprlubrd 42000*	Natural deduction form of specialized suprlub 12012. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧)    ⇒   ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < ))