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 ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ 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 ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ 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