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 ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )