Metamath Proof Explorer

Theorem ntrneik3

Description: The intersection of interiors of any pair is a subset of the interior of the intersection if and only if the intersection of any two neighborhoods of a point is also a neighborhood. (Contributed by RP, 19-Jun-2021)

Ref Expression
Hypotheses ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion ntrneik3 ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4 dfss3 ⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) )
5 1 2 3 ntrneiiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
7 5 6 syl ⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
9 8 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
10 ssinss1 ⊢ ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
12 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
13 ralss ⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
14 12 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
15 elin ⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
16 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
17 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
19 1 2 16 17 18 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
21 1 2 16 17 20 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
22 19 21 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
23 15 22 syl5bb ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
24 1 2 3 ntrneibex ⊢ ( 𝜑 → 𝐵 ∈ V )
25 24 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ V )
26 18 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ⊆ 𝐵 )
27 ssinss1 ⊢ ( 𝑠 ⊆ 𝐵 → ( 𝑠 ∩ 𝑡 ) ⊆ 𝐵 )
28 26 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ⊆ 𝐵 )
29 25 28 sselpwd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ∈ 𝒫 𝐵 )
30 1 2 16 17 29 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
31 23 30 imbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
32 31 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
33 14 32 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
34 4 33 syl5bb ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
35 34 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
36 ralcom ⊢ ( ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
37 35 36 bitrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
38 37 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
39 ralcom ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
40 38 39 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) ) )