cfilres

Description: Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	cfilres	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F \in CauFil (D) \leftrightarrow F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}))$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to F \in Fil (X)$
2		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
3	1 2	syl	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to F \in fBas (X)$
4		simp3	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to Y \in F$
5		fbncp	$⊢ (F \in fBas (X) \land Y \in F) \to \neg X ∖ Y \in F$
6	3 4 5	syl2anc	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to \neg X ∖ Y \in F$
7		filelss	$⊢ (F \in Fil (X) \land Y \in F) \to Y \subseteq X$
8	7	3adant1	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to Y \subseteq X$
9		trfil3	$⊢ (F \in Fil (X) \land Y \subseteq X) \to (F ↾_{𝑡} Y \in Fil (Y) \leftrightarrow \neg X ∖ Y \in F)$
10	1 8 9	syl2anc	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F ↾_{𝑡} Y \in Fil (Y) \leftrightarrow \neg X ∖ Y \in F)$
11	6 10	mpbird	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to F ↾_{𝑡} Y \in Fil (Y)$
12	11	adantr	$⊢ ((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \to F ↾_{𝑡} Y \in Fil (Y)$
13		cfili	$⊢ (F \in CauFil (D) \land x \in ℝ^{+}) \to \exists s \in F \forall u \in s \forall v \in s u D v < x$
14	13	adantll	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to \exists s \in F \forall u \in s \forall v \in s u D v < x$
15		simpll2	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to F \in Fil (X)$
16		simpll3	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to Y \in F$
17	15 16	jca	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to (F \in Fil (X) \land Y \in F)$
18		elrestr	$⊢ (F \in Fil (X) \land Y \in F \land s \in F) \to s \cap Y \in (F ↾_{𝑡} Y)$
19	18	3expa	$⊢ ((F \in Fil (X) \land Y \in F) \land s \in F) \to s \cap Y \in (F ↾_{𝑡} Y)$
20	17 19	sylan	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \land s \in F) \to s \cap Y \in (F ↾_{𝑡} Y)$
21		inss1	$⊢ s \cap Y \subseteq s$
22		ss2ralv	$⊢ s \cap Y \subseteq s \to (\forall u \in s \forall v \in s u D v < x \to \forall u \in (s \cap Y) \forall v \in (s \cap Y) u D v < x)$
23	21 22	ax-mp	$⊢ \forall u \in s \forall v \in s u D v < x \to \forall u \in (s \cap Y) \forall v \in (s \cap Y) u D v < x$
24		elinel2	$⊢ u \in (s \cap Y) \to u \in Y$
25		elinel2	$⊢ v \in (s \cap Y) \to v \in Y$
26		ovres	$⊢ (u \in Y \land v \in Y) \to u ({D ↾}_{(Y \times Y)}) v = u D v$
27	26	breq1d	$⊢ (u \in Y \land v \in Y) \to (u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow u D v < x)$
28	24 25 27	syl2an	$⊢ (u \in (s \cap Y) \land v \in (s \cap Y)) \to (u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow u D v < x)$
29	28	ralbidva	$⊢ u \in (s \cap Y) \to (\forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall v \in (s \cap Y) u D v < x)$
30	29	ralbiia	$⊢ \forall u \in (s \cap Y) \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall u \in (s \cap Y) \forall v \in (s \cap Y) u D v < x$
31	23 30	sylibr	$⊢ \forall u \in s \forall v \in s u D v < x \to \forall u \in (s \cap Y) \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x$
32		raleq	$⊢ y = s \cap Y \to (\forall v \in y u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x)$
33	32	raleqbi1dv	$⊢ y = s \cap Y \to (\forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x \leftrightarrow \forall u \in (s \cap Y) \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x)$
34	33	rspcev	$⊢ (s \cap Y \in (F ↾_{𝑡} Y) \land \forall u \in (s \cap Y) \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x) \to \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x$
35	34	ex	$⊢ s \cap Y \in (F ↾_{𝑡} Y) \to (\forall u \in (s \cap Y) \forall v \in (s \cap Y) u ({D ↾}_{(Y \times Y)}) v < x \to \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x)$
36	20 31 35	syl2im	$⊢ ((((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \land s \in F) \to (\forall u \in s \forall v \in s u D v < x \to \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x)$
37	36	rexlimdva	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to (\exists s \in F \forall u \in s \forall v \in s u D v < x \to \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x)$
38	14 37	mpd	$⊢ (((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \land x \in ℝ^{+}) \to \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x$
39	38	ralrimiva	$⊢ ((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \to \forall x \in ℝ^{+} \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x$
40		simp1	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to D \in ∞Met (X)$
41		xmetres2	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
42	40 8 41	syl2anc	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
43	42	adantr	$⊢ ((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
44		iscfil2	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (Y) \to (F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}) \leftrightarrow (F ↾_{𝑡} Y \in Fil (Y) \land \forall x \in ℝ^{+} \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x))$
45	43 44	syl	$⊢ ((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \to (F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}) \leftrightarrow (F ↾_{𝑡} Y \in Fil (Y) \land \forall x \in ℝ^{+} \exists y \in (F ↾_{𝑡} Y) \forall u \in y \forall v \in y u ({D ↾}_{(Y \times Y)}) v < x))$
46	12 39 45	mpbir2and	$⊢ ((D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \land F \in CauFil (D)) \to F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)})$
47	46	ex	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F \in CauFil (D) \to F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}))$
48		cfilresi	$⊢ (D \in ∞Met (X) \land F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen (F ↾_{𝑡} Y) \in CauFil (D)$
49	48	ex	$⊢ D \in ∞Met (X) \to (F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}) \to X filGen (F ↾_{𝑡} Y) \in CauFil (D))$
50	49	3ad2ant1	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}) \to X filGen (F ↾_{𝑡} Y) \in CauFil (D))$
51		fgtr	$⊢ (F \in Fil (X) \land Y \in F) \to X filGen (F ↾_{𝑡} Y) = F$
52	51	3adant1	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to X filGen (F ↾_{𝑡} Y) = F$
53	52	eleq1d	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (X filGen (F ↾_{𝑡} Y) \in CauFil (D) \leftrightarrow F \in CauFil (D))$
54	50 53	sylibd	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}) \to F \in CauFil (D))$
55	47 54	impbid	$⊢ (D \in ∞Met (X) \land F \in Fil (X) \land Y \in F) \to (F \in CauFil (D) \leftrightarrow F ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}))$

Metamath Proof Explorer

Theorem cfilres

Proof