Metamath Proof Explorer

Theorem ntrneik4

Description: Idempotence of the interior function is equivalent to stating a set, s , is a neighborhood of a point, x is equivalent to there existing a special neighborhood, u , of x such that a point is an element of the special neighborhood if and only if s is also a neighborhood of the 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 ntrneik4 ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y

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 1 2 3 ntrneik4w ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x
5 3 ad2antrr ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → I F N
6 simplr ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → x ∈ B
7 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
8 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
9 7 8 syl ⊢ φ → I : 𝒫 B ⟶ 𝒫 B
10 9 ffvelcdmda ⊢ φ ∧ s ∈ 𝒫 B → I ⁡ s ∈ 𝒫 B
11 10 adantlr ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → I ⁡ s ∈ 𝒫 B
12 1 2 5 6 11 ntrneiel ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → x ∈ I ⁡ I ⁡ s ↔ I ⁡ s ∈ N ⁡ x
13 simpr ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → s ∈ 𝒫 B
14 1 2 5 6 13 ntrneiel2 ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → x ∈ I ⁡ I ⁡ s ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y
15 12 14 bitr3d ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → I ⁡ s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y
16 15 bibi2d ⊢ φ ∧ x ∈ B ∧ s ∈ 𝒫 B → s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x ↔ s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y
17 16 ralbidva ⊢ φ ∧ x ∈ B → ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x ↔ ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y
18 17 ralbidva ⊢ φ → ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ I ⁡ s ∈ N ⁡ x ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y
19 4 18 bitrd ⊢ φ → ∀ s ∈ 𝒫 B I ⁡ I ⁡ s = I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B s ∈ N ⁡ x ↔ ∃ u ∈ N ⁡ x ∀ y ∈ B y ∈ u ↔ s ∈ N ⁡ y