P. 449 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44801-44900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neik0pk1imk0 44801*	Kuratowski's K0' and K1 axioms imply K0. Neighborhood version. (Contributed by RP, 3-Jun-2021.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑m 𝐵))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥))
Theorem	isotone1 44802*	Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)
⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
Theorem	isotone2 44803*	Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)
⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝐹‘(𝑎 ∩ 𝑏)) ⊆ ((𝐹‘𝑎) ∩ (𝐹‘𝑏)))
Theorem	ntrk1k3eqk13 44804*	An interior function is both monotone and sub-linear if and only if it is finitely linear. (Contributed by RP, 18-Jun-2021.)
⊢ ((∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡))) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝑠 ∩ 𝑡)) = ((𝐼‘𝑠) ∩ (𝐼‘𝑡)))
Theorem	ntrclsf1o 44805*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐷:(𝒫 𝐵 ↑m 𝒫 𝐵)–1-1-onto→(𝒫 𝐵 ↑m 𝒫 𝐵))
Theorem	ntrclsnvobr 44806*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then they are related the opposite way. (Contributed by RP, 21-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐾𝐷𝐼)
Theorem	ntrclsiex 44807*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (Contributed by RP, 21-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
Theorem	ntrclskex 44808*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (Contributed by RP, 21-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵))
Theorem	ntrclsfv1 44809*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
Theorem	ntrclsfv2 44810*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (𝐷‘𝐾) = 𝐼)
Theorem	ntrclselnel1 44811*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality 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, 28-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ ¬ 𝑋 ∈ (𝐾‘(𝐵 ∖ 𝑆))))
Theorem	ntrclselnel2 44812*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in interior of the complement of a set and non-membership in the closure of the set. (Contributed by RP, 28-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐼‘(𝐵 ∖ 𝑆)) ↔ ¬ 𝑋 ∈ (𝐾‘𝑆)))
Theorem	ntrclsfv 44813*	The value of the interior (closure) expressed in terms of the closure (interior). (Contributed by RP, 25-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → (𝐼‘𝑆) = (𝐵 ∖ (𝐾‘(𝐵 ∖ 𝑆))))
Theorem	ntrclsfveq1 44814*	If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) = 𝐶 ↔ (𝐾‘(𝐵 ∖ 𝑆)) = (𝐵 ∖ 𝐶)))
Theorem	ntrclsfveq2 44815*	If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘(𝐵 ∖ 𝑆)) = 𝐶 ↔ (𝐾‘𝑆) = (𝐵 ∖ 𝐶)))
Theorem	ntrclsfveq 44816*	If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) = (𝐼‘𝑇) ↔ (𝐾‘(𝐵 ∖ 𝑆)) = (𝐾‘(𝐵 ∖ 𝑇))))
Theorem	ntrclsss 44817*	If interior and closure functions are related then a subset relation of a pair of function values is equivalent to subset relation of a pair of the other function's values. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ((𝐼‘𝑆) ⊆ (𝐼‘𝑇) ↔ (𝐾‘(𝐵 ∖ 𝑇)) ⊆ (𝐾‘(𝐵 ∖ 𝑆))))
Theorem	ntrclsneine0lem 44818*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that at least one (pseudo-)neighborbood of a particular point exists hold equally. (Contributed by RP, 21-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝐵𝑋 ∈ (𝐼‘𝑠) ↔ ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ (𝐾‘𝑠)))
Theorem	ntrclsneine0 44819*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 21-May-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵𝑥 ∈ (𝐼‘𝑠) ↔ ∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ (𝐾‘𝑠)))
Theorem	ntrclscls00 44820*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 1-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → ((𝐼‘𝐵) = 𝐵 ↔ (𝐾‘∅) = ∅))
Theorem	ntrclsiso 44821*	If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that either is isotonic hold equally. (Contributed by RP, 3-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐼‘𝑠) ⊆ (𝐼‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝑠 ⊆ 𝑡 → (𝐾‘𝑠) ⊆ (𝐾‘𝑡))))
Theorem	ntrclsk2 44822*	An interior function is contracting if and only if the closure function is expansive. (Contributed by RP, 9-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐾‘𝑠)))
Theorem	ntrclskb 44823*	The interiors of disjoint sets are disjoint if and only if the closures of sets that span the base set also span the base set. (Contributed by RP, 10-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∪ 𝑡) = 𝐵 → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = 𝐵)))
Theorem	ntrclsk3 44824*	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 44825*	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 44826*	Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-2021.)
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))    &   ⊢ 𝐷 = (𝑂‘𝐵)    &   ⊢ (𝜑 → 𝐼𝐷𝐾)    ⇒   ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)))
Theorem	ntrneibex 44827*	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 44828*	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 44829*	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 44830*	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 44831*	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 44832*	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 44833*	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 44834*	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 44835*	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 44836*	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 44837*	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 44838*	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 44839*	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 44840*	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 44841*	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 44842*	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 44843*	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 44844*	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 44845*	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 44846*	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 44847*	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 44848*	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 44849*	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 44850*	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 44851*	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 44852*	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 44853*	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 44854*	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 44855*	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 44856	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 44857	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐷)    &   ⊢ (𝜑 → 𝐾𝐻𝑁)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	clsneif1o 44858*	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 44859*	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 44860*	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 44861*	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 44862*	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 44863*	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 44864*	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 44865*	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 44866	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 44867	The relative complement of the class 𝑆 exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.)
⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    ⇒   ⊢ (𝜑 → (𝐵 ∖ 𝑆) ∈ 𝒫 𝐵)
Theorem	neicvgf1o 44868*	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 44869*	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 44870*	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 44871*	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 44872*	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 44873*	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 44874*	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 44875*	The value of the neighborhoods (convergents) in terms of the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.)
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)})))    &   ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜))))))    &   ⊢ 𝐷 = (𝑃‘𝐵)    &   ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵)    &   ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵)    &   ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺))    &   ⊢ (𝜑 → 𝑁𝐻𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = {𝑠 ∈ 𝒫 𝐵 ∣ ¬ (𝐵 ∖ 𝑠) ∈ (𝑀‘𝑋)})
Theorem	ntrrn 44876	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 44877	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 44878	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 44879	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 44880	The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 23216. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)
Theorem	clselmap 44881	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 44882*	The interior and closure operators on a topology are duals of each other. See also kur14lem2 35707. (Contributed by RP, 21-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾))
Theorem	dssmapclsntr 44883*	The closure and interior operators on a topology are duals of each other. See also kur14lem2 35707. (Contributed by RP, 22-Apr-2021.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))    &   ⊢ 𝐷 = (𝑂‘𝑋)    ⇒   ⊢ (𝐽 ∈ Top → 𝐾 = (𝐷‘𝐼))
21.37.7.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 23167 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems.
Theorem	gneispa 44884*	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 44885*	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 44886*	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 44887*	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 44888*	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 44889*	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 44890*	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 44891*	A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.)
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}    ⇒   ⊢ (𝐹 ∈ 𝐴 → Fun 𝐹)
Theorem	gneispacern 44892*	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 44893*	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 44894*	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 44895*	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 44896*	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 44897*	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 44898*	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 44899*	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 44900*	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 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃))