Metamath Proof Explorer

Theorem utopsnnei

Description: Images of singletons by entourages V are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018)

Ref Expression
Hypothesis utoptop.1 ⊢ J = unifTop ⁡ U
Assertion utopsnnei ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ∈ nei ⁡ J ⁡ P

Proof

Step Hyp Ref Expression
1 utoptop.1 ⊢ J = unifTop ⁡ U
2 eqid ⊢ V P = V P
3 imaeq1 ⊢ v = V → v P = V P
4 3 rspceeqv ⊢ V ∈ U ∧ V P = V P → ∃ v ∈ U V P = v P
5 2 4 mpan2 ⊢ V ∈ U → ∃ v ∈ U V P = v P
6 5 3ad2ant2 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → ∃ v ∈ U V P = v P
7 1 utopsnneip ⊢ U ∈ UnifOn ⁡ X ∧ P ∈ X → nei ⁡ J ⁡ P = ran ⁡ v ∈ U ⟼ v P
8 7 3adant2 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → nei ⁡ J ⁡ P = ran ⁡ v ∈ U ⟼ v P
9 8 eleq2d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ∈ nei ⁡ J ⁡ P ↔ V P ∈ ran ⁡ v ∈ U ⟼ v P
10 imaexg ⊢ V ∈ U → V P ∈ V
11 eqid ⊢ v ∈ U ⟼ v P = v ∈ U ⟼ v P
12 11 elrnmpt ⊢ V P ∈ V → V P ∈ ran ⁡ v ∈ U ⟼ v P ↔ ∃ v ∈ U V P = v P
13 10 12 syl ⊢ V ∈ U → V P ∈ ran ⁡ v ∈ U ⟼ v P ↔ ∃ v ∈ U V P = v P
14 13 3ad2ant2 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ∈ ran ⁡ v ∈ U ⟼ v P ↔ ∃ v ∈ U V P = v P
15 9 14 bitrd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ∈ nei ⁡ J ⁡ P ↔ ∃ v ∈ U V P = v P
16 6 15 mpbird ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ∈ nei ⁡ J ⁡ P