Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-islpt Unicode version

Definition df-islpt 24996
Description: Definition of an isolated point. Experimental. (Contributed by FL, 16-Sep-2013.)
Assertion
Ref Expression
df-islpt  |-  IsolatedPt  =  (
j  e.  Top  |->  ( a  e.  ~P U. j  |->  { x  e.  a  |  E. v  e.  ( ( nei `  j
) `  { x } ) ( v  i^i  a )  =  { x } }
) )
Distinct variable group:    j, a, x, v

Detailed syntax breakdown of Definition df-islpt
StepHypRef Expression
1 cisopt 24995 . 2  class  IsolatedPt
2 vj . . 3  set  j
3 ctop 16631 . . 3  class  Top
4 va . . . 4  set  a
52cv 1622 . . . . . 6  class  j
65cuni 3827 . . . . 5  class  U. j
76cpw 3625 . . . 4  class  ~P U. j
8 vv . . . . . . . . 9  set  v
98cv 1622 . . . . . . . 8  class  v
104cv 1622 . . . . . . . 8  class  a
119, 10cin 3151 . . . . . . 7  class  ( v  i^i  a )
12 vx . . . . . . . . 9  set  x
1312cv 1622 . . . . . . . 8  class  x
1413csn 3640 . . . . . . 7  class  { x }
1511, 14wceq 1623 . . . . . 6  wff  ( v  i^i  a )  =  { x }
16 cnei 16834 . . . . . . . 8  class  nei
175, 16cfv 5255 . . . . . . 7  class  ( nei `  j )
1814, 17cfv 5255 . . . . . 6  class  ( ( nei `  j ) `
 { x }
)
1915, 8, 18wrex 2544 . . . . 5  wff  E. v  e.  ( ( nei `  j
) `  { x } ) ( v  i^i  a )  =  { x }
2019, 12, 10crab 2547 . . . 4  class  { x  e.  a  |  E. v  e.  ( ( nei `  j ) `  { x } ) ( v  i^i  a
)  =  { x } }
214, 7, 20cmpt 4077 . . 3  class  ( a  e.  ~P U. j  |->  { x  e.  a  |  E. v  e.  ( ( nei `  j
) `  { x } ) ( v  i^i  a )  =  { x } }
)
222, 3, 21cmpt 4077 . 2  class  ( j  e.  Top  |->  ( a  e.  ~P U. j  |->  { x  e.  a  |  E. v  e.  ( ( nei `  j
) `  { x } ) ( v  i^i  a )  =  { x } }
) )
231, 22wceq 1623 1  wff  IsolatedPt  =  (
j  e.  Top  |->  ( a  e.  ~P U. j  |->  { x  e.  a  |  E. v  e.  ( ( nei `  j
) `  { x } ) ( v  i^i  a )  =  { x } }
) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator