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 ‘ 𝐽 ) ‘ { 𝑃 } ) )