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

Theorem tgcl 19922
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 4178 . . . . . . . 8  |-  ( u 
C_  ( topGen `  B
)  ->  U. u  C_ 
U. ( topGen `  B
) )
21adantl 467 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. ( topGen `  B
) )
3 unitg 19919 . . . . . . . 8  |-  ( B  e.  TopBases  ->  U. ( topGen `  B
)  =  U. B
)
43adantr 466 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. ( topGen `
 B )  = 
U. B )
52, 4sseqtrd 3438 . . . . . 6  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. B )
6 eluni2 4161 . . . . . . . 8  |-  ( x  e.  U. u  <->  E. t  e.  u  x  e.  t )
7 ssel2 3397 . . . . . . . . . . . 12  |-  ( ( u  C_  ( topGen `  B )  /\  t  e.  u )  ->  t  e.  ( topGen `  B )
)
8 eltg2b 19911 . . . . . . . . . . . . . . 15  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  <->  A. x  e.  t  E. y  e.  B  (
x  e.  y  /\  y  C_  t ) ) )
9 rsp 2726 . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . 14  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  ->  ( x  e.  t  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) ) ) )
1110imp31 433 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  TopBases  /\  t  e.  ( topGen `  B ) )  /\  x  e.  t )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
1211an32s 811 . . . . . . . . . . . 12  |-  ( ( ( B  e.  TopBases  /\  x  e.  t )  /\  t  e.  ( topGen `
 B ) )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
137, 12sylan2 476 . . . . . . . . . . 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 834 . . . . . . . . . 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 4186 . . . . . . . . . . . . . 14  |-  ( t  e.  u  ->  t  C_ 
U. u )
16 sstr2 3409 . . . . . . . . . . . . . 14  |-  ( y 
C_  t  ->  (
t  C_  U. u  ->  y  C_  U. u
) )
1715, 16syl5com 31 . . . . . . . . . . . . 13  |-  ( t  e.  u  ->  (
y  C_  t  ->  y 
C_  U. u ) )
1817anim2d 567 . . . . . . . . . . . 12  |-  ( t  e.  u  ->  (
( x  e.  y  /\  y  C_  t
)  ->  ( x  e.  y  /\  y  C_ 
U. u ) ) )
1918reximdv 2833 . . . . . . . . . . 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 732 . . . . . . . . . 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 2852 . . . . . . . 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 220 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  ( x  e.  U. u  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) ) )
2423ralrimiv 2772 . . . . . 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 534 . . . . 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 435 . . . 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 19910 . . . 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 237 . . 3  |-  ( B  e.  TopBases  ->  ( u  C_  ( topGen `  B )  ->  U. u  e.  (
topGen `  B ) ) )
2928alrimiv 1767 . 2  |-  ( B  e.  TopBases  ->  A. u ( u 
C_  ( topGen `  B
)  ->  U. u  e.  ( topGen `  B )
) )
30 inss1 3620 . . . . . . . 8  |-  ( u  i^i  v )  C_  u
31 tg1 19916 . . . . . . . 8  |-  ( u  e.  ( topGen `  B
)  ->  u  C_  U. B
)
3230, 31syl5ss 3413 . . . . . . 7  |-  ( u  e.  ( topGen `  B
)  ->  ( u  i^i  v )  C_  U. B
)
3332ad2antrl 732 . . . . . 6  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
u  i^i  v )  C_ 
U. B )
34 eltg2 19910 . . . . . . . . . . . . 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 628 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  A. x  e.  u  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) )
36 rsp 2726 . . . . . . . . . . . 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 17 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  ( x  e.  u  ->  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) ) )
38 eltg2 19910 . . . . . . . . . . . . 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 628 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  A. x  e.  v  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) )
40 rsp 2726 . . . . . . . . . . . 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 17 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  ( x  e.  v  ->  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) )
4237, 41im2anan9 843 . . . . . . . . . 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 3587 . . . . . . . . . 10  |-  ( x  e.  ( u  i^i  v )  <->  ( x  e.  u  /\  x  e.  v ) )
44 reeanv 2930 . . . . . . . . . 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 273 . . . . . . . . 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 837 . . . . . . . 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 3587 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( z  i^i  w )  <->  ( x  e.  z  /\  x  e.  w ) )
4847biimpri 209 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  z  /\  x  e.  w )  ->  x  e.  ( z  i^i  w ) )
49 ss2in 3627 . . . . . . . . . . . . . . . 16  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( z  i^i  w
)  C_  ( u  i^i  v ) )
5048, 49anim12i 568 . . . . . . . . . . . . . . 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 833 . . . . . . . . . . . . . 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 19903 . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . 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 3409 . . . . . . . . . . . . . . . . . . . 20  |-  ( t 
C_  ( z  i^i  w )  ->  (
( z  i^i  w
)  C_  ( u  i^i  v )  ->  t  C_  ( u  i^i  v
) ) )
5655com12 32 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
t  C_  ( z  i^i  w )  ->  t  C_  ( u  i^i  v
) ) )
5756anim2d 567 . . . . . . . . . . . . . . . . . 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 2833 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 657 . . . . . . . . . . . . 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 2852 . . . . . . . . . . . 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 2851 . . . . . . . . . . 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 435 . . . . . . . . . 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 29 . . . . . . . . 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 430 . . . . . . . 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 472 . . . . . . 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 2772 . . . . . 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 534 . . . . 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 435 . . . 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 19910 . . . 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 237 . . 3  |-  ( B  e.  TopBases  ->  ( ( u  e.  ( topGen `  B
)  /\  v  e.  ( topGen `  B )
)  ->  ( u  i^i  v )  e.  (
topGen `  B ) ) )
7473ralrimivv 2780 . 2  |-  ( B  e.  TopBases  ->  A. u  e.  (
topGen `  B ) A. v  e.  ( topGen `  B ) ( u  i^i  v )  e.  ( topGen `  B )
)
75 fvex 5830 . . 3  |-  ( topGen `  B )  e.  _V
76 istopg 19862 . . 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 668 1  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1872   A.wral 2709   E.wrex 2710   _Vcvv 3017    i^i cin 3373    C_ wss 3374   U.cuni 4157   ` cfv 5539   topGenctg 15274   Topctop 19854   TopBasesctb 19857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-iota 5503  df-fun 5541  df-fv 5547  df-topgen 15280  df-top 19858  df-bases 19859
This theorem is referenced by:  tgclb  19923  tgtopon  19924  bastop  19934  elcls3  20036  resttop  20113  leordtval2  20165  tgcmp  20353  2ndctop  20399  2ndcsb  20401  2ndcsep  20411  txtop  20521  pttop  20534  xkotop  20540  alexsubALT  21003  retop  21719  onsuctop  31037  kelac2lem  35835
  Copyright terms: Public domain W3C validator