MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgcl Structured version   Unicode version

Theorem tgcl 19638
Description: Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
Assertion
Ref Expression
tgcl  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )

Proof of Theorem tgcl
Dummy variables  x  y  z  u  t 
v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 4256 . . . . . . . 8  |-  ( u 
C_  ( topGen `  B
)  ->  U. u  C_ 
U. ( topGen `  B
) )
21adantl 464 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. ( topGen `  B
) )
3 unitg 19635 . . . . . . . 8  |-  ( B  e.  TopBases  ->  U. ( topGen `  B
)  =  U. B
)
43adantr 463 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. ( topGen `
 B )  = 
U. B )
52, 4sseqtrd 3525 . . . . . 6  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. B )
6 eluni2 4239 . . . . . . . 8  |-  ( x  e.  U. u  <->  E. t  e.  u  x  e.  t )
7 ssel2 3484 . . . . . . . . . . . 12  |-  ( ( u  C_  ( topGen `  B )  /\  t  e.  u )  ->  t  e.  ( topGen `  B )
)
8 eltg2b 19627 . . . . . . . . . . . . . . 15  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  <->  A. x  e.  t  E. y  e.  B  (
x  e.  y  /\  y  C_  t ) ) )
9 rsp 2820 . . . . . . . . . . . . . . 15  |-  ( A. x  e.  t  E. y  e.  B  (
x  e.  y  /\  y  C_  t )  -> 
( x  e.  t  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) ) )
108, 9syl6bi 228 . . . . . . . . . . . . . 14  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  ->  ( x  e.  t  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) ) ) )
1110imp31 430 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  TopBases  /\  t  e.  ( topGen `  B ) )  /\  x  e.  t )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
1211an32s 802 . . . . . . . . . . . 12  |-  ( ( ( B  e.  TopBases  /\  x  e.  t )  /\  t  e.  ( topGen `
 B ) )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
137, 12sylan2 472 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  x  e.  t )  /\  ( u  C_  ( topGen `
 B )  /\  t  e.  u )
)  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
1413an42s 825 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B
) )  /\  (
t  e.  u  /\  x  e.  t )
)  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
15 elssuni 4264 . . . . . . . . . . . . . 14  |-  ( t  e.  u  ->  t  C_ 
U. u )
16 sstr2 3496 . . . . . . . . . . . . . 14  |-  ( y 
C_  t  ->  (
t  C_  U. u  ->  y  C_  U. u
) )
1715, 16syl5com 30 . . . . . . . . . . . . 13  |-  ( t  e.  u  ->  (
y  C_  t  ->  y 
C_  U. u ) )
1817anim2d 563 . . . . . . . . . . . 12  |-  ( t  e.  u  ->  (
( x  e.  y  /\  y  C_  t
)  ->  ( x  e.  y  /\  y  C_ 
U. u ) ) )
1918reximdv 2928 . . . . . . . . . . 11  |-  ( t  e.  u  ->  ( E. y  e.  B  ( x  e.  y  /\  y  C_  t )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  U. u
) ) )
2019ad2antrl 725 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B
) )  /\  (
t  e.  u  /\  x  e.  t )
)  ->  ( E. y  e.  B  (
x  e.  y  /\  y  C_  t )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  U. u
) ) )
2114, 20mpd 15 . . . . . . . . 9  |-  ( ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B
) )  /\  (
t  e.  u  /\  x  e.  t )
)  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) )
2221rexlimdvaa 2947 . . . . . . . 8  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  ( E. t  e.  u  x  e.  t  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) ) )
236, 22syl5bi 217 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  ( x  e.  U. u  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) ) )
2423ralrimiv 2866 . . . . . 6  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  A. x  e.  U. u E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) )
255, 24jca 530 . . . . 5  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  ( U. u  C_  U. B  /\  A. x  e.  U. u E. y  e.  B  ( x  e.  y  /\  y  C_  U. u
) ) )
2625ex 432 . . . 4  |-  ( B  e.  TopBases  ->  ( u  C_  ( topGen `  B )  ->  ( U. u  C_  U. B  /\  A. x  e.  U. u E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) ) ) )
27 eltg2 19626 . . . 4  |-  ( B  e.  TopBases  ->  ( U. u  e.  ( topGen `  B )  <->  ( U. u  C_  U. B  /\  A. x  e.  U. u E. y  e.  B  ( x  e.  y  /\  y  C_  U. u
) ) ) )
2826, 27sylibrd 234 . . 3  |-  ( B  e.  TopBases  ->  ( u  C_  ( topGen `  B )  ->  U. u  e.  (
topGen `  B ) ) )
2928alrimiv 1724 . 2  |-  ( B  e.  TopBases  ->  A. u ( u 
C_  ( topGen `  B
)  ->  U. u  e.  ( topGen `  B )
) )
30 inss1 3704 . . . . . . . 8  |-  ( u  i^i  v )  C_  u
31 tg1 19632 . . . . . . . 8  |-  ( u  e.  ( topGen `  B
)  ->  u  C_  U. B
)
3230, 31syl5ss 3500 . . . . . . 7  |-  ( u  e.  ( topGen `  B
)  ->  ( u  i^i  v )  C_  U. B
)
3332ad2antrl 725 . . . . . 6  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
u  i^i  v )  C_ 
U. B )
34 eltg2 19626 . . . . . . . . . . . . 13  |-  ( B  e.  TopBases  ->  ( u  e.  ( topGen `  B )  <->  ( u  C_  U. B  /\  A. x  e.  u  E. z  e.  B  (
x  e.  z  /\  z  C_  u ) ) ) )
3534simplbda 622 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  A. x  e.  u  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) )
36 rsp 2820 . . . . . . . . . . . 12  |-  ( A. x  e.  u  E. z  e.  B  (
x  e.  z  /\  z  C_  u )  -> 
( x  e.  u  ->  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) ) )
3735, 36syl 16 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  ( x  e.  u  ->  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) ) )
38 eltg2 19626 . . . . . . . . . . . . 13  |-  ( B  e.  TopBases  ->  ( v  e.  ( topGen `  B )  <->  ( v  C_  U. B  /\  A. x  e.  v  E. w  e.  B  (
x  e.  w  /\  w  C_  v ) ) ) )
3938simplbda 622 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  A. x  e.  v  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) )
40 rsp 2820 . . . . . . . . . . . 12  |-  ( A. x  e.  v  E. w  e.  B  (
x  e.  w  /\  w  C_  v )  -> 
( x  e.  v  ->  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) )
4139, 40syl 16 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  ( x  e.  v  ->  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) )
4237, 41im2anan9 833 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B ) )  /\  ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
) )  ->  (
( x  e.  u  /\  x  e.  v
)  ->  ( E. z  e.  B  (
x  e.  z  /\  z  C_  u )  /\  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) ) )
43 elin 3673 . . . . . . . . . 10  |-  ( x  e.  ( u  i^i  v )  <->  ( x  e.  u  /\  x  e.  v ) )
44 reeanv 3022 . . . . . . . . . 10  |-  ( E. z  e.  B  E. w  e.  B  (
( x  e.  z  /\  z  C_  u
)  /\  ( x  e.  w  /\  w  C_  v ) )  <->  ( E. z  e.  B  (
x  e.  z  /\  z  C_  u )  /\  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) )
4542, 43, 443imtr4g 270 . . . . . . . . 9  |-  ( ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B ) )  /\  ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
) )  ->  (
x  e.  ( u  i^i  v )  ->  E. z  e.  B  E. w  e.  B  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) ) ) )
4645anandis 828 . . . . . . . 8  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
x  e.  ( u  i^i  v )  ->  E. z  e.  B  E. w  e.  B  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) ) ) )
47 elin 3673 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( z  i^i  w )  <->  ( x  e.  z  /\  x  e.  w ) )
4847biimpri 206 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  z  /\  x  e.  w )  ->  x  e.  ( z  i^i  w ) )
49 ss2in 3711 . . . . . . . . . . . . . . . 16  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( z  i^i  w
)  C_  ( u  i^i  v ) )
5048, 49anim12i 564 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  z  /\  x  e.  w
)  /\  ( z  C_  u  /\  w  C_  v ) )  -> 
( x  e.  ( z  i^i  w )  /\  ( z  i^i  w )  C_  (
u  i^i  v )
) )
5150an4s 824 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  z  /\  z  C_  u
)  /\  ( x  e.  w  /\  w  C_  v ) )  -> 
( x  e.  ( z  i^i  w )  /\  ( z  i^i  w )  C_  (
u  i^i  v )
) )
52 basis2 19619 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  e.  TopBases  /\  z  e.  B )  /\  ( w  e.  B  /\  x  e.  (
z  i^i  w )
) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( z  i^i  w
) ) )
5352adantllr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( B  e.  TopBases 
/\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  /\  (
w  e.  B  /\  x  e.  ( z  i^i  w ) ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( z  i^i  w ) ) )
5453adantrrr 722 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  e.  TopBases 
/\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  /\  (
w  e.  B  /\  ( x  e.  (
z  i^i  w )  /\  ( z  i^i  w
)  C_  ( u  i^i  v ) ) ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( z  i^i  w
) ) )
55 sstr2 3496 . . . . . . . . . . . . . . . . . . . 20  |-  ( t 
C_  ( z  i^i  w )  ->  (
( z  i^i  w
)  C_  ( u  i^i  v )  ->  t  C_  ( u  i^i  v
) ) )
5655com12 31 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
t  C_  ( z  i^i  w )  ->  t  C_  ( u  i^i  v
) ) )
5756anim2d 563 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
( x  e.  t  /\  t  C_  (
z  i^i  w )
)  ->  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) ) )
5857reximdv 2928 . . . . . . . . . . . . . . . . 17  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  ( E. t  e.  B  ( x  e.  t  /\  t  C_  ( z  i^i  w ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
5958adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( z  i^i  w )  /\  ( z  i^i  w
)  C_  ( u  i^i  v ) )  -> 
( E. t  e.  B  ( x  e.  t  /\  t  C_  ( z  i^i  w
) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) ) )
6059ad2antll 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  e.  TopBases 
/\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  /\  (
w  e.  B  /\  ( x  e.  (
z  i^i  w )  /\  ( z  i^i  w
)  C_  ( u  i^i  v ) ) ) )  ->  ( E. t  e.  B  (
x  e.  t  /\  t  C_  ( z  i^i  w ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
6154, 60mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( B  e.  TopBases 
/\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  /\  (
w  e.  B  /\  ( x  e.  (
z  i^i  w )  /\  ( z  i^i  w
)  C_  ( u  i^i  v ) ) ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) )
6251, 61sylanr2 651 . . . . . . . . . . . . 13  |-  ( ( ( ( B  e.  TopBases 
/\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  /\  (
w  e.  B  /\  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) ) ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) )
6362rexlimdvaa 2947 . . . . . . . . . . . 12  |-  ( ( ( B  e.  TopBases  /\  x  e.  ( u  i^i  v ) )  /\  z  e.  B )  ->  ( E. w  e.  B  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
6463rexlimdva 2946 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  x  e.  ( u  i^i  v
) )  ->  ( E. z  e.  B  E. w  e.  B  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
6564ex 432 . . . . . . . . . 10  |-  ( B  e.  TopBases  ->  ( x  e.  ( u  i^i  v
)  ->  ( E. z  e.  B  E. w  e.  B  (
( x  e.  z  /\  z  C_  u
)  /\  ( x  e.  w  /\  w  C_  v ) )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) ) )
6665a2d 26 . . . . . . . . 9  |-  ( B  e.  TopBases  ->  ( ( x  e.  ( u  i^i  v )  ->  E. z  e.  B  E. w  e.  B  ( (
x  e.  z  /\  z  C_  u )  /\  ( x  e.  w  /\  w  C_  v ) ) )  ->  (
x  e.  ( u  i^i  v )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) ) )
6766imp 427 . . . . . . . 8  |-  ( ( B  e.  TopBases  /\  (
x  e.  ( u  i^i  v )  ->  E. z  e.  B  E. w  e.  B  ( ( x  e.  z  /\  z  C_  u )  /\  (
x  e.  w  /\  w  C_  v ) ) ) )  ->  (
x  e.  ( u  i^i  v )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
6846, 67syldan 468 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
x  e.  ( u  i^i  v )  ->  E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
6968ralrimiv 2866 . . . . . 6  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  A. x  e.  ( u  i^i  v
) E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) )
7033, 69jca 530 . . . . 5  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
( u  i^i  v
)  C_  U. B  /\  A. x  e.  ( u  i^i  v ) E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) )
7170ex 432 . . . 4  |-  ( B  e.  TopBases  ->  ( ( u  e.  ( topGen `  B
)  /\  v  e.  ( topGen `  B )
)  ->  ( (
u  i^i  v )  C_ 
U. B  /\  A. x  e.  ( u  i^i  v ) E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v
) ) ) ) )
72 eltg2 19626 . . . 4  |-  ( B  e.  TopBases  ->  ( ( u  i^i  v )  e.  ( topGen `  B )  <->  ( ( u  i^i  v
)  C_  U. B  /\  A. x  e.  ( u  i^i  v ) E. t  e.  B  ( x  e.  t  /\  t  C_  ( u  i^i  v ) ) ) ) )
7371, 72sylibrd 234 . . 3  |-  ( B  e.  TopBases  ->  ( ( u  e.  ( topGen `  B
)  /\  v  e.  ( topGen `  B )
)  ->  ( u  i^i  v )  e.  (
topGen `  B ) ) )
7473ralrimivv 2874 . 2  |-  ( B  e.  TopBases  ->  A. u  e.  (
topGen `  B ) A. v  e.  ( topGen `  B ) ( u  i^i  v )  e.  ( topGen `  B )
)
75 fvex 5858 . . 3  |-  ( topGen `  B )  e.  _V
76 istopg 19571 . . 3  |-  ( (
topGen `  B )  e. 
_V  ->  ( ( topGen `  B )  e.  Top  <->  ( A. u ( u  C_  ( topGen `  B )  ->  U. u  e.  (
topGen `  B ) )  /\  A. u  e.  ( topGen `  B ) A. v  e.  ( topGen `
 B ) ( u  i^i  v )  e.  ( topGen `  B
) ) ) )
7775, 76ax-mp 5 . 2  |-  ( (
topGen `  B )  e. 
Top 
<->  ( A. u ( u  C_  ( topGen `  B )  ->  U. u  e.  ( topGen `  B )
)  /\  A. u  e.  ( topGen `  B ) A. v  e.  ( topGen `
 B ) ( u  i^i  v )  e.  ( topGen `  B
) ) )
7829, 74, 77sylanbrc 662 1  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1396    = wceq 1398    e. wcel 1823   A.wral 2804   E.wrex 2805   _Vcvv 3106    i^i cin 3460    C_ wss 3461   U.cuni 4235   ` cfv 5570   topGenctg 14927   Topctop 19561   TopBasesctb 19565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fv 5578  df-topgen 14933  df-top 19566  df-bases 19568
This theorem is referenced by:  tgclb  19639  tgtopon  19640  bastop  19650  elcls3  19751  resttop  19828  leordtval2  19880  tgcmp  20068  2ndctop  20114  2ndcsb  20116  2ndcsep  20126  txtop  20236  pttop  20249  xkotop  20255  alexsubALT  20717  retop  21434  onsuctop  30126  kelac2lem  31249
  Copyright terms: Public domain W3C validator