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∈JCnK
cnneiima.2 ⊢φ→N∈nei⁡K⁡T
cnneiima.3 ⊢φ→S⊆F-1T
Assertion cnneiima ⊢φ→F-1N∈nei⁡J⁡S

Proof

Step Hyp Ref Expression
1 cnneiima.1 ⊢φ→F∈JCnK
2 cnneiima.2 ⊢φ→N∈nei⁡K⁡T
3 cnneiima.3 ⊢φ→S⊆F-1T
4 eqid ⊢⋃J=⋃J
5 eqid ⊢⋃K=⋃K
6 4 5 cnf ⊢F∈JCnK→F:⋃J⟶⋃K
7 1 6 syl ⊢φ→F:⋃J⟶⋃K
8 7 ffund ⊢φ→Fun⁡F
9 cntop2 ⊢F∈JCnK→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-1T⊆F-1int⁡K⁡N
19 8 17 18 syl2anc ⊢φ→F-1T⊆F-1int⁡K⁡N
20 3 19 sstrd ⊢φ→S⊆F-1int⁡K⁡N
21 5 cnntri ⊢F∈JCnK∧N⊆⋃K→F-1int⁡K⁡N⊆int⁡J⁡F-1N
22 1 14 21 syl2anc ⊢φ→F-1int⁡K⁡N⊆int⁡J⁡F-1N
23 20 22 sstrd ⊢φ→S⊆int⁡J⁡F-1N
24 cntop1 ⊢F∈JCnK→J∈Top
25 1 24 syl ⊢φ→J∈Top
26 sspreima ⊢Fun⁡F∧T⊆⋃K→F-1T⊆F-1⋃K
27 8 12 26 syl2anc ⊢φ→F-1T⊆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-1T⊆⋃J
31 3 30 sstrd ⊢φ→S⊆⋃J
32 sspreima ⊢Fun⁡F∧N⊆⋃K→F-1N⊆F-1⋃K
33 8 14 32 syl2anc ⊢φ→F-1N⊆F-1⋃K
34 33 29 sseqtrd ⊢φ→F-1N⊆⋃J
35 4 neiint ⊢J∈Top∧S⊆⋃J∧F-1N⊆⋃J→F-1N∈nei⁡J⁡S↔S⊆int⁡J⁡F-1N
36 25 31 34 35 syl3anc ⊢φ→F-1N∈nei⁡J⁡S↔S⊆int⁡J⁡F-1N
37 23 36 mpbird ⊢φ→F-1N∈nei⁡J⁡S