neipcfilu

Description: In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018)

	Ref	Expression
Hypotheses	neipcfilu.x	$⊢ X = {Base}_{W}$
	neipcfilu.j	$⊢ J = TopOpen (W)$
	neipcfilu.u	$⊢ U = UnifSt (W)$
Assertion	neipcfilu	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in CauFilU (U)$

Proof

Step	Hyp	Ref	Expression
1		neipcfilu.x	$⊢ X = {Base}_{W}$
2		neipcfilu.j	$⊢ J = TopOpen (W)$
3		neipcfilu.u	$⊢ U = UnifSt (W)$
4		simp2	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to W \in TopSp$
5	1 2	istps	$⊢ W \in TopSp \leftrightarrow J \in TopOn (X)$
6	4 5	sylib	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to J \in TopOn (X)$
7		simp3	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to P \in X$
8	7	snssd	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to \{P\} \subseteq X$
9	7	snn0d	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to \{P\} \neq \emptyset$
10		neifil	$⊢ (J \in TopOn (X) \land \{P\} \subseteq X \land \{P\} \neq \emptyset) \to nei (J) (\{P\}) \in Fil (X)$
11	6 8 9 10	syl3anc	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in Fil (X)$
12		filfbas	$⊢ nei (J) (\{P\}) \in Fil (X) \to nei (J) (\{P\}) \in fBas (X)$
13	11 12	syl	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in fBas (X)$
14		eqid	$⊢ w [\{P\}] = w [\{P\}]$
15		imaeq1	$⊢ v = w \to v [\{P\}] = w [\{P\}]$
16	15	rspceeqv	$⊢ (w \in U \land w [\{P\}] = w [\{P\}]) \to \exists v \in U w [\{P\}] = v [\{P\}]$
17	14 16	mpan2	$⊢ w \in U \to \exists v \in U w [\{P\}] = v [\{P\}]$
18		vex	$⊢ w \in V$
19	18	imaex	$⊢ w [\{P\}] \in V$
20		eqid	$⊢ (v \in U ⟼ v [\{P\}]) = (v \in U ⟼ v [\{P\}])$
21	20	elrnmpt	$⊢ w [\{P\}] \in V \to (w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]) \leftrightarrow \exists v \in U w [\{P\}] = v [\{P\}])$
22	19 21	ax-mp	$⊢ w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]) \leftrightarrow \exists v \in U w [\{P\}] = v [\{P\}]$
23	17 22	sylibr	$⊢ w \in U \to w [\{P\}] \in ran (v \in U ⟼ v [\{P\}])$
24	23	ad2antlr	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to w [\{P\}] \in ran (v \in U ⟼ v [\{P\}])$
25	1 3 2	isusp	$⊢ W \in UnifSp \leftrightarrow (U \in UnifOn (X) \land J = unifTop (U))$
26	25	simplbi	$⊢ W \in UnifSp \to U \in UnifOn (X)$
27	26	3ad2ant1	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to U \in UnifOn (X)$
28		eqid	$⊢ unifTop (U) = unifTop (U)$
29	28	utopsnneip	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (unifTop (U)) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$
30	27 7 29	syl2anc	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (unifTop (U)) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$
31	30	eleq2d	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to (w [\{P\}] \in nei (unifTop (U)) (\{P\}) \leftrightarrow w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]))$
32	31	ad3antrrr	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to (w [\{P\}] \in nei (unifTop (U)) (\{P\}) \leftrightarrow w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]))$
33	24 32	mpbird	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to w [\{P\}] \in nei (unifTop (U)) (\{P\})$
34		simpl1	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land (v \in U \land w \in U \land w [\{P\}] \times w [\{P\}] \subseteq v)) \to W \in UnifSp$
35	34	3anassrs	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to W \in UnifSp$
36	25	simprbi	$⊢ W \in UnifSp \to J = unifTop (U)$
37	35 36	syl	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to J = unifTop (U)$
38	37	fveq2d	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to nei (J) = nei (unifTop (U))$
39	38	fveq1d	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to nei (J) (\{P\}) = nei (unifTop (U)) (\{P\})$
40	33 39	eleqtrrd	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to w [\{P\}] \in nei (J) (\{P\})$
41		simpr	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to w [\{P\}] \times w [\{P\}] \subseteq v$
42		id	$⊢ a = w [\{P\}] \to a = w [\{P\}]$
43	42	sqxpeqd	$⊢ a = w [\{P\}] \to a \times a = w [\{P\}] \times w [\{P\}]$
44	43	sseq1d	$⊢ a = w [\{P\}] \to (a \times a \subseteq v \leftrightarrow w [\{P\}] \times w [\{P\}] \subseteq v)$
45	44	rspcev	$⊢ (w [\{P\}] \in nei (J) (\{P\}) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to \exists a \in nei (J) (\{P\}) a \times a \subseteq v$
46	40 41 45	syl2anc	$⊢ ((((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \land w \in U) \land w [\{P\}] \times w [\{P\}] \subseteq v) \to \exists a \in nei (J) (\{P\}) a \times a \subseteq v$
47	27	adantr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to U \in UnifOn (X)$
48	7	adantr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to P \in X$
49		simpr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to v \in U$
50		simpll1	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \to U \in UnifOn (X)$
51		simplr	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \to u \in U$
52		ustexsym	$⊢ (U \in UnifOn (X) \land u \in U) \to \exists w \in U (w^{-1} = w \land w \subseteq u)$
53	50 51 52	syl2anc	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \to \exists w \in U (w^{-1} = w \land w \subseteq u)$
54	50	ad2antrr	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to U \in UnifOn (X)$
55		simplr	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \in U$
56		ustssxp	$⊢ (U \in UnifOn (X) \land w \in U) \to w \subseteq X \times X$
57	54 55 56	syl2anc	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \subseteq X \times X$
58		simpll2	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land (u \circ u \subseteq v \land w \in U \land (w^{-1} = w \land w \subseteq u))) \to P \in X$
59	58	3anassrs	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to P \in X$
60		ustneism	$⊢ (w \subseteq X \times X \land P \in X) \to w [\{P\}] \times w [\{P\}] \subseteq w \circ w^{-1}$
61	57 59 60	syl2anc	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w [\{P\}] \times w [\{P\}] \subseteq w \circ w^{-1}$
62		simprl	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w^{-1} = w$
63	62	coeq2d	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \circ w^{-1} = w \circ w$
64		coss1	$⊢ w \subseteq u \to w \circ w \subseteq u \circ w$
65		coss2	$⊢ w \subseteq u \to u \circ w \subseteq u \circ u$
66	64 65	sstrd	$⊢ w \subseteq u \to w \circ w \subseteq u \circ u$
67	66	ad2antll	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \circ w \subseteq u \circ u$
68		simpllr	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to u \circ u \subseteq v$
69	67 68	sstrd	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \circ w \subseteq v$
70	63 69	eqsstrd	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w \circ w^{-1} \subseteq v$
71	61 70	sstrd	$⊢ (((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \land (w^{-1} = w \land w \subseteq u)) \to w [\{P\}] \times w [\{P\}] \subseteq v$
72	71	ex	$⊢ ((((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \land w \in U) \to ((w^{-1} = w \land w \subseteq u) \to w [\{P\}] \times w [\{P\}] \subseteq v)$
73	72	reximdva	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \to (\exists w \in U (w^{-1} = w \land w \subseteq u) \to \exists w \in U w [\{P\}] \times w [\{P\}] \subseteq v)$
74	53 73	mpd	$⊢ (((U \in UnifOn (X) \land P \in X \land v \in U) \land u \in U) \land u \circ u \subseteq v) \to \exists w \in U w [\{P\}] \times w [\{P\}] \subseteq v$
75		ustexhalf	$⊢ (U \in UnifOn (X) \land v \in U) \to \exists u \in U u \circ u \subseteq v$
76	75	3adant2	$⊢ (U \in UnifOn (X) \land P \in X \land v \in U) \to \exists u \in U u \circ u \subseteq v$
77	74 76	r19.29a	$⊢ (U \in UnifOn (X) \land P \in X \land v \in U) \to \exists w \in U w [\{P\}] \times w [\{P\}] \subseteq v$
78	47 48 49 77	syl3anc	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to \exists w \in U w [\{P\}] \times w [\{P\}] \subseteq v$
79	46 78	r19.29a	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to \exists a \in nei (J) (\{P\}) a \times a \subseteq v$
80	79	ralrimiva	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to \forall v \in U \exists a \in nei (J) (\{P\}) a \times a \subseteq v$
81		iscfilu	$⊢ U \in UnifOn (X) \to (nei (J) (\{P\}) \in CauFilU (U) \leftrightarrow (nei (J) (\{P\}) \in fBas (X) \land \forall v \in U \exists a \in nei (J) (\{P\}) a \times a \subseteq v))$
82	27 81	syl	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to (nei (J) (\{P\}) \in CauFilU (U) \leftrightarrow (nei (J) (\{P\}) \in fBas (X) \land \forall v \in U \exists a \in nei (J) (\{P\}) a \times a \subseteq v))$
83	13 80 82	mpbir2and	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in CauFilU (U)$

Metamath Proof Explorer

Theorem neipcfilu

Proof