Metamath Proof Explorer

Theorem gneispace0nelrn3

Description: A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021)

Ref Expression
Hypothesis gneispace.a ⊢A=f|f:dom⁡f⟶𝒫𝒫dom⁡f∖∅∖∅∧∀p∈dom⁡f∀n∈f⁡pp∈n∧∀s∈𝒫dom⁡fn⊆s→s∈f⁡p
Assertion gneispace0nelrn3 ⊢F∈A→¬∅∈ran⁡F

Proof

Step Hyp Ref Expression
1 gneispace.a ⊢A=f|f:dom⁡f⟶𝒫𝒫dom⁡f∖∅∖∅∧∀p∈dom⁡f∀n∈f⁡pp∈n∧∀s∈𝒫dom⁡fn⊆s→s∈f⁡p
2 1 gneispacern ⊢F∈A→ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
3 neldifsnd ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→¬∅∈𝒫𝒫dom⁡F∖∅∖∅
4 ssel ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→∅∈ran⁡F→∅∈𝒫𝒫dom⁡F∖∅∖∅
5 3 4 mtod ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→¬∅∈ran⁡F
6 2 5 syl ⊢F∈A→¬∅∈ran⁡F