Metamath Proof Explorer

Theorem ntrneik4w

Description: Idempotence of the interior function is equivalent to saying a set is a neighborhood of a point if and only if the interior of the set is a neighborhood of a point. (Contributed by RP, 11-Jul-2021)

Ref Expression
Hypotheses ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
ntrnei.f ⊢ F = 𝒫 B O B
ntrnei.r ⊢ φ → I F N
Assertion ntrneik4w ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 ntrnei.f ⊢ F = 𝒫 B O B
3 ntrnei.r ⊢ φ → I F N
4 dfcleq ⊢ I ⁡ s = I ⁡ I ⁡ s ↔ ∀ x x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
5 eqcom ⊢ I ⁡ I ⁡ s = I ⁡ s ↔ I ⁡ s = I ⁡ I ⁡ s
6 ralv ⊢ ∀ x ∈ V x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s ↔ ∀ x x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
7 4 5 6 3bitr4i ⊢ I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ V x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
8 ssv ⊢ B ⊆ V
9 8 a1i ⊢ φ ∧ s ∈ 𝒫 B → B ⊆ V
10 vex ⊢ x ∈ V
11 eldif ⊢ x ∈ V ∖ B ↔ x ∈ V ∧ ¬ x ∈ B
12 10 11 mpbiran ⊢ x ∈ V ∖ B ↔ ¬ x ∈ B
13 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
14 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
15 13 14 syl ⊢ φ → I : 𝒫 B ⟶ 𝒫 B
16 15 ffvelrnda ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ s ∈ 𝒫 B
17 16 elpwid ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ s ⊆ B
18 17 sseld ⊢ φ ∧ s ∈ 𝒫 B → x ∈ I ⁡ s → x ∈ B
19 18 con3dimp ⊢ φ ∧ s ∈ 𝒫 B ∧ ¬ x ∈ B → ¬ x ∈ I ⁡ s
20 15 adantr ⊢ φ ∧ s ∈ 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
21 20 16 ffvelrnd ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ I ⁡ s ∈ 𝒫 B
22 21 elpwid ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ I ⁡ s ⊆ B
23 22 sseld ⊢ φ ∧ s ∈ 𝒫 B → x ∈ I ⁡ I ⁡ s → x ∈ B
24 23 con3dimp ⊢ φ ∧ s ∈ 𝒫 B ∧ ¬ x ∈ B → ¬ x ∈ I ⁡ I ⁡ s
25 19 24 2falsed ⊢ φ ∧ s ∈ 𝒫 B ∧ ¬ x ∈ B → x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
26 25 ex ⊢ φ ∧ s ∈ 𝒫 B → ¬ x ∈ B → x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
27 12 26 syl5bi ⊢ φ ∧ s ∈ 𝒫 B → x ∈ V ∖ B → x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
28 27 ralrimiv ⊢ φ ∧ s ∈ 𝒫 B → ∀ x ∈ V ∖ B x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
29 9 28 raldifeq ⊢ φ ∧ s ∈ 𝒫 B → ∀ x ∈ B x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s ↔ ∀ x ∈ V x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s
30 3 adantr ⊢ φ ∧ s ∈ 𝒫 B → I F N
31 30 adantr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → I F N
32 simpr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ B
33 simplr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → s ∈ 𝒫 B
34 1 2 31 32 33 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ↔ s ∈ N ⁡ x
35 16 adantr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → I ⁡ s ∈ 𝒫 B
36 1 2 31 32 35 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ I ⁡ s ↔ I ⁡ s ∈ N ⁡ x
37 34 36 bibi12d ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s ↔ s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
38 37 ralbidva ⊢ φ ∧ s ∈ 𝒫 B → ∀ x ∈ B x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s ↔ ∀ x ∈ B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
39 29 38 bitr3d ⊢ φ ∧ s ∈ 𝒫 B → ∀ x ∈ V x ∈ I ⁡ s ↔ x ∈ I ⁡ I ⁡ s ↔ ∀ x ∈ B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
40 7 39 syl5bb ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
41 40 ralbidva ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ s ∈ 𝒫 B ∀ x ∈ B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
42 ralcom ⊢ ∀ s ∈ 𝒫 B ∀ x ∈ B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
43 41 42 bitrdi ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x