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 
|- J = ( unifTop ` U )
Assertion utopsnneip 
|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 
 |-  J = ( unifTop ` U )
2 fveq2 
 |-  ( r = p -> ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` r ) = ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) )
3 2 eleq2d 
 |-  ( r = p -> ( b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` r ) <-> b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) ) )
4 3 cbvralvw 
 |-  ( A. r e. b b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` r ) <-> A. p e. b b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) )
5 eleq1w 
 |-  ( b = a -> ( b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) <-> a e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) ) )
6 5 raleqbi1dv 
 |-  ( b = a -> ( A. p e. b b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) <-> A. p e. a a e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) ) )
7 4 6 syl5bb 
 |-  ( b = a -> ( A. r e. b b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` r ) <-> A. p e. a a e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) ) )
8 7 cbvrabv 
 |-  { b e. ~P X | A. r e. b b e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` r ) } = { a e. ~P X | A. p e. a a e. ( ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) ` p ) }
9 simpl 
 |-  ( ( q = p /\ v e. U ) -> q = p )
10 9 sneqd 
 |-  ( ( q = p /\ v e. U ) -> { q } = { p } )
11 10 imaeq2d 
 |-  ( ( q = p /\ v e. U ) -> ( v " { q } ) = ( v " { p } ) )
12 11 mpteq2dva 
 |-  ( q = p -> ( v e. U |-> ( v " { q } ) ) = ( v e. U |-> ( v " { p } ) ) )
13 12 rneqd 
 |-  ( q = p -> ran ( v e. U |-> ( v " { q } ) ) = ran ( v e. U |-> ( v " { p } ) ) )
14 13 cbvmptv 
 |-  ( q e. X |-> ran ( v e. U |-> ( v " { q } ) ) ) = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
15 1 8 14 utopsnneiplem 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )