flfcntr

Description: A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020)

	Ref	Expression
Hypotheses	flfcntr.c	$⊢ C = ⋃ J$
	flfcntr.b	$⊢ B = ⋃ K$
	flfcntr.j	$⊢ φ \to J \in Top$
	flfcntr.a	$⊢ φ \to A \subseteq C$
	flfcntr.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
	flfcntr.y	$⊢ φ \to X \in A$
Assertion	flfcntr	$⊢ φ \to F (X) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$

Proof

Step	Hyp	Ref	Expression
1		flfcntr.c	$⊢ C = ⋃ J$
2		flfcntr.b	$⊢ B = ⋃ K$
3		flfcntr.j	$⊢ φ \to J \in Top$
4		flfcntr.a	$⊢ φ \to A \subseteq C$
5		flfcntr.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
6		flfcntr.y	$⊢ φ \to X \in A$
7		fveq2	$⊢ x = X \to F (x) = F (X)$
8	7	eleq1d	$⊢ x = X \to (F (x) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F) \leftrightarrow F (X) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F))$
9		oveq2	$⊢ a = nei (J) (\{X\}) ↾_{𝑡} A \to (J ↾_{𝑡} A) fLim a = (J ↾_{𝑡} A) fLim (nei (J) (\{X\}) ↾_{𝑡} A)$
10		oveq2	$⊢ a = nei (J) (\{X\}) ↾_{𝑡} A \to K fLimf a = K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)$
11	10	fveq1d	$⊢ a = nei (J) (\{X\}) ↾_{𝑡} A \to (K fLimf a) (F) = (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$
12	11	eleq2d	$⊢ a = nei (J) (\{X\}) ↾_{𝑡} A \to (F (x) \in (K fLimf a) (F) \leftrightarrow F (x) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F))$
13	9 12	raleqbidv	$⊢ a = nei (J) (\{X\}) ↾_{𝑡} A \to (\forall x \in ((J ↾_{𝑡} A) fLim a) F (x) \in (K fLimf a) (F) \leftrightarrow \forall x \in ((J ↾_{𝑡} A) fLim (nei (J) (\{X\}) ↾_{𝑡} A)) F (x) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F))$
14	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (C)$
15	3 14	sylib	$⊢ φ \to J \in TopOn (C)$
16		resttopon	$⊢ (J \in TopOn (C) \land A \subseteq C) \to J ↾_{𝑡} A \in TopOn (A)$
17	15 4 16	syl2anc	$⊢ φ \to J ↾_{𝑡} A \in TopOn (A)$
18		cntop2	$⊢ F \in ((J ↾_{𝑡} A) Cn K) \to K \in Top$
19	5 18	syl	$⊢ φ \to K \in Top$
20	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (B)$
21	19 20	sylib	$⊢ φ \to K \in TopOn (B)$
22		cnflf	$⊢ (J ↾_{𝑡} A \in TopOn (A) \land K \in TopOn (B)) \to (F \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow (F : A ⟶ B \land \forall a \in Fil (A) \forall x \in ((J ↾_{𝑡} A) fLim a) F (x) \in (K fLimf a) (F)))$
23	17 21 22	syl2anc	$⊢ φ \to (F \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow (F : A ⟶ B \land \forall a \in Fil (A) \forall x \in ((J ↾_{𝑡} A) fLim a) F (x) \in (K fLimf a) (F)))$
24	5 23	mpbid	$⊢ φ \to (F : A ⟶ B \land \forall a \in Fil (A) \forall x \in ((J ↾_{𝑡} A) fLim a) F (x) \in (K fLimf a) (F))$
25	24	simprd	$⊢ φ \to \forall a \in Fil (A) \forall x \in ((J ↾_{𝑡} A) fLim a) F (x) \in (K fLimf a) (F)$
26	1	sscls	$⊢ (J \in Top \land A \subseteq C) \to A \subseteq cls (J) (A)$
27	3 4 26	syl2anc	$⊢ φ \to A \subseteq cls (J) (A)$
28	27 6	sseldd	$⊢ φ \to X \in cls (J) (A)$
29	4 6	sseldd	$⊢ φ \to X \in C$
30		trnei	$⊢ (J \in TopOn (C) \land A \subseteq C \land X \in C) \to (X \in cls (J) (A) \leftrightarrow nei (J) (\{X\}) ↾_{𝑡} A \in Fil (A))$
31	15 4 29 30	syl3anc	$⊢ φ \to (X \in cls (J) (A) \leftrightarrow nei (J) (\{X\}) ↾_{𝑡} A \in Fil (A))$
32	28 31	mpbid	$⊢ φ \to nei (J) (\{X\}) ↾_{𝑡} A \in Fil (A)$
33	13 25 32	rspcdva	$⊢ φ \to \forall x \in ((J ↾_{𝑡} A) fLim (nei (J) (\{X\}) ↾_{𝑡} A)) F (x) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$
34		neiflim	$⊢ (J ↾_{𝑡} A \in TopOn (A) \land X \in A) \to X \in ((J ↾_{𝑡} A) fLim nei (J ↾_{𝑡} A) (\{X\}))$
35	17 6 34	syl2anc	$⊢ φ \to X \in ((J ↾_{𝑡} A) fLim nei (J ↾_{𝑡} A) (\{X\}))$
36	6	snssd	$⊢ φ \to \{X\} \subseteq A$
37	1	neitr	$⊢ (J \in Top \land A \subseteq C \land \{X\} \subseteq A) \to nei (J ↾_{𝑡} A) (\{X\}) = nei (J) (\{X\}) ↾_{𝑡} A$
38	3 4 36 37	syl3anc	$⊢ φ \to nei (J ↾_{𝑡} A) (\{X\}) = nei (J) (\{X\}) ↾_{𝑡} A$
39	38	oveq2d	$⊢ φ \to (J ↾_{𝑡} A) fLim nei (J ↾_{𝑡} A) (\{X\}) = (J ↾_{𝑡} A) fLim (nei (J) (\{X\}) ↾_{𝑡} A)$
40	35 39	eleqtrd	$⊢ φ \to X \in ((J ↾_{𝑡} A) fLim (nei (J) (\{X\}) ↾_{𝑡} A))$
41	8 33 40	rspcdva	$⊢ φ \to F (X) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$

Metamath Proof Explorer

Theorem flfcntr

Proof