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	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
Assertion	gneispace0nelrn3	⊢ ( 𝐹 ∈ 𝐴 → ¬ ∅ ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2	1	gneispacern	⊢ ( 𝐹 ∈ 𝐴 → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
3		neldifsnd	⊢ ( ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) → ¬ ∅ ∈ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
4		ssel	⊢ ( ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) → ( ∅ ∈ ran 𝐹 → ∅ ∈ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
5	3 4	mtod	⊢ ( ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) → ¬ ∅ ∈ ran 𝐹 )
6	2 5	syl	⊢ ( 𝐹 ∈ 𝐴 → ¬ ∅ ∈ ran 𝐹 )