Metamath Proof Explorer

Theorem gneispace0nelrn

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 gneispace0nelrn ⊢F∈A→∀p∈dom⁡FF⁡p≠∅

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 elex ⊢F∈A→F∈V
3 1 gneispace ⊢F∈V→F∈A↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
4 2 3 syl ⊢F∈A→F∈A↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
5 4 ibi ⊢F∈A→Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
6 5 simp3d ⊢F∈A→∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
7 simpl ⊢F⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→F⁡p≠∅
8 7 ralimi ⊢∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅
9 6 8 syl ⊢F∈A→∀p∈dom⁡FF⁡p≠∅