cfilresi

Description: A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	cfilresi	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen F \in CauFil (D)$

Proof

Step	Hyp	Ref	Expression
1		xmetres	$⊢ D \in ∞Met (X) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
2		iscfil2	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \to (F \in CauFil ({D ↾}_{(Y \times Y)}) \leftrightarrow (F \in Fil (X \cap Y) \land \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x))$
3	2	simplbda	$⊢ ({D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x$
4	1 3	sylan	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x$
5		cfilfil	$⊢ ({D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \in Fil (X \cap Y)$
6	1 5	sylan	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \in Fil (X \cap Y)$
7		filelss	$⊢ (F \in Fil (X \cap Y) \land y \in F) \to y \subseteq X \cap Y$
8	6 7	sylan	$⊢ ((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \to y \subseteq X \cap Y$
9		inss2	$⊢ X \cap Y \subseteq Y$
10	8 9	sstrdi	$⊢ ((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \to y \subseteq Y$
11	10	sselda	$⊢ (((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \land u \in y) \to u \in Y$
12	10	sselda	$⊢ (((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \land v \in y) \to v \in Y$
13	11 12	anim12dan	$⊢ (((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \land (u \in y \land v \in y)) \to (u \in Y \land v \in Y)$
14		ovres	$⊢ (u \in Y \land v \in Y) \to u ({D ↾}_{(Y \times Y)}) v = u D v$
15	13 14	syl	$⊢ (((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \land (u \in y \land v \in y)) \to u ({D ↾}_{(Y \times Y)}) v = u D v$
16	15	breq1d	$⊢ (((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \land (u \in y \land v \in y)) \to (u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow u D v < x)$
17	16	2ralbidva	$⊢ ((D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \land y \in F) \to (\forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall u \in y \forall v \in y u D v < x)$
18	17	rexbidva	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to (\exists y \in F \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \exists y \in F \forall u \in y \forall v \in y u D v < x)$
19	18	ralbidv	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to (\forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < x)$
20	4 19	mpbid	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < x$
21		filfbas	$⊢ F \in Fil (X \cap Y) \to F \in fBas (X \cap Y)$
22	6 21	syl	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \in fBas (X \cap Y)$
23		filsspw	$⊢ F \in Fil (X \cap Y) \to F \subseteq 𝒫 (X \cap Y)$
24	6 23	syl	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \subseteq 𝒫 (X \cap Y)$
25		inss1	$⊢ X \cap Y \subseteq X$
26	25	sspwi	$⊢ 𝒫 (X \cap Y) \subseteq 𝒫 X$
27	24 26	sstrdi	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \subseteq 𝒫 X$
28		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
29	28	adantr	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to X \in dom ∞Met$
30		fbasweak	$⊢ (F \in fBas (X \cap Y) \land F \subseteq 𝒫 X \land X \in dom ∞Met) \to F \in fBas (X)$
31	22 27 29 30	syl3anc	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to F \in fBas (X)$
32		fgcfil	$⊢ (D \in ∞Met (X) \land F \in fBas (X)) \to (X filGen F \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < x)$
33	31 32	syldan	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to (X filGen F \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists y \in F \forall u \in y \forall v \in y u D v < x)$
34	20 33	mpbird	$⊢ (D \in ∞Met (X) \land F \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen F \in CauFil (D)$

Metamath Proof Explorer

Theorem cfilresi

Proof