Metamath Proof Explorer

Theorem neibastop2

Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
Assertion neibastop2 ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
3 neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
4 neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
5 neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
6 neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
7 1 2 3 4 neibastop1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
8 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
9 7 8 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ Top )
11 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
12 11 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑁 ⊆ ∪ 𝐽 )
13 10 12 sylan ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑁 ⊆ ∪ 𝐽 )
14 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15 7 14 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑋 = ∪ 𝐽 )
17 13 16 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑁 ⊆ 𝑋 )
18 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∃ 𝑦 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) )
19 10 18 sylan ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∃ 𝑦 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) )
20 pweq ⊢ ( 𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦 )
21 20 ineq2d ⊢ ( 𝑜 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) )
22 21 neeq1d ⊢ ( 𝑜 = 𝑦 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
23 22 raleqbi1dv ⊢ ( 𝑜 = 𝑦 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
24 23 4 elrab2 ⊢ ( 𝑦 ∈ 𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
25 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → 𝑦 ⊆ 𝑁 )
26 25 sspwd ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → 𝒫 𝑦 ⊆ 𝒫 𝑁 )
27 sslin ⊢ ( 𝒫 𝑦 ⊆ 𝒫 𝑁 → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) )
28 26 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) )
29 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → { 𝑃 } ⊆ 𝑦 )
30 snssg ⊢ ( 𝑃 ∈ 𝑋 → ( 𝑃 ∈ 𝑦 ↔ { 𝑃 } ⊆ 𝑦 ) )
31 30 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → ( 𝑃 ∈ 𝑦 ↔ { 𝑃 } ⊆ 𝑦 ) )
32 29 31 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → 𝑃 ∈ 𝑦 )
33 fveq2 ⊢ ( 𝑥 = 𝑃 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑃 ) )
34 33 ineq1d ⊢ ( 𝑥 = 𝑃 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) = ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) )
35 34 neeq1d ⊢ ( 𝑥 = 𝑃 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
36 35 rspcv ⊢ ( 𝑃 ∈ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
37 32 36 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
38 ssn0 ⊢ ( ( ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ )
39 28 37 38 syl6an ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) )
40 39 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )
41 40 com23 ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ( ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )
42 41 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) → ( ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )
43 24 42 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝑦 ∈ 𝐽 → ( ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )
44 43 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ∃ 𝑦 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) )
45 19 44 mpd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ )
46 17 45 jca ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝑁 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) )
47 46 ex ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) → ( 𝑁 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )
48 n0 ⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) )
49 elin ⊢ ( 𝑠 ∈ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ↔ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) )
50 simprl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑁 ⊆ 𝑋 )
51 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑋 = ∪ 𝐽 )
52 50 51 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑁 ⊆ ∪ 𝐽 )
53 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑋 ∈ 𝑉 )
54 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
55 simpll ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝜑 )
56 55 3 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
57 55 5 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
58 55 6 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑃 ∈ 𝑋 )
60 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) )
61 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑠 ∈ 𝒫 𝑁 )
62 61 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑠 ⊆ 𝑁 )
63 fveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑥 ) )
64 63 ineq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑏 ) )
65 64 cbviunv ⊢ ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) = ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑏 )
66 pweq ⊢ ( 𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧 )
67 66 ineq2d ⊢ ( 𝑏 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑏 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
68 67 iuneq2d ⊢ ( 𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑏 ) = ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
69 65 68 syl5eq ⊢ ( 𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) = ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
70 69 cbviunv ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 )
71 70 mpteq2i ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
72 rdgeq1 ⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑠 } ) )
73 71 72 ax-mp ⊢ rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑠 } )
74 73 reseq1i ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑠 } ) ↾ ω )
75 pweq ⊢ ( 𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓 )
76 75 ineq2d ⊢ ( 𝑔 = 𝑓 → ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑔 ) = ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) )
77 76 neeq1d ⊢ ( 𝑔 = 𝑓 → ( ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑔 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
78 77 cbvrexvw ⊢ ( ∃ 𝑔 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑔 ) ≠ ∅ ↔ ∃ 𝑓 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) ≠ ∅ )
79 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
80 79 ineq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) = ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) )
81 80 neeq1d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
82 81 rexbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑓 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ∃ 𝑓 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
83 78 82 syl5bb ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑔 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑔 ) ≠ ∅ ↔ ∃ 𝑓 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
84 83 cbvrabv ⊢ { 𝑤 ∈ 𝑋 ∣ ∃ 𝑔 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑤 ) ∩ 𝒫 𝑔 ) ≠ ∅ } = { 𝑦 ∈ 𝑋 ∣ ∃ 𝑓 ∈ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ( ( 𝐹 ‘ 𝑛 ) ∩ 𝒫 𝑏 ) ) , { 𝑠 } ) ↾ ω ) ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ }
85 53 54 56 4 57 58 59 50 60 62 74 84 neibastop2lem ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) )
86 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝐽 ∈ Top )
87 59 51 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑃 ∈ ∪ 𝐽 )
88 11 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) ) ) )
89 86 87 88 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) ) ) )
90 52 85 89 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑁 ⊆ 𝑋 ∧ ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) ) ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
91 90 expr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑠 ∈ 𝒫 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
92 49 91 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑠 ∈ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
93 92 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑠 𝑠 ∈ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
94 48 93 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
95 94 expimpd ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
96 47 95 impbid ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑁 ) ≠ ∅ ) ) )