Theorem neircl

Description: Reverse closure of the neighborhood operation. (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 Zhi Wang, 16-Sep-2024)

	Ref	Expression
Assertion	neircl	|- ( N e. ( ( nei ` J ) ` S ) -> J e. Top )

Proof

Step	Hyp	Ref	Expression
1		elfvne0	|- ( N e. ( ( nei ` J ) ` S ) -> ( nei ` J ) =/= (/) )
2		n0	|- ( ( nei ` J ) =/= (/) <-> E. f f e. ( nei ` J ) )
3	2	biimpi	|- ( ( nei ` J ) =/= (/) -> E. f f e. ( nei ` J ) )
4		df-nei	|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
5	4	mptrcl	|- ( f e. ( nei ` J ) -> J e. Top )
6	5	exlimiv	|- ( E. f f e. ( nei ` J ) -> J e. Top )
7	1 3 6	3syl	|- ( N e. ( ( nei ` J ) ` S ) -> J e. Top )