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 ⟼ v P

Proof

Step Hyp Ref Expression
1 utoptop.1 ⊢ J = unifTop ⁡ U
2 fveq2 ⊢ r = p → q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ r = q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
3 2 eleq2d ⊢ r = p → b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ r ↔ b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
4 3 cbvralvw ⊢ ∀ r ∈ b b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ r ↔ ∀ p ∈ b b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
5 eleq1w ⊢ b = a → b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p ↔ a ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
6 5 raleqbi1dv ⊢ b = a → ∀ p ∈ b b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p ↔ ∀ p ∈ a a ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
7 4 6 bitrid ⊢ b = a → ∀ r ∈ b b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ r ↔ ∀ p ∈ a a ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ p
8 7 cbvrabv ⊢ b ∈ 𝒫 X | ∀ r ∈ b b ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ r = a ∈ 𝒫 X | ∀ p ∈ a a ∈ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q ⁡ 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 → v q = v p
12 11 mpteq2dva ⊢ q = p → v ∈ U ⟼ v q = v ∈ U ⟼ v p
13 12 rneqd ⊢ q = p → ran ⁡ v ∈ U ⟼ v q = ran ⁡ v ∈ U ⟼ v p
14 13 cbvmptv ⊢ q ∈ X ⟼ ran ⁡ v ∈ U ⟼ v q = p ∈ X ⟼ ran ⁡ v ∈ U ⟼ v p
15 1 8 14 utopsnneiplem ⊢ U ∈ UnifOn ⁡ X ∧ P ∈ X → nei ⁡ J ⁡ P = ran ⁡ v ∈ U ⟼ v P