Metamath Proof Explorer


Theorem cnneiima

Description: Given a continuous function, the preimage of a neighborhood is a neighborhood. To be precise, the preimage of a neighborhood of a subset T of the codomain of a continuous function is a neighborhood of any subset of the preimage of T . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Hypotheses cnneiima.1 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
cnneiima.2 ( 𝜑𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) )
cnneiima.3 ( 𝜑𝑆 ⊆ ( 𝐹𝑇 ) )
Assertion cnneiima ( 𝜑 → ( 𝐹𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cnneiima.1 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2 cnneiima.2 ( 𝜑𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) )
3 cnneiima.3 ( 𝜑𝑆 ⊆ ( 𝐹𝑇 ) )
4 eqid 𝐽 = 𝐽
5 eqid 𝐾 = 𝐾
6 4 5 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝐽 𝐾 )
7 1 6 syl ( 𝜑𝐹 : 𝐽 𝐾 )
8 7 ffund ( 𝜑 → Fun 𝐹 )
9 cntop2 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
10 1 9 syl ( 𝜑𝐾 ∈ Top )
11 5 neiss2 ( ( 𝐾 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) ) → 𝑇 𝐾 )
12 10 2 11 syl2anc ( 𝜑𝑇 𝐾 )
13 5 neii1 ( ( 𝐾 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) ) → 𝑁 𝐾 )
14 10 2 13 syl2anc ( 𝜑𝑁 𝐾 )
15 5 neiint ( ( 𝐾 ∈ Top ∧ 𝑇 𝐾𝑁 𝐾 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) ↔ 𝑇 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) )
16 10 12 14 15 syl3anc ( 𝜑 → ( 𝑁 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑇 ) ↔ 𝑇 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) )
17 2 16 mpbid ( 𝜑𝑇 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) )
18 sspreima ( ( Fun 𝐹𝑇 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) → ( 𝐹𝑇 ) ⊆ ( 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) )
19 8 17 18 syl2anc ( 𝜑 → ( 𝐹𝑇 ) ⊆ ( 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) )
20 3 19 sstrd ( 𝜑𝑆 ⊆ ( 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) )
21 5 cnntri ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑁 𝐾 ) → ( 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐹𝑁 ) ) )
22 1 14 21 syl2anc ( 𝜑 → ( 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑁 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐹𝑁 ) ) )
23 20 22 sstrd ( 𝜑𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐹𝑁 ) ) )
24 cntop1 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
25 1 24 syl ( 𝜑𝐽 ∈ Top )
26 sspreima ( ( Fun 𝐹𝑇 𝐾 ) → ( 𝐹𝑇 ) ⊆ ( 𝐹 𝐾 ) )
27 8 12 26 syl2anc ( 𝜑 → ( 𝐹𝑇 ) ⊆ ( 𝐹 𝐾 ) )
28 fimacnv ( 𝐹 : 𝐽 𝐾 → ( 𝐹 𝐾 ) = 𝐽 )
29 7 28 syl ( 𝜑 → ( 𝐹 𝐾 ) = 𝐽 )
30 27 29 sseqtrd ( 𝜑 → ( 𝐹𝑇 ) ⊆ 𝐽 )
31 3 30 sstrd ( 𝜑𝑆 𝐽 )
32 sspreima ( ( Fun 𝐹𝑁 𝐾 ) → ( 𝐹𝑁 ) ⊆ ( 𝐹 𝐾 ) )
33 8 14 32 syl2anc ( 𝜑 → ( 𝐹𝑁 ) ⊆ ( 𝐹 𝐾 ) )
34 33 29 sseqtrd ( 𝜑 → ( 𝐹𝑁 ) ⊆ 𝐽 )
35 4 neiint ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ∧ ( 𝐹𝑁 ) ⊆ 𝐽 ) → ( ( 𝐹𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐹𝑁 ) ) ) )
36 25 31 34 35 syl3anc ( 𝜑 → ( ( 𝐹𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐹𝑁 ) ) ) )
37 23 36 mpbird ( 𝜑 → ( 𝐹𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )