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 4 fndmd J Top dom nei J = 𝒫 X
6 5 eleq2d J Top S dom nei J S 𝒫 X
7 6 adantr J Top N nei J S S dom nei J S 𝒫 X
8 3 7 mpbid J Top N nei J S S 𝒫 X
9 8 elpwid J Top N nei J S S X