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	⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		elfvne0	⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → ( nei ‘ 𝐽 ) ≠ ∅ )
2		n0	⊢ ( ( nei ‘ 𝐽 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( nei ‘ 𝐽 ) )
3	2	biimpi	⊢ ( ( nei ‘ 𝐽 ) ≠ ∅ → ∃ 𝑓 𝑓 ∈ ( nei ‘ 𝐽 ) )
4		df-nei	⊢ nei = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) } ) )
5	4	mptrcl	⊢ ( 𝑓 ∈ ( nei ‘ 𝐽 ) → 𝐽 ∈ Top )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( nei ‘ 𝐽 ) → 𝐽 ∈ Top )
7	1 3 6	3syl	⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝐽 ∈ Top )