Metamath Proof Explorer

Theorem utopsnneip

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

Ref Expression
Hypothesis utoptop.1 ⊢J=unifTop⁡U
Assertion utopsnneip ⊢U∈UnifOn⁡X∧P∈X→nei⁡J⁡P=ran⁡v∈U⟼vP

Proof

Step Hyp Ref Expression
1 utoptop.1 ⊢J=unifTop⁡U
2 fveq2 ⊢r=p→q∈X⟼ran⁡v∈U⟼vq⁡r=q∈X⟼ran⁡v∈U⟼vq⁡p
3 2 eleq2d ⊢r=p→b∈q∈X⟼ran⁡v∈U⟼vq⁡r↔b∈q∈X⟼ran⁡v∈U⟼vq⁡p
4 3 cbvralvw ⊢∀r∈bb∈q∈X⟼ran⁡v∈U⟼vq⁡r↔∀p∈bb∈q∈X⟼ran⁡v∈U⟼vq⁡p
5 eleq1w ⊢b=a→b∈q∈X⟼ran⁡v∈U⟼vq⁡p↔a∈q∈X⟼ran⁡v∈U⟼vq⁡p
6 5 raleqbi1dv ⊢b=a→∀p∈bb∈q∈X⟼ran⁡v∈U⟼vq⁡p↔∀p∈aa∈q∈X⟼ran⁡v∈U⟼vq⁡p
7 4 6 bitrid ⊢b=a→∀r∈bb∈q∈X⟼ran⁡v∈U⟼vq⁡r↔∀p∈aa∈q∈X⟼ran⁡v∈U⟼vq⁡p
8 7 cbvrabv ⊢b∈𝒫X|∀r∈bb∈q∈X⟼ran⁡v∈U⟼vq⁡r=a∈𝒫X|∀p∈aa∈q∈X⟼ran⁡v∈U⟼vq⁡p
9 simpl ⊢q=p∧v∈U→q=p
10 9 sneqd ⊢q=p∧v∈U→q=p
11 10 imaeq2d ⊢q=p∧v∈U→vq=vp
12 11 mpteq2dva ⊢q=p→v∈U⟼vq=v∈U⟼vp
13 12 rneqd ⊢q=p→ran⁡v∈U⟼vq=ran⁡v∈U⟼vp
14 13 cbvmptv ⊢q∈X⟼ran⁡v∈U⟼vq=p∈X⟼ran⁡v∈U⟼vp
15 1 8 14 utopsnneiplem ⊢U∈UnifOn⁡X∧P∈X→nei⁡J⁡P=ran⁡v∈U⟼vP