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 ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
neicvg.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
neicvg.d ⊢ D = P ⁡ B
neicvg.f ⊢ F = 𝒫 B O B
neicvg.g ⊢ G = B O 𝒫 B
neicvg.h ⊢ H = F ∘ D ∘ G
neicvg.r ⊢ φ → N H M
neicvgel.x ⊢ φ → X ∈ B
neicvgel.s ⊢ φ → S ∈ 𝒫 B
Assertion neicvgel1 ⊢ φ → S ∈ N ⁡ X ↔ ¬ B ∖ S ∈ M ⁡ X

Proof

Step Hyp Ref Expression
1 neicvg.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 neicvg.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
3 neicvg.d ⊢ D = P ⁡ B
4 neicvg.f ⊢ F = 𝒫 B O B
5 neicvg.g ⊢ G = B O 𝒫 B
6 neicvg.h ⊢ H = F ∘ D ∘ G
7 neicvg.r ⊢ φ → N H M
8 neicvgel.x ⊢ φ → X ∈ B
9 neicvgel.s ⊢ φ → S ∈ 𝒫 B
10 3 6 7 neicvgbex ⊢ φ → B ∈ V
11 simpr ⊢ φ ∧ B ∈ V → B ∈ V
12 11 pwexd ⊢ φ ∧ B ∈ V → 𝒫 B ∈ V
13 1 12 11 4 fsovf1od ⊢ φ ∧ B ∈ V → F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
14 f1ofn ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → F Fn 𝒫 B 𝒫 B
15 13 14 syl ⊢ φ ∧ B ∈ V → F Fn 𝒫 B 𝒫 B
16 2 3 11 dssmapf1od ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
17 f1of ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
18 16 17 syl ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
19 1 11 12 5 fsovfd ⊢ φ ∧ B ∈ V → G : 𝒫 𝒫 B B ⟶ 𝒫 B 𝒫 B
20 6 breqi ⊢ N H M ↔ N F ∘ D ∘ G M
21 7 20 sylib ⊢ φ → N F ∘ D ∘ G M
22 21 adantr ⊢ φ ∧ B ∈ V → N F ∘ D ∘ G M
23 15 18 19 22 brcofffn ⊢ φ ∧ B ∈ V → N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M
24 10 23 mpdan ⊢ φ → N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M
25 simpr2 ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → G ⁡ N D D ⁡ G ⁡ N
26 8 adantr ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → X ∈ B
27 9 adantr ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → S ∈ 𝒫 B
28 2 3 25 26 27 ntrclselnel1 ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → X ∈ G ⁡ N ⁡ S ↔ ¬ X ∈ D ⁡ G ⁡ N ⁡ B ∖ S
29 eqid ⊢ 𝒫 B O B = 𝒫 B O B
30 simpr1 ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → N G G ⁡ N
31 5 breqi ⊢ N G G ⁡ N ↔ N B O 𝒫 B G ⁡ N
32 31 a1i ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → N G G ⁡ N ↔ N B O 𝒫 B G ⁡ N
33 10 adantr ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → B ∈ V
34 id ⊢ B ∈ V → B ∈ V
35 pwexg ⊢ B ∈ V → 𝒫 B ∈ V
36 eqid ⊢ B O 𝒫 B = B O 𝒫 B
37 1 34 35 36 fsovf1od ⊢ B ∈ V → B O 𝒫 B : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B
38 33 37 syl ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → B O 𝒫 B : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B
39 f1orel ⊢ B O 𝒫 B : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B → Rel ⁡ B O 𝒫 B
40 relbrcnvg ⊢ Rel ⁡ B O 𝒫 B → G ⁡ N B O 𝒫 B -1 N ↔ N B O 𝒫 B G ⁡ N
41 38 39 40 3syl ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → G ⁡ N B O 𝒫 B -1 N ↔ N B O 𝒫 B G ⁡ N
42 1 34 35 36 29 fsovcnvd ⊢ B ∈ V → B O 𝒫 B -1 = 𝒫 B O B
43 42 breqd ⊢ B ∈ V → G ⁡ N B O 𝒫 B -1 N ↔ G ⁡ N 𝒫 B O B N
44 33 43 syl ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → G ⁡ N B O 𝒫 B -1 N ↔ G ⁡ N 𝒫 B O B N
45 32 41 44 3bitr2d ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → N G G ⁡ N ↔ G ⁡ N 𝒫 B O B N
46 30 45 mpbid ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → G ⁡ N 𝒫 B O B N
47 1 29 46 26 27 ntrneiel ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → X ∈ G ⁡ N ⁡ S ↔ S ∈ N ⁡ X
48 simpr3 ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → D ⁡ G ⁡ N F M
49 difssd ⊢ φ → B ∖ S ⊆ B
50 10 49 sselpwd ⊢ φ → B ∖ S ∈ 𝒫 B
51 50 adantr ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → B ∖ S ∈ 𝒫 B
52 1 4 48 26 51 ntrneiel ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → X ∈ D ⁡ G ⁡ N ⁡ B ∖ S ↔ B ∖ S ∈ M ⁡ X
53 52 notbid ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → ¬ X ∈ D ⁡ G ⁡ N ⁡ B ∖ S ↔ ¬ B ∖ S ∈ M ⁡ X
54 28 47 53 3bitr3d ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → S ∈ N ⁡ X ↔ ¬ B ∖ S ∈ M ⁡ X
55 24 54 mpdan ⊢ φ → S ∈ N ⁡ X ↔ ¬ B ∖ S ∈ M ⁡ X