This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( unifTop ‘ 𝑈 )
Assertion utopsnnei ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 ⊢ 𝐽 = ( unifTop ‘ 𝑈 )
2 eqid ⊢ ( 𝑉 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } )
3 imaeq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } ) )
4 3 rspceeqv ⊢ ( ( 𝑉 ∈ 𝑈 ∧ ( 𝑉 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
5 2 4 mpan2 ⊢ ( 𝑉 ∈ 𝑈 → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
6 5 3ad2ant2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
7 1 utopsnneip ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
8 7 3adant2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
9 8 eleq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) )
10 imaexg ⊢ ( 𝑉 ∈ 𝑈 → ( 𝑉 “ { 𝑃 } ) ∈ V )
11 eqid ⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) )
12 11 elrnmpt ⊢ ( ( 𝑉 “ { 𝑃 } ) ∈ V → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
13 10 12 syl ⊢ ( 𝑉 ∈ 𝑈 → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
14 13 3ad2ant2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
15 9 14 bitrd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
16 6 15 mpbird ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )