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 φ F J Cn K
cnneiima.2 φ N nei K T
cnneiima.3 φ S F -1 T
Assertion cnneiima φ F -1 N nei J S

Proof

Step Hyp Ref Expression
1 cnneiima.1 φ F J Cn K
2 cnneiima.2 φ N nei K T
3 cnneiima.3 φ S F -1 T
4 eqid J = J
5 eqid K = K
6 4 5 cnf F J Cn K F : J K
7 1 6 syl φ F : J K
8 7 ffund φ Fun F
9 cntop2 F J Cn K K Top
10 1 9 syl φ K Top
11 5 neiss2 K Top N nei K T T K
12 10 2 11 syl2anc φ T K
13 5 neii1 K Top N nei K T N K
14 10 2 13 syl2anc φ N K
15 5 neiint K Top T K N K N nei K T T int K N
16 10 12 14 15 syl3anc φ N nei K T T int K N
17 2 16 mpbid φ T int K N
18 sspreima Fun F T int K N F -1 T F -1 int K N
19 8 17 18 syl2anc φ F -1 T F -1 int K N
20 3 19 sstrd φ S F -1 int K N
21 5 cnntri F J Cn K N K F -1 int K N int J F -1 N
22 1 14 21 syl2anc φ F -1 int K N int J F -1 N
23 20 22 sstrd φ S int J F -1 N
24 cntop1 F J Cn K J Top
25 1 24 syl φ J Top
26 sspreima Fun F T K F -1 T F -1 K
27 8 12 26 syl2anc φ F -1 T F -1 K
28 fimacnv F : J K F -1 K = J
29 7 28 syl φ F -1 K = J
30 27 29 sseqtrd φ F -1 T J
31 3 30 sstrd φ S J
32 sspreima Fun F N K F -1 N F -1 K
33 8 14 32 syl2anc φ F -1 N F -1 K
34 33 29 sseqtrd φ F -1 N J
35 4 neiint J Top S J F -1 N J F -1 N nei J S S int J F -1 N
36 25 31 34 35 syl3anc φ F -1 N nei J S S int J F -1 N
37 23 36 mpbird φ F -1 N nei J S