Metamath Proof Explorer

Theorem ntrneix2

Description: An interior (closure) function is expansive if and only if all subsets which contain a point are neighborhoods (convergents) of that point. (Contributed by RP, 11-Jun-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 ntrneix2 ⊢ φ → ∀ s ∈ 𝒫 B s ⊆ I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B x ∈ s → 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 simpr ⊢ φ ∧ s ∈ 𝒫 B → s ∈ 𝒫 B
5 elpwi ⊢ s ∈ 𝒫 B → s ⊆ B
6 5 sselda ⊢ s ∈ 𝒫 B ∧ x ∈ s → x ∈ B
7 biimt ⊢ x ∈ B → x ∈ I ⁡ s ↔ x ∈ B → x ∈ I ⁡ s
8 6 7 syl ⊢ s ∈ 𝒫 B ∧ x ∈ s → x ∈ I ⁡ s ↔ x ∈ B → x ∈ I ⁡ s
9 8 pm5.74da ⊢ s ∈ 𝒫 B → x ∈ s → x ∈ I ⁡ s ↔ x ∈ s → x ∈ B → x ∈ I ⁡ s
10 bi2.04 ⊢ x ∈ s → x ∈ B → x ∈ I ⁡ s ↔ x ∈ B → x ∈ s → x ∈ I ⁡ s
11 9 10 bitrdi ⊢ s ∈ 𝒫 B → x ∈ s → x ∈ I ⁡ s ↔ x ∈ B → x ∈ s → x ∈ I ⁡ s
12 11 albidv ⊢ s ∈ 𝒫 B → ∀ x x ∈ s → x ∈ I ⁡ s ↔ ∀ x x ∈ B → x ∈ s → x ∈ I ⁡ s
13 dfss2 ⊢ s ⊆ I ⁡ s ↔ ∀ x x ∈ s → x ∈ I ⁡ s
14 df-ral ⊢ ∀ x ∈ B x ∈ s → x ∈ I ⁡ s ↔ ∀ x x ∈ B → x ∈ s → x ∈ I ⁡ s
15 12 13 14 3bitr4g ⊢ s ∈ 𝒫 B → s ⊆ I ⁡ s ↔ ∀ x ∈ B x ∈ s → x ∈ I ⁡ s
16 4 15 syl ⊢ φ ∧ s ∈ 𝒫 B → s ⊆ I ⁡ s ↔ ∀ x ∈ B x ∈ s → x ∈ I ⁡ s
17 3 ad2antrr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → I F N
18 simpr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ B
19 simplr ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → s ∈ 𝒫 B
20 1 2 17 18 19 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ↔ s ∈ N ⁡ x
21 20 imbi2d ⊢ φ ∧ s ∈ 𝒫 B ∧ x ∈ B → x ∈ s → x ∈ I ⁡ s ↔ x ∈ s → s ∈ N ⁡ x
22 21 ralbidva ⊢ φ ∧ s ∈ 𝒫 B → ∀ x ∈ B x ∈ s → x ∈ I ⁡ s ↔ ∀ x ∈ B x ∈ s → s ∈ N ⁡ x
23 16 22 bitrd ⊢ φ ∧ s ∈ 𝒫 B → s ⊆ I ⁡ s ↔ ∀ x ∈ B x ∈ s → s ∈ N ⁡ x
24 23 ralbidva ⊢ φ → ∀ s ∈ 𝒫 B s ⊆ I ⁡ s ↔ ∀ s ∈ 𝒫 B ∀ x ∈ B x ∈ s → s ∈ N ⁡ x
25 ralcom ⊢ ∀ s ∈ 𝒫 B ∀ x ∈ B x ∈ s → s ∈ N ⁡ x ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B x ∈ s → s ∈ N ⁡ x
26 24 25 bitrdi ⊢ φ → ∀ s ∈ 𝒫 B s ⊆ I ⁡ s ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B x ∈ s → s ∈ N ⁡ x