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

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

Proof

Step Hyp Ref Expression
1 utoptop.1 ⊢ 𝐽 = ( unifTop ‘ 𝑈 )
2 fveq2 ⊢ ( 𝑟 = 𝑝 → ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑟 ) = ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) )
3 2 eleq2d ⊢ ( 𝑟 = 𝑝 → ( 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑟 ) ↔ 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ) )
4 3 cbvralvw ⊢ ( ∀ 𝑟 ∈ 𝑏 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑟 ) ↔ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) )
5 eleq1w ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ↔ 𝑎 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ) )
6 5 raleqbi1dv ⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ) )
7 4 6 bitrid ⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑟 ∈ 𝑏 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑟 ) ↔ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) ) )
8 7 cbvrabv ⊢ { 𝑏 ∈ 𝒫 𝑋 ∣ ∀ 𝑟 ∈ 𝑏 𝑏 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑟 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) ‘ 𝑝 ) }
9 simpl ⊢ ( ( 𝑞 = 𝑝 ∧ 𝑣 ∈ 𝑈 ) → 𝑞 = 𝑝 )
10 9 sneqd ⊢ ( ( 𝑞 = 𝑝 ∧ 𝑣 ∈ 𝑈 ) → { 𝑞 } = { 𝑝 } )
11 10 imaeq2d ⊢ ( ( 𝑞 = 𝑝 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑞 } ) = ( 𝑣 “ { 𝑝 } ) )
12 11 mpteq2dva ⊢ ( 𝑞 = 𝑝 → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
13 12 rneqd ⊢ ( 𝑞 = 𝑝 → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
14 13 cbvmptv ⊢ ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
15 1 8 14 utopsnneiplem ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )