Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
ntrneineine0
Metamath Proof Explorer
Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related
by the operator, F , then conditions equal to claiming that for
every point, at least one (pseudo-)neighborbood exists hold equally.
(Contributed by RP , 29-May-2021)
Ref
Expression
Hypotheses
ntrnei.o
⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
ntrnei.f
⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r
⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion
ntrneineine0
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) )
Proof
Step
Hyp
Ref
Expression
1
ntrnei.o
⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2
ntrnei.f
⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3
ntrnei.r
⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4
3
adantr
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
5
simpr
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
6
1 2 4 5
ntrneineine0lem
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) )
7
6
ralbidva
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) )