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

Theorem tgcl 16669
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
StepHypRef Expression
1 uniss 3822 . . . . . . . 8  |-  ( u 
C_  ( topGen `  B
)  ->  U. u  C_ 
U. ( topGen `  B
) )
21adantl 454 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. ( topGen `  B
) )
3 unitg 16667 . . . . . . . 8  |-  ( B  e.  TopBases  ->  U. ( topGen `  B
)  =  U. B
)
43adantr 453 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. ( topGen `
 B )  = 
U. B )
52, 4sseqtrd 3189 . . . . . 6  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  U. u  C_ 
U. B )
6 eluni2 3805 . . . . . . . 8  |-  ( x  e.  U. u  <->  E. t  e.  u  x  e.  t )
7 ssel2 3150 . . . . . . . . . . . . 13  |-  ( ( u  C_  ( topGen `  B )  /\  t  e.  u )  ->  t  e.  ( topGen `  B )
)
8 eltg2b 16659 . . . . . . . . . . . . . . . 16  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  <->  A. x  e.  t  E. y  e.  B  (
x  e.  y  /\  y  C_  t ) ) )
9 ra4 2578 . . . . . . . . . . . . . . . 16  |-  ( 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 221 . . . . . . . . . . . . . . 15  |-  ( B  e.  TopBases  ->  ( t  e.  ( topGen `  B )  ->  ( x  e.  t  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) ) ) )
1110imp31 423 . . . . . . . . . . . . . 14  |-  ( ( ( B  e.  TopBases  /\  t  e.  ( topGen `  B ) )  /\  x  e.  t )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
1211an32s 782 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  TopBases  /\  x  e.  t )  /\  t  e.  ( topGen `
 B ) )  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
137, 12sylan2 462 . . . . . . . . . . . 12  |-  ( ( ( B  e.  TopBases  /\  x  e.  t )  /\  ( u  C_  ( topGen `
 B )  /\  t  e.  u )
)  ->  E. y  e.  B  ( x  e.  y  /\  y  C_  t ) )
1413an42s 803 . . . . . . . . . . 11  |-  ( ( ( 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 3829 . . . . . . . . . . . . . . 15  |-  ( t  e.  u  ->  t  C_ 
U. u )
16 sstr2 3161 . . . . . . . . . . . . . . 15  |-  ( y 
C_  t  ->  (
t  C_  U. u  ->  y  C_  U. u
) )
1715, 16syl5com 28 . . . . . . . . . . . . . 14  |-  ( t  e.  u  ->  (
y  C_  t  ->  y 
C_  U. u ) )
1817anim2d 550 . . . . . . . . . . . . 13  |-  ( t  e.  u  ->  (
( x  e.  y  /\  y  C_  t
)  ->  ( x  e.  y  /\  y  C_ 
U. u ) ) )
1918reximdv 2629 . . . . . . . . . . . 12  |-  ( 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 711 . . . . . . . . . . 11  |-  ( ( ( 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 16 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B
) )  /\  (
t  e.  u  /\  x  e.  t )
)  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) )
2221exp32 591 . . . . . . . . 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 ) ) ) )
2322rexlimdv 2641 . . . . . . . 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 ) ) )
246, 23syl5bi 210 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  ( x  e.  U. u  ->  E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) ) )
2524ralrimiv 2600 . . . . . 6  |-  ( ( B  e.  TopBases  /\  u  C_  ( topGen `  B )
)  ->  A. x  e.  U. u E. y  e.  B  ( x  e.  y  /\  y  C_ 
U. u ) )
265, 25jca 520 . . . . 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
) ) )
2726ex 425 . . . 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 ) ) ) )
28 eltg2 16658 . . . 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
) ) ) )
2927, 28sylibrd 227 . . 3  |-  ( B  e.  TopBases  ->  ( u  C_  ( topGen `  B )  ->  U. u  e.  (
topGen `  B ) ) )
3029alrimiv 2013 . 2  |-  ( B  e.  TopBases  ->  A. u ( u 
C_  ( topGen `  B
)  ->  U. u  e.  ( topGen `  B )
) )
31 inss1 3364 . . . . . . . 8  |-  ( u  i^i  v )  C_  u
32 tg1 16664 . . . . . . . 8  |-  ( u  e.  ( topGen `  B
)  ->  u  C_  U. B
)
3331, 32syl5ss 3165 . . . . . . 7  |-  ( u  e.  ( topGen `  B
)  ->  ( u  i^i  v )  C_  U. B
)
3433ad2antrl 711 . . . . . 6  |-  ( ( B  e.  TopBases  /\  (
u  e.  ( topGen `  B )  /\  v  e.  ( topGen `  B )
) )  ->  (
u  i^i  v )  C_ 
U. B )
35 eltg2 16658 . . . . . . . . . . . . 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 ) ) ) )
3635simplbda 610 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  A. x  e.  u  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) )
37 ra4 2578 . . . . . . . . . . . 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 ) ) )
3836, 37syl 17 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  u  e.  ( topGen `  B )
)  ->  ( x  e.  u  ->  E. z  e.  B  ( x  e.  z  /\  z  C_  u ) ) )
39 eltg2 16658 . . . . . . . . . . . . 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 ) ) ) )
4039simplbda 610 . . . . . . . . . . . 12  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  A. x  e.  v  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) )
41 ra4 2578 . . . . . . . . . . . 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 ) ) )
4240, 41syl 17 . . . . . . . . . . 11  |-  ( ( B  e.  TopBases  /\  v  e.  ( topGen `  B )
)  ->  ( x  e.  v  ->  E. w  e.  B  ( x  e.  w  /\  w  C_  v ) ) )
4338, 42im2anan9 811 . . . . . . . . . 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 ) ) ) )
44 elin 3333 . . . . . . . . . 10  |-  ( x  e.  ( u  i^i  v )  <->  ( x  e.  u  /\  x  e.  v ) )
45 reeanv 2682 . . . . . . . . . 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 ) ) )
4643, 44, 453imtr4g 263 . . . . . . . . 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 ) ) ) )
4746anandis 806 . . . . . . . 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 ) ) ) )
48 elin 3333 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( z  i^i  w )  <->  ( x  e.  z  /\  x  e.  w ) )
4948biimpri 199 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  z  /\  x  e.  w )  ->  x  e.  ( z  i^i  w ) )
50 ss2in 3371 . . . . . . . . . . . . . . . . 17  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( z  i^i  w
)  C_  ( u  i^i  v ) )
5149, 50anim12i 551 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
) )
5251an4s 802 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
) )
53 basis2 16651 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )
5453adantllr 702 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )
5554adantrrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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
) ) )
56 sstr2 3161 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t 
C_  ( z  i^i  w )  ->  (
( z  i^i  w
)  C_  ( u  i^i  v )  ->  t  C_  ( u  i^i  v
) ) )
5756com12 29 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
t  C_  ( z  i^i  w )  ->  t  C_  ( u  i^i  v
) ) )
5857anim2d 550 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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
) ) ) )
5958reximdv 2629 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
6059adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) ) )
6160ad2antll 712 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) )
6255, 61mpd 16 . . . . . . . . . . . . . . 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_  ( u  i^i  v
) ) )
6352, 62sylanr2 637 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
6463exp32 591 . . . . . . . . . . . . 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 ) ) ) ) )
6564rexlimdv 2641 . . . . . . . . . . . 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 ) ) ) )
6665rexlimdva 2642 . . . . . . . . . . 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 ) ) ) )
6766ex 425 . . . . . . . . . 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 ) ) ) ) )
6867a2d 25 . . . . . . . . 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 ) ) ) ) )
6968imp 420 . . . . . . . 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 ) ) ) )
7047, 69syldan 458 . . . . . . 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 ) ) ) )
7170ralrimiv 2600 . . . . . 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
) ) )
7234, 71jca 520 . . . . 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 ) ) ) )
7372ex 425 . . . 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
) ) ) ) )
74 eltg2 16658 . . . 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 ) ) ) ) )
7573, 74sylibrd 227 . . 3  |-  ( B  e.  TopBases  ->  ( ( u  e.  ( topGen `  B
)  /\  v  e.  ( topGen `  B )
)  ->  ( u  i^i  v )  e.  (
topGen `  B ) ) )
7675ralrimivv 2609 . 2  |-  ( B  e.  TopBases  ->  A. u  e.  (
topGen `  B ) A. v  e.  ( topGen `  B ) ( u  i^i  v )  e.  ( topGen `  B )
)
77 fvex 5472 . . 3  |-  ( topGen `  B )  e.  _V
78 istopg 16603 . . 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
) ) ) )
7977, 78ax-mp 10 . 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
) ) )
8030, 76, 79sylanbrc 648 1  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621   A.wral 2518   E.wrex 2519   _Vcvv 2763    i^i cin 3126    C_ wss 3127   U.cuni 3801   ` cfv 4673   topGenctg 13304   Topctop 16593   TopBasesctb 16597
This theorem is referenced by:  tgclb  16670  tgtopon  16671  bastop  16681  elcls3  16782  resttop  16853  leordtval2  16904  tgcmp  17090  2ndctop  17135  2ndcsb  17137  2ndcsep  17147  txtop  17226  pttop  17239  xkotop  17245  alexsubALT  17707  retop  18232  onsuctop  24247  stovr  24890  intopcoaconb  24907  intopcoaconc  24908  kelac2lem  26529
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fv 4689  df-topgen 13306  df-top 16598  df-bases 16600
  Copyright terms: Public domain W3C validator