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 ‘ 𝐽 ) ‘ 𝑆 ) )