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 f1orel ⊢ B O 𝒫 B : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B → Rel ⁡ B O 𝒫 B
39 relbrcnvg ⊢ Rel ⁡ B O 𝒫 B → G ⁡ N B O 𝒫 B -1 N ↔ N B O 𝒫 B G ⁡ N
40 33 37 38 39 4syl ⊢ φ ∧ 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
41 1 34 35 36 29 fsovcnvd ⊢ B ∈ V → B O 𝒫 B -1 = 𝒫 B O B
42 41 breqd ⊢ B ∈ V → G ⁡ N B O 𝒫 B -1 N ↔ G ⁡ N 𝒫 B O B N
43 33 42 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
44 32 40 43 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
45 30 44 mpbid ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → G ⁡ N 𝒫 B O B N
46 1 29 45 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
47 simpr3 ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → D ⁡ G ⁡ N F M
48 difssd ⊢ φ → B ∖ S ⊆ B
49 10 48 sselpwd ⊢ φ → B ∖ S ∈ 𝒫 B
50 49 adantr ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → B ∖ S ∈ 𝒫 B
51 1 4 47 26 50 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
52 51 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
53 28 46 52 3bitr3d ⊢ φ ∧ N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M → S ∈ N ⁡ X ↔ ¬ B ∖ S ∈ M ⁡ X
54 24 53 mpdan ⊢ φ → S ∈ N ⁡ X ↔ ¬ B ∖ S ∈ M ⁡ X