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	|- ( ph -> F e. ( J Cn K ) )
	cnneiima.2	|- ( ph -> N e. ( ( nei ` K ) ` T ) )
	cnneiima.3	|- ( ph -> S C_ ( `' F " T ) )
Assertion	cnneiima	|- ( ph -> ( `' F " N ) e. ( ( nei ` J ) ` S ) )

Proof

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