Metamath Proof Explorer

Theorem neiss2

Description: A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007)

Ref Expression
Hypothesis neifval.1 ⊢ X = ⋃ J
Assertion neiss2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ X

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 elfvdm ⊢ N ∈ nei ⁡ J ⁡ S → S ∈ dom ⁡ nei ⁡ J
3 2 adantl ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ∈ dom ⁡ nei ⁡ J
4 1 neif ⊢ J ∈ Top → nei ⁡ J Fn 𝒫 X
5 fndm ⊢ nei ⁡ J Fn 𝒫 X → dom ⁡ nei ⁡ J = 𝒫 X
6 4 5 syl ⊢ J ∈ Top → dom ⁡ nei ⁡ J = 𝒫 X
7 6 eleq2d ⊢ J ∈ Top → S ∈ dom ⁡ nei ⁡ J ↔ S ∈ 𝒫 X
8 7 adantr ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ∈ dom ⁡ nei ⁡ J ↔ S ∈ 𝒫 X
9 3 8 mpbid ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ∈ 𝒫 X
10 9 elpwid ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ S → S ⊆ X