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∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
Assertion ntrneix2 ⊢φ→∀s∈𝒫Bs⊆I⁡s↔∀x∈B∀s∈𝒫Bx∈s→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 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→∀xx∈s→x∈I⁡s↔∀xx∈B→x∈s→x∈I⁡s
13 dfss2 ⊢s⊆I⁡s↔∀xx∈s→x∈I⁡s
14 df-ral ⊢∀x∈Bx∈s→x∈I⁡s↔∀xx∈B→x∈s→x∈I⁡s
15 12 13 14 3bitr4g ⊢s∈𝒫B→s⊆I⁡s↔∀x∈Bx∈s→x∈I⁡s
16 4 15 syl ⊢φ∧s∈𝒫B→s⊆I⁡s↔∀x∈Bx∈s→x∈I⁡s
17 3 ad2antrr ⊢φ∧s∈𝒫B∧x∈B→IFN
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∈Bx∈s→x∈I⁡s↔∀x∈Bx∈s→s∈N⁡x
23 16 22 bitrd ⊢φ∧s∈𝒫B→s⊆I⁡s↔∀x∈Bx∈s→s∈N⁡x
24 23 ralbidva ⊢φ→∀s∈𝒫Bs⊆I⁡s↔∀s∈𝒫B∀x∈Bx∈s→s∈N⁡x
25 ralcom ⊢∀s∈𝒫B∀x∈Bx∈s→s∈N⁡x↔∀x∈B∀s∈𝒫Bx∈s→s∈N⁡x
26 24 25 bitrdi ⊢φ→∀s∈𝒫Bs⊆I⁡s↔∀x∈B∀s∈𝒫Bx∈s→s∈N⁡x