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 ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion ntrneix2 ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
5 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
6 5 sselda ⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝑠 ) → 𝑥 ∈ 𝐵 )
7 biimt ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
8 6 7 syl ⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝑠 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
9 8 pm5.74da ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ( 𝑥 ∈ 𝑠 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) ) )
10 bi2.04 ⊢ ( ( 𝑥 ∈ 𝑠 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
11 9 10 bitrdi ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) ) )
12 11 albidv ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) ) )
13 dfss2 ⊢ ( 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) )
14 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
15 12 13 14 3bitr4g ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
16 4 15 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ) )
17 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
20 1 2 17 18 19 ntrneiel ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
21 20 imbi2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
22 21 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
23 16 22 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
24 23 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
25 ralcom ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
26 24 25 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ⊆ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑥 ∈ 𝑠 → 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )