fmcncfil

Description: The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017)

	Ref	Expression
Hypotheses	fmcncfil.1	$⊢ J = MetOpen (D)$
	fmcncfil.2	$⊢ K = MetOpen (E)$
Assertion	fmcncfil	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (Y FilMap F) (B) \in CauFil (E)$

Proof

Step	Hyp	Ref	Expression
1		fmcncfil.1	$⊢ J = MetOpen (D)$
2		fmcncfil.2	$⊢ K = MetOpen (E)$
3		simpl2	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to E \in ∞Met (Y)$
4		simpl1	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to D \in CMet (X)$
5	1	cmetcvg	$⊢ (D \in CMet (X) \land B \in CauFil (D)) \to J fLim B \neq \emptyset$
6		n0	$⊢ J fLim B \neq \emptyset \leftrightarrow \exists x x \in (J fLim B)$
7	5 6	sylib	$⊢ (D \in CMet (X) \land B \in CauFil (D)) \to \exists x x \in (J fLim B)$
8	4 7	sylancom	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \exists x x \in (J fLim B)$
9		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
10		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
11	4 9 10	3syl	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to D \in ∞Met (X)$
12		cfilfil	$⊢ (D \in ∞Met (X) \land B \in CauFil (D)) \to B \in Fil (X)$
13	11 12	sylancom	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to B \in Fil (X)$
14	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
15	11 14	syl	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to J \in TopOn (X)$
16	2	mopntopon	$⊢ E \in ∞Met (Y) \to K \in TopOn (Y)$
17	3 16	syl	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to K \in TopOn (Y)$
18		simpl3	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to F \in (J Cn K)$
19		cnflf	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall b \in Fil (X) \forall x \in (J fLim b) F (x) \in (K fLimf b) (F)))$
20	19	simplbda	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J Cn K)) \to \forall b \in Fil (X) \forall x \in (J fLim b) F (x) \in (K fLimf b) (F)$
21	15 17 18 20	syl21anc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \forall b \in Fil (X) \forall x \in (J fLim b) F (x) \in (K fLimf b) (F)$
22		oveq2	$⊢ b = B \to J fLim b = J fLim B$
23		oveq2	$⊢ b = B \to K fLimf b = K fLimf B$
24	23	fveq1d	$⊢ b = B \to (K fLimf b) (F) = (K fLimf B) (F)$
25	24	eleq2d	$⊢ b = B \to (F (x) \in (K fLimf b) (F) \leftrightarrow F (x) \in (K fLimf B) (F))$
26	22 25	raleqbidv	$⊢ b = B \to (\forall x \in (J fLim b) F (x) \in (K fLimf b) (F) \leftrightarrow \forall x \in (J fLim B) F (x) \in (K fLimf B) (F))$
27	26	rspcv	$⊢ B \in Fil (X) \to (\forall b \in Fil (X) \forall x \in (J fLim b) F (x) \in (K fLimf b) (F) \to \forall x \in (J fLim B) F (x) \in (K fLimf B) (F))$
28	13 21 27	sylc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \forall x \in (J fLim B) F (x) \in (K fLimf B) (F)$
29		df-ral	$⊢ \forall x \in (J fLim B) F (x) \in (K fLimf B) (F) \leftrightarrow \forall x (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))$
30	28 29	sylib	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \forall x (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))$
31		19.29r	$⊢ (\exists x x \in (J fLim B) \land \forall x (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))) \to \exists x (x \in (J fLim B) \land (x \in (J fLim B) \to F (x) \in (K fLimf B) (F)))$
32		pm3.35	$⊢ (x \in (J fLim B) \land (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))) \to F (x) \in (K fLimf B) (F)$
33	32	eximi	$⊢ \exists x (x \in (J fLim B) \land (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))) \to \exists x F (x) \in (K fLimf B) (F)$
34	31 33	syl	$⊢ (\exists x x \in (J fLim B) \land \forall x (x \in (J fLim B) \to F (x) \in (K fLimf B) (F))) \to \exists x F (x) \in (K fLimf B) (F)$
35	8 30 34	syl2anc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \exists x F (x) \in (K fLimf B) (F)$
36	1 2	metcn	$⊢ (D \in ∞Met (X) \land E \in ∞Met (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in X \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in X (x D y < d \to F (x) E F (y) < e)))$
37	36	biimpa	$⊢ ((D \in ∞Met (X) \land E \in ∞Met (Y)) \land F \in (J Cn K)) \to (F : X ⟶ Y \land \forall x \in X \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in X (x D y < d \to F (x) E F (y) < e))$
38	11 3 18 37	syl21anc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (F : X ⟶ Y \land \forall x \in X \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in X (x D y < d \to F (x) E F (y) < e))$
39	38	simpld	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to F : X ⟶ Y$
40		flfval	$⊢ (K \in TopOn (Y) \land B \in Fil (X) \land F : X ⟶ Y) \to (K fLimf B) (F) = K fLim (Y FilMap F) (B)$
41	17 13 39 40	syl3anc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (K fLimf B) (F) = K fLim (Y FilMap F) (B)$
42	41	eleq2d	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (F (x) \in (K fLimf B) (F) \leftrightarrow F (x) \in (K fLim (Y FilMap F) (B)))$
43	42	exbidv	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (\exists x F (x) \in (K fLimf B) (F) \leftrightarrow \exists x F (x) \in (K fLim (Y FilMap F) (B)))$
44	35 43	mpbid	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to \exists x F (x) \in (K fLim (Y FilMap F) (B))$
45	2	flimcfil	$⊢ (E \in ∞Met (Y) \land F (x) \in (K fLim (Y FilMap F) (B))) \to (Y FilMap F) (B) \in CauFil (E)$
46	45	ex	$⊢ E \in ∞Met (Y) \to (F (x) \in (K fLim (Y FilMap F) (B)) \to (Y FilMap F) (B) \in CauFil (E))$
47	46	exlimdv	$⊢ E \in ∞Met (Y) \to (\exists x F (x) \in (K fLim (Y FilMap F) (B)) \to (Y FilMap F) (B) \in CauFil (E))$
48	3 44 47	sylc	$⊢ ((D \in CMet (X) \land E \in ∞Met (Y) \land F \in (J Cn K)) \land B \in CauFil (D)) \to (Y FilMap F) (B) \in CauFil (E)$

Metamath Proof Explorer

Theorem fmcncfil

Proof