Metamath Proof Explorer

Theorem neicvgel1

Description: A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021)

Ref Expression
Hypotheses neicvg.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
neicvg.p ⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
neicvg.d ⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
neicvg.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
neicvg.g ⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
neicvg.h ⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
neicvg.r ⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
neicvgel.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
neicvgel.s ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion neicvgel1 ( 𝜑 → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 neicvg.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 neicvg.p ⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
3 neicvg.d ⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
4 neicvg.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
5 neicvg.g ⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
6 neicvg.h ⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
7 neicvg.r ⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
8 neicvgel.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 neicvgel.s ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
10 3 6 7 neicvgbex ⊢ ( 𝜑 → 𝐵 ∈ V )
11 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
12 11 pwexd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
13 1 12 11 4 fsovf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
14 f1ofn ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
16 2 3 11 dssmapf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
17 f1of ⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
19 1 11 12 5 fsovfd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐺 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
20 6 breqi ⊢ ( 𝑁 𝐻 𝑀 ↔ 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
21 7 20 sylib ⊢ ( 𝜑 → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
23 15 18 19 22 brcofffn ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
24 10 23 mpdan ⊢ ( 𝜑 → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
25 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) )
26 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑋 ∈ 𝐵 )
27 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑆 ∈ 𝒫 𝐵 )
28 2 3 25 26 27 ntrclselnel1 ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐺 ‘ 𝑁 ) ‘ 𝑆 ) ↔ ¬ 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
29 eqid ⊢ ( 𝒫 𝐵 𝑂 𝐵 ) = ( 𝒫 𝐵 𝑂 𝐵 )
30 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) )
31 5 breqi ⊢ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) )
32 31 a1i ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
33 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → 𝐵 ∈ V )
34 id ⊢ ( 𝐵 ∈ V → 𝐵 ∈ V )
35 pwexg ⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
36 eqid ⊢ ( 𝐵 𝑂 𝒫 𝐵 ) = ( 𝐵 𝑂 𝒫 𝐵 )
37 1 34 35 36 fsovf1od ⊢ ( 𝐵 ∈ V → ( 𝐵 𝑂 𝒫 𝐵 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
38 f1orel ⊢ ( ( 𝐵 𝑂 𝒫 𝐵 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → Rel ( 𝐵 𝑂 𝒫 𝐵 ) )
39 relbrcnvg ⊢ ( Rel ( 𝐵 𝑂 𝒫 𝐵 ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
40 33 37 38 39 4syl ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ 𝑁 ( 𝐵 𝑂 𝒫 𝐵 ) ( 𝐺 ‘ 𝑁 ) ) )
41 1 34 35 36 29 fsovcnvd ⊢ ( 𝐵 ∈ V → ◡ ( 𝐵 𝑂 𝒫 𝐵 ) = ( 𝒫 𝐵 𝑂 𝐵 ) )
42 41 breqd ⊢ ( 𝐵 ∈ V → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
43 33 42 syl ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ( 𝐺 ‘ 𝑁 ) ◡ ( 𝐵 𝑂 𝒫 𝐵 ) 𝑁 ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
44 32 40 43 3bitr2d ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ↔ ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 ) )
45 30 44 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐺 ‘ 𝑁 ) ( 𝒫 𝐵 𝑂 𝐵 ) 𝑁 )
46 1 29 45 26 27 ntrneiel ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐺 ‘ 𝑁 ) ‘ 𝑆 ) ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ) )
47 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 )
48 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ⊆ 𝐵 )
49 10 48 sselpwd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
51 1 4 47 26 50 ntrneiel ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
52 51 notbid ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( ¬ 𝑋 ∈ ( ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
53 28 46 52 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) ) → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )
54 24 53 mpdan ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑀 ‘ 𝑋 ) ) )