fmcfil

Description: The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Assertion	fmcfil	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ((X FilMap F) (B) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists y \in B \forall z \in y \forall w \in y F (z) D F (w) < x)$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
2		fmval	$⊢ (X \in dom ∞Met \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = X filGen ran (y \in B ⟼ F [y])$
3	1 2	syl3an1	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = X filGen ran (y \in B ⟼ F [y])$
4	3	eleq1d	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ((X FilMap F) (B) \in CauFil (D) \leftrightarrow X filGen ran (y \in B ⟼ F [y]) \in CauFil (D))$
5		simp1	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to D \in ∞Met (X)$
6		simp2	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to B \in fBas (Y)$
7		simp3	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to F : Y ⟶ X$
8	1	3ad2ant1	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to X \in dom ∞Met$
9		eqid	$⊢ ran (y \in B ⟼ F [y]) = ran (y \in B ⟼ F [y])$
10	9	fbasrn	$⊢ (B \in fBas (Y) \land F : Y ⟶ X \land X \in dom ∞Met) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
11	6 7 8 10	syl3anc	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
12		fgcfil	$⊢ (D \in ∞Met (X) \land ran (y \in B ⟼ F [y]) \in fBas (X)) \to (X filGen ran (y \in B ⟼ F [y]) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x)$
13	5 11 12	syl2anc	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (X filGen ran (y \in B ⟼ F [y]) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x)$
14		imassrn	$⊢ F [y] \subseteq ran F$
15		frn	$⊢ F : Y ⟶ X \to ran F \subseteq X$
16	15	3ad2ant3	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ran F \subseteq X$
17	14 16	sstrid	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to F [y] \subseteq X$
18	8 17	ssexd	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to F [y] \in V$
19	18	ralrimivw	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to \forall y \in B F [y] \in V$
20		eqid	$⊢ (y \in B ⟼ F [y]) = (y \in B ⟼ F [y])$
21		raleq	$⊢ s = F [y] \to (\forall v \in s u D v < x \leftrightarrow \forall v \in F [y] u D v < x)$
22	21	raleqbi1dv	$⊢ s = F [y] \to (\forall u \in s \forall v \in s u D v < x \leftrightarrow \forall u \in F [y] \forall v \in F [y] u D v < x)$
23	20 22	rexrnmptw	$⊢ \forall y \in B F [y] \in V \to (\exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x \leftrightarrow \exists y \in B \forall u \in F [y] \forall v \in F [y] u D v < x)$
24	19 23	syl	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x \leftrightarrow \exists y \in B \forall u \in F [y] \forall v \in F [y] u D v < x)$
25		simpl3	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to F : Y ⟶ X$
26	25	ffnd	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to F Fn Y$
27		fbelss	$⊢ (B \in fBas (Y) \land y \in B) \to y \subseteq Y$
28	6 27	sylan	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to y \subseteq Y$
29		oveq1	$⊢ u = F (z) \to u D v = F (z) D v$
30	29	breq1d	$⊢ u = F (z) \to (u D v < x \leftrightarrow F (z) D v < x)$
31	30	ralbidv	$⊢ u = F (z) \to (\forall v \in F [y] u D v < x \leftrightarrow \forall v \in F [y] F (z) D v < x)$
32	31	ralima	$⊢ (F Fn Y \land y \subseteq Y) \to (\forall u \in F [y] \forall v \in F [y] u D v < x \leftrightarrow \forall z \in y \forall v \in F [y] F (z) D v < x)$
33	26 28 32	syl2anc	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to (\forall u \in F [y] \forall v \in F [y] u D v < x \leftrightarrow \forall z \in y \forall v \in F [y] F (z) D v < x)$
34		oveq2	$⊢ v = F (w) \to F (z) D v = F (z) D F (w)$
35	34	breq1d	$⊢ v = F (w) \to (F (z) D v < x \leftrightarrow F (z) D F (w) < x)$
36	35	ralima	$⊢ (F Fn Y \land y \subseteq Y) \to (\forall v \in F [y] F (z) D v < x \leftrightarrow \forall w \in y F (z) D F (w) < x)$
37	26 28 36	syl2anc	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to (\forall v \in F [y] F (z) D v < x \leftrightarrow \forall w \in y F (z) D F (w) < x)$
38	37	ralbidv	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to (\forall z \in y \forall v \in F [y] F (z) D v < x \leftrightarrow \forall z \in y \forall w \in y F (z) D F (w) < x)$
39	33 38	bitrd	$⊢ ((D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \land y \in B) \to (\forall u \in F [y] \forall v \in F [y] u D v < x \leftrightarrow \forall z \in y \forall w \in y F (z) D F (w) < x)$
40	39	rexbidva	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists y \in B \forall u \in F [y] \forall v \in F [y] u D v < x \leftrightarrow \exists y \in B \forall z \in y \forall w \in y F (z) D F (w) < x)$
41	24 40	bitrd	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (\exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x \leftrightarrow \exists y \in B \forall z \in y \forall w \in y F (z) D F (w) < x)$
42	41	ralbidv	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to (\forall x \in ℝ^{+} \exists s \in ran (y \in B ⟼ F [y]) \forall u \in s \forall v \in s u D v < x \leftrightarrow \forall x \in ℝ^{+} \exists y \in B \forall z \in y \forall w \in y F (z) D F (w) < x)$
43	4 13 42	3bitrd	$⊢ (D \in ∞Met (X) \land B \in fBas (Y) \land F : Y ⟶ X) \to ((X FilMap F) (B) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists y \in B \forall z \in y \forall w \in y F (z) D F (w) < x)$

Metamath Proof Explorer

Theorem fmcfil

Proof