ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-topgen Unicode version

Definition df-topgen 12587
Description: Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78. (Contributed by NM, 16-Jul-2006.)
Assertion
Ref Expression
df-topgen  |-  topGen  =  ( x  e.  _V  |->  { y  |  y  C_  U. ( x  i^i  ~P y ) } )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-topgen
StepHypRef Expression
1 ctg 12581 . 2  class  topGen
2 vx . . 3  setvar  x
3 cvv 2730 . . 3  class  _V
4 vy . . . . . 6  setvar  y
54cv 1347 . . . . 5  class  y
62cv 1347 . . . . . . 7  class  x
75cpw 3564 . . . . . . 7  class  ~P y
86, 7cin 3120 . . . . . 6  class  ( x  i^i  ~P y )
98cuni 3794 . . . . 5  class  U. (
x  i^i  ~P y
)
105, 9wss 3121 . . . 4  wff  y  C_  U. ( x  i^i  ~P y )
1110, 4cab 2156 . . 3  class  { y  |  y  C_  U. (
x  i^i  ~P y
) }
122, 3, 11cmpt 4048 . 2  class  ( x  e.  _V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
131, 12wceq 1348 1  wff  topGen  =  ( x  e.  _V  |->  { y  |  y  C_  U. ( x  i^i  ~P y ) } )
Colors of variables: wff set class
This definition is referenced by:  tgval  12802  eltg4i  12808  eltg3  12810  tg1  12812  tg2  12813  tgclb  12818
  Copyright terms: Public domain W3C validator