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		snnzg	$⊢ P \in X \to \{P\} \neq \emptyset$
10	7 9	syl	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to \{P\} \neq \emptyset$
11		neifil	$⊢ (J \in TopOn (X) \land \{P\} \subseteq X \land \{P\} \neq \emptyset) \to nei (J) (\{P\}) \in Fil (X)$
12	6 8 10 11	syl3anc	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in Fil (X)$
13		filfbas	$⊢ nei (J) (\{P\}) \in Fil (X) \to nei (J) (\{P\}) \in fBas (X)$
14	12 13	syl	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (J) (\{P\}) \in fBas (X)$
15		eqid	$⊢ w [\{P\}] = w [\{P\}]$
16		imaeq1	$⊢ v = w \to v [\{P\}] = w [\{P\}]$
17	16	rspceeqv	$⊢ (w \in U \land w [\{P\}] = w [\{P\}]) \to \exists v \in U w [\{P\}] = v [\{P\}]$
18	15 17	mpan2	$⊢ w \in U \to \exists v \in U w [\{P\}] = v [\{P\}]$
19		vex	$⊢ w \in V$
20	19	imaex	$⊢ w [\{P\}] \in V$
21		eqid	$⊢ (v \in U ⟼ v [\{P\}]) = (v \in U ⟼ v [\{P\}])$
22	21	elrnmpt	$⊢ w [\{P\}] \in V \to (w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]) \leftrightarrow \exists v \in U w [\{P\}] = v [\{P\}])$
23	20 22	ax-mp	$⊢ w [\{P\}] \in ran (v \in U ⟼ v [\{P\}]) \leftrightarrow \exists v \in U w [\{P\}] = v [\{P\}]$
24	18 23	sylibr	$⊢ w \in U \to w [\{P\}] \in ran (v \in U ⟼ v [\{P\}])$
25	24	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\}])$
26	1 3 2	isusp	$⊢ W \in UnifSp \leftrightarrow (U \in UnifOn (X) \land J = unifTop (U))$
27	26	simplbi	$⊢ W \in UnifSp \to U \in UnifOn (X)$
28	27	3ad2ant1	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to U \in UnifOn (X)$
29		eqid	$⊢ unifTop (U) = unifTop (U)$
30	29	utopsnneip	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (unifTop (U)) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$
31	28 7 30	syl2anc	$⊢ (W \in UnifSp \land W \in TopSp \land P \in X) \to nei (unifTop (U)) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$
32	31	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\}]))$
33	32	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\}]))$
34	25 33	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\})$
35		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$
36	35	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$
37	26	simprbi	$⊢ W \in UnifSp \to J = unifTop (U)$
38	36 37	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)$
39	38	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))$
40	39	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\})$
41	34 40	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\})$
42		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$
43		id	$⊢ a = w [\{P\}] \to a = w [\{P\}]$
44	43	sqxpeqd	$⊢ a = w [\{P\}] \to a \times a = w [\{P\}] \times w [\{P\}]$
45	44	sseq1d	$⊢ a = w [\{P\}] \to (a \times a \subseteq v \leftrightarrow w [\{P\}] \times w [\{P\}] \subseteq v)$
46	45	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$
47	41 42 46	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$
48	28	adantr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to U \in UnifOn (X)$
49	7	adantr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to P \in X$
50		simpr	$⊢ ((W \in UnifSp \land W \in TopSp \land P \in X) \land v \in U) \to v \in U$
51		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)$
52		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$
53		ustexsym	$⊢ (U \in UnifOn (X) \land u \in U) \to \exists w \in U (w^{-1} = w \land w \subseteq u)$
54	51 52 53	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)$
55	51	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)$
56		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$
57		ustssxp	$⊢ (U \in UnifOn (X) \land w \in U) \to w \subseteq X \times X$
58	55 56 57	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$
59		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$
60	59	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$
61		ustneism	$⊢ (w \subseteq X \times X \land P \in X) \to w [\{P\}] \times w [\{P\}] \subseteq w \circ w^{-1}$
62	58 60 61	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}$
63		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$
64	63	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$
65		coss1	$⊢ w \subseteq u \to w \circ w \subseteq u \circ w$
66		coss2	$⊢ w \subseteq u \to u \circ w \subseteq u \circ u$
67	65 66	sstrd	$⊢ w \subseteq u \to w \circ w \subseteq u \circ u$
68	67	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$
69		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$
70	68 69	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$
71	64 70	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$
72	62 71	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$
73	72	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)$
74	73	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)$
75	54 74	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$
76		ustexhalf	$⊢ (U \in UnifOn (X) \land v \in U) \to \exists u \in U u \circ u \subseteq v$
77	76	3adant2	$⊢ (U \in UnifOn (X) \land P \in X \land v \in U) \to \exists u \in U u \circ u \subseteq v$
78	75 77	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$
79	48 49 50 78	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$
80	47 79	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$
81	80	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$
82		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))$
83	28 82	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))$
84	14 81 83	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