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

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 dfcleq ⊢I⁡s=I⁡I⁡s↔∀xx∈I⁡s↔x∈I⁡I⁡s
5 eqcom ⊢I⁡I⁡s=I⁡s↔I⁡s=I⁡I⁡s
6 ralv ⊢∀x∈Vx∈I⁡s↔x∈I⁡I⁡s↔∀xx∈I⁡s↔x∈I⁡I⁡s
7 4 5 6 3bitr4i ⊢I⁡I⁡s=I⁡s↔∀x∈Vx∈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 ffvelcdmda ⊢φ∧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 ffvelcdmd ⊢φ∧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 biimtrid ⊢φ∧s∈𝒫B→x∈V∖B→x∈I⁡s↔x∈I⁡I⁡s
28 27 ralrimiv ⊢φ∧s∈𝒫B→∀x∈V∖Bx∈I⁡s↔x∈I⁡I⁡s
29 9 28 raldifeq ⊢φ∧s∈𝒫B→∀x∈Bx∈I⁡s↔x∈I⁡I⁡s↔∀x∈Vx∈I⁡s↔x∈I⁡I⁡s
30 3 adantr ⊢φ∧s∈𝒫B→IFN
31 30 adantr ⊢φ∧s∈𝒫B∧x∈B→IFN
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∈Bx∈I⁡s↔x∈I⁡I⁡s↔∀x∈Bs∈N⁡x↔I⁡s∈N⁡x
39 29 38 bitr3d ⊢φ∧s∈𝒫B→∀x∈Vx∈I⁡s↔x∈I⁡I⁡s↔∀x∈Bs∈N⁡x↔I⁡s∈N⁡x
40 7 39 bitrid ⊢φ∧s∈𝒫B→I⁡I⁡s=I⁡s↔∀x∈Bs∈N⁡x↔I⁡s∈N⁡x
41 40 ralbidva ⊢φ→∀s∈𝒫BI⁡I⁡s=I⁡s↔∀s∈𝒫B∀x∈Bs∈N⁡x↔I⁡s∈N⁡x
42 ralcom ⊢∀s∈𝒫B∀x∈Bs∈N⁡x↔I⁡s∈N⁡x↔∀x∈B∀s∈𝒫Bs∈N⁡x↔I⁡s∈N⁡x
43 41 42 bitrdi ⊢φ→∀s∈𝒫BI⁡I⁡s=I⁡s↔∀x∈B∀s∈𝒫Bs∈N⁡x↔I⁡s∈N⁡x