utopsnneiplem

Description: The neighborhoods of a point P for the topology induced by an uniform space U . (Contributed by Thierry Arnoux, 11-Jan-2018)

	Ref	Expression
Hypotheses	utoptop.1	$⊢ J = unifTop (U)$
	utopsnneip.1	$⊢ K = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
	utopsnneip.2	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
Assertion	utopsnneiplem	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (J) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	$⊢ J = unifTop (U)$
2		utopsnneip.1	$⊢ K = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
3		utopsnneip.2	$⊢ N = (p \in X ⟼ ran (v \in U ⟼ v [\{p\}]))$
4		utopval	$⊢ U \in UnifOn (X) \to unifTop (U) = \{a \in 𝒫 X \| \forall p \in a \exists w \in U w [\{p\}] \subseteq a\}$
5	1 4	syl5eq	$⊢ U \in UnifOn (X) \to J = \{a \in 𝒫 X \| \forall p \in a \exists w \in U w [\{p\}] \subseteq a\}$
6		simpll	$⊢ ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \to U \in UnifOn (X)$
7		simpr	$⊢ (U \in UnifOn (X) \land a \in 𝒫 X) \to a \in 𝒫 X$
8	7	elpwid	$⊢ (U \in UnifOn (X) \land a \in 𝒫 X) \to a \subseteq X$
9	8	sselda	$⊢ ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \to p \in X$
10		simpr	$⊢ (U \in UnifOn (X) \land p \in X) \to p \in X$
11		mptexg	$⊢ U \in UnifOn (X) \to (v \in U ⟼ v [\{p\}]) \in V$
12		rnexg	$⊢ (v \in U ⟼ v [\{p\}]) \in V \to ran (v \in U ⟼ v [\{p\}]) \in V$
13	11 12	syl	$⊢ U \in UnifOn (X) \to ran (v \in U ⟼ v [\{p\}]) \in V$
14	13	adantr	$⊢ (U \in UnifOn (X) \land p \in X) \to ran (v \in U ⟼ v [\{p\}]) \in V$
15	3	fvmpt2	$⊢ (p \in X \land ran (v \in U ⟼ v [\{p\}]) \in V) \to N (p) = ran (v \in U ⟼ v [\{p\}])$
16	10 14 15	syl2anc	$⊢ (U \in UnifOn (X) \land p \in X) \to N (p) = ran (v \in U ⟼ v [\{p\}])$
17	16	eleq2d	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow a \in ran (v \in U ⟼ v [\{p\}]))$
18		eqid	$⊢ (v \in U ⟼ v [\{p\}]) = (v \in U ⟼ v [\{p\}])$
19	18	elrnmpt	$⊢ a \in V \to (a \in ran (v \in U ⟼ v [\{p\}]) \leftrightarrow \exists v \in U a = v [\{p\}])$
20	19	elv	$⊢ a \in ran (v \in U ⟼ v [\{p\}]) \leftrightarrow \exists v \in U a = v [\{p\}]$
21	17 20	bitrdi	$⊢ (U \in UnifOn (X) \land p \in X) \to (a \in N (p) \leftrightarrow \exists v \in U a = v [\{p\}])$
22	6 9 21	syl2anc	$⊢ ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \to (a \in N (p) \leftrightarrow \exists v \in U a = v [\{p\}])$
23		nfv	$⊢ Ⅎ v ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a)$
24		nfre1	$⊢ Ⅎ v \exists v \in U a = v [\{p\}]$
25	23 24	nfan	$⊢ Ⅎ v (((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}])$
26		simplr	$⊢ (((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}]) \land v \in U) \land a = v [\{p\}]) \to v \in U$
27		eqimss2	$⊢ a = v [\{p\}] \to v [\{p\}] \subseteq a$
28	27	adantl	$⊢ (((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}]) \land v \in U) \land a = v [\{p\}]) \to v [\{p\}] \subseteq a$
29		imaeq1	$⊢ w = v \to w [\{p\}] = v [\{p\}]$
30	29	sseq1d	$⊢ w = v \to (w [\{p\}] \subseteq a \leftrightarrow v [\{p\}] \subseteq a)$
31	30	rspcev	$⊢ (v \in U \land v [\{p\}] \subseteq a) \to \exists w \in U w [\{p\}] \subseteq a$
32	26 28 31	syl2anc	$⊢ (((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}]) \land v \in U) \land a = v [\{p\}]) \to \exists w \in U w [\{p\}] \subseteq a$
33		simpr	$⊢ (((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}]) \to \exists v \in U a = v [\{p\}]$
34	25 32 33	r19.29af	$⊢ (((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists v \in U a = v [\{p\}]) \to \exists w \in U w [\{p\}] \subseteq a$
35	6	ad2antrr	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to U \in UnifOn (X)$
36	9	ad2antrr	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to p \in X$
37	35 36	jca	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to (U \in UnifOn (X) \land p \in X)$
38		simpr	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to w [\{p\}] \subseteq a$
39	8	ad3antrrr	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to a \subseteq X$
40		simplr	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to w \in U$
41		eqid	$⊢ w [\{p\}] = w [\{p\}]$
42		imaeq1	$⊢ u = w \to u [\{p\}] = w [\{p\}]$
43	42	rspceeqv	$⊢ (w \in U \land w [\{p\}] = w [\{p\}]) \to \exists u \in U w [\{p\}] = u [\{p\}]$
44	41 43	mpan2	$⊢ w \in U \to \exists u \in U w [\{p\}] = u [\{p\}]$
45	44	adantl	$⊢ ((U \in UnifOn (X) \land p \in X) \land w \in U) \to \exists u \in U w [\{p\}] = u [\{p\}]$
46		vex	$⊢ w \in V$
47	46	imaex	$⊢ w [\{p\}] \in V$
48	3	ustuqtoplem	$⊢ ((U \in UnifOn (X) \land p \in X) \land w [\{p\}] \in V) \to (w [\{p\}] \in N (p) \leftrightarrow \exists u \in U w [\{p\}] = u [\{p\}])$
49	47 48	mpan2	$⊢ (U \in UnifOn (X) \land p \in X) \to (w [\{p\}] \in N (p) \leftrightarrow \exists u \in U w [\{p\}] = u [\{p\}])$
50	49	adantr	$⊢ ((U \in UnifOn (X) \land p \in X) \land w \in U) \to (w [\{p\}] \in N (p) \leftrightarrow \exists u \in U w [\{p\}] = u [\{p\}])$
51	45 50	mpbird	$⊢ ((U \in UnifOn (X) \land p \in X) \land w \in U) \to w [\{p\}] \in N (p)$
52	35 36 40 51	syl21anc	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to w [\{p\}] \in N (p)$
53		sseq1	$⊢ b = w [\{p\}] \to (b \subseteq a \leftrightarrow w [\{p\}] \subseteq a)$
54	53	3anbi2d	$⊢ b = w [\{p\}] \to (((U \in UnifOn (X) \land p \in X) \land b \subseteq a \land a \subseteq X) \leftrightarrow ((U \in UnifOn (X) \land p \in X) \land w [\{p\}] \subseteq a \land a \subseteq X))$
55		eleq1	$⊢ b = w [\{p\}] \to (b \in N (p) \leftrightarrow w [\{p\}] \in N (p))$
56	54 55	anbi12d	$⊢ b = w [\{p\}] \to ((((U \in UnifOn (X) \land p \in X) \land b \subseteq a \land a \subseteq X) \land b \in N (p)) \leftrightarrow (((U \in UnifOn (X) \land p \in X) \land w [\{p\}] \subseteq a \land a \subseteq X) \land w [\{p\}] \in N (p)))$
57	56	imbi1d	$⊢ b = w [\{p\}] \to (((((U \in UnifOn (X) \land p \in X) \land b \subseteq a \land a \subseteq X) \land b \in N (p)) \to a \in N (p)) \leftrightarrow ((((U \in UnifOn (X) \land p \in X) \land w [\{p\}] \subseteq a \land a \subseteq X) \land w [\{p\}] \in N (p)) \to a \in N (p)))$
58	3	ustuqtop1	$⊢ (((U \in UnifOn (X) \land p \in X) \land b \subseteq a \land a \subseteq X) \land b \in N (p)) \to a \in N (p)$
59	47 57 58	vtocl	$⊢ (((U \in UnifOn (X) \land p \in X) \land w [\{p\}] \subseteq a \land a \subseteq X) \land w [\{p\}] \in N (p)) \to a \in N (p)$
60	37 38 39 52 59	syl31anc	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to a \in N (p)$
61	37 21	syl	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to (a \in N (p) \leftrightarrow \exists v \in U a = v [\{p\}])$
62	60 61	mpbid	$⊢ ((((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land w \in U) \land w [\{p\}] \subseteq a) \to \exists v \in U a = v [\{p\}]$
63	62	r19.29an	$⊢ (((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \land \exists w \in U w [\{p\}] \subseteq a) \to \exists v \in U a = v [\{p\}]$
64	34 63	impbida	$⊢ ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \to (\exists v \in U a = v [\{p\}] \leftrightarrow \exists w \in U w [\{p\}] \subseteq a)$
65	22 64	bitrd	$⊢ ((U \in UnifOn (X) \land a \in 𝒫 X) \land p \in a) \to (a \in N (p) \leftrightarrow \exists w \in U w [\{p\}] \subseteq a)$
66	65	ralbidva	$⊢ (U \in UnifOn (X) \land a \in 𝒫 X) \to (\forall p \in a a \in N (p) \leftrightarrow \forall p \in a \exists w \in U w [\{p\}] \subseteq a)$
67	66	rabbidva	$⊢ U \in UnifOn (X) \to \{a \in 𝒫 X \| \forall p \in a a \in N (p)\} = \{a \in 𝒫 X \| \forall p \in a \exists w \in U w [\{p\}] \subseteq a\}$
68	5 67	eqtr4d	$⊢ U \in UnifOn (X) \to J = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
69	68 2	eqtr4di	$⊢ U \in UnifOn (X) \to J = K$
70	69	fveq2d	$⊢ U \in UnifOn (X) \to nei (J) = nei (K)$
71	70	fveq1d	$⊢ U \in UnifOn (X) \to nei (J) (\{P\}) = nei (K) (\{P\})$
72	71	adantr	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (J) (\{P\}) = nei (K) (\{P\})$
73	3	ustuqtop0	$⊢ U \in UnifOn (X) \to N : X ⟶ 𝒫 𝒫 X$
74	3	ustuqtop1	$⊢ (((U \in UnifOn (X) \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$
75	3	ustuqtop2	$⊢ (U \in UnifOn (X) \land p \in X) \to fi (N (p)) \subseteq N (p)$
76	3	ustuqtop3	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to p \in a$
77	3	ustuqtop4	$⊢ ((U \in UnifOn (X) \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$
78	3	ustuqtop5	$⊢ (U \in UnifOn (X) \land p \in X) \to X \in N (p)$
79	2 73 74 75 76 77 78	neiptopnei	$⊢ U \in UnifOn (X) \to N = (p \in X ⟼ nei (K) (\{p\}))$
80	79	adantr	$⊢ (U \in UnifOn (X) \land P \in X) \to N = (p \in X ⟼ nei (K) (\{p\}))$
81		simpr	$⊢ ((U \in UnifOn (X) \land P \in X) \land p = P) \to p = P$
82	81	sneqd	$⊢ ((U \in UnifOn (X) \land P \in X) \land p = P) \to \{p\} = \{P\}$
83	82	fveq2d	$⊢ ((U \in UnifOn (X) \land P \in X) \land p = P) \to nei (K) (\{p\}) = nei (K) (\{P\})$
84		simpr	$⊢ (U \in UnifOn (X) \land P \in X) \to P \in X$
85		fvexd	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (K) (\{P\}) \in V$
86	80 83 84 85	fvmptd	$⊢ (U \in UnifOn (X) \land P \in X) \to N (P) = nei (K) (\{P\})$
87		mptexg	$⊢ U \in UnifOn (X) \to (v \in U ⟼ v [\{P\}]) \in V$
88		rnexg	$⊢ (v \in U ⟼ v [\{P\}]) \in V \to ran (v \in U ⟼ v [\{P\}]) \in V$
89	87 88	syl	$⊢ U \in UnifOn (X) \to ran (v \in U ⟼ v [\{P\}]) \in V$
90	89	adantr	$⊢ (U \in UnifOn (X) \land P \in X) \to ran (v \in U ⟼ v [\{P\}]) \in V$
91		nfv	$⊢ Ⅎ v P \in X$
92		nfmpt1	$⊢ \underline{Ⅎ} v (v \in U ⟼ v [\{P\}])$
93	92	nfrn	$⊢ \underline{Ⅎ} v ran (v \in U ⟼ v [\{P\}])$
94	93	nfel1	$⊢ Ⅎ v ran (v \in U ⟼ v [\{P\}]) \in V$
95	91 94	nfan	$⊢ Ⅎ v (P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V)$
96		nfv	$⊢ Ⅎ v p = P$
97	95 96	nfan	$⊢ Ⅎ v ((P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \land p = P)$
98		simpr2	$⊢ (P \in X \land (ran (v \in U ⟼ v [\{P\}]) \in V \land p = P \land v \in U)) \to p = P$
99	98	sneqd	$⊢ (P \in X \land (ran (v \in U ⟼ v [\{P\}]) \in V \land p = P \land v \in U)) \to \{p\} = \{P\}$
100	99	imaeq2d	$⊢ (P \in X \land (ran (v \in U ⟼ v [\{P\}]) \in V \land p = P \land v \in U)) \to v [\{p\}] = v [\{P\}]$
101	100	3anassrs	$⊢ (((P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \land p = P) \land v \in U) \to v [\{p\}] = v [\{P\}]$
102	97 101	mpteq2da	$⊢ ((P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \land p = P) \to (v \in U ⟼ v [\{p\}]) = (v \in U ⟼ v [\{P\}])$
103	102	rneqd	$⊢ ((P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \land p = P) \to ran (v \in U ⟼ v [\{p\}]) = ran (v \in U ⟼ v [\{P\}])$
104		simpl	$⊢ (P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \to P \in X$
105		simpr	$⊢ (P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \to ran (v \in U ⟼ v [\{P\}]) \in V$
106	3 103 104 105	fvmptd2	$⊢ (P \in X \land ran (v \in U ⟼ v [\{P\}]) \in V) \to N (P) = ran (v \in U ⟼ v [\{P\}])$
107	84 90 106	syl2anc	$⊢ (U \in UnifOn (X) \land P \in X) \to N (P) = ran (v \in U ⟼ v [\{P\}])$
108	72 86 107	3eqtr2d	$⊢ (U \in UnifOn (X) \land P \in X) \to nei (J) (\{P\}) = ran (v \in U ⟼ v [\{P\}])$

Metamath Proof Explorer

Theorem utopsnneiplem

Proof