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