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	$⊢ φ \to F \in (J Cn K)$
	cnneiima.2	$⊢ φ \to N \in nei (K) (T)$
	cnneiima.3	$⊢ φ \to S \subseteq F^{-1} [T]$
Assertion	cnneiima	$⊢ φ \to F^{-1} [N] \in nei (J) (S)$

Proof

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

Metamath Proof Explorer

Theorem cnneiima

Proof