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∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
Assertion ntrneik4 ⊢φ→∀s∈𝒫BI⁡I⁡s=I⁡s↔∀x∈B∀s∈𝒫Bs∈N⁡x↔∃u∈N⁡x∀y∈By∈u↔s∈N⁡y

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
4 1 2 3 ntrneik4w ⊢φ→∀s∈𝒫BI⁡I⁡s=I⁡s↔∀x∈B∀s∈𝒫Bs∈N⁡x↔I⁡s∈N⁡x
5 3 ad2antrr ⊢φ∧x∈B∧s∈𝒫B→IFN
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∈By∈u↔s∈N⁡y
15 12 14 bitr3d ⊢φ∧x∈B∧s∈𝒫B→I⁡s∈N⁡x↔∃u∈N⁡x∀y∈By∈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∈By∈u↔s∈N⁡y
17 16 ralbidva ⊢φ∧x∈B→∀s∈𝒫Bs∈N⁡x↔I⁡s∈N⁡x↔∀s∈𝒫Bs∈N⁡x↔∃u∈N⁡x∀y∈By∈u↔s∈N⁡y
18 17 ralbidva ⊢φ→∀x∈B∀s∈𝒫Bs∈N⁡x↔I⁡s∈N⁡x↔∀x∈B∀s∈𝒫Bs∈N⁡x↔∃u∈N⁡x∀y∈By∈u↔s∈N⁡y
19 4 18 bitrd ⊢φ→∀s∈𝒫BI⁡I⁡s=I⁡s↔∀x∈B∀s∈𝒫Bs∈N⁡x↔∃u∈N⁡x∀y∈By∈u↔s∈N⁡y