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

Theorem tgcmp 20006
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 20649, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
tgcmp  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( topGen `  B
)  e.  Comp  <->  A. y  e.  ~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
) ) )
Distinct variable groups:    y, z, B    y, X, z

Proof of Theorem tgcmp
Dummy variables  t 
f  u  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2392 . . . . 5  |-  U. ( topGen `
 B )  = 
U. ( topGen `  B
)
21iscmp 19993 . . . 4  |-  ( (
topGen `  B )  e. 
Comp 
<->  ( ( topGen `  B
)  e.  Top  /\  A. y  e.  ~P  ( topGen `
 B ) ( U. ( topGen `  B
)  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) U. ( topGen `  B
)  =  U. z
) ) )
32simprbi 462 . . 3  |-  ( (
topGen `  B )  e. 
Comp  ->  A. y  e.  ~P  ( topGen `  B )
( U. ( topGen `  B )  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) U. ( topGen `  B
)  =  U. z
) )
4 unitg 19572 . . . . . . . 8  |-  ( B  e.  TopBases  ->  U. ( topGen `  B
)  =  U. B
)
5 eqtr3 2420 . . . . . . . 8  |-  ( ( U. ( topGen `  B
)  =  U. B  /\  X  =  U. B )  ->  U. ( topGen `
 B )  =  X )
64, 5sylan 469 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  ->  U. ( topGen `  B )  =  X )
76eqeq1d 2394 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. y 
<->  X  =  U. y
) )
86eqeq1d 2394 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. z 
<->  X  =  U. z
) )
98rexbidv 2906 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( E. z  e.  ( ~P y  i^i 
Fin ) U. ( topGen `
 B )  = 
U. z  <->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) )
107, 9imbi12d 318 . . . . 5  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( U. ( topGen `
 B )  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) U. ( topGen `
 B )  = 
U. z )  <->  ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) ) )
1110ralbidv 2831 . . . 4  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. y  e. 
~P  ( topGen `  B
) ( U. ( topGen `
 B )  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) U. ( topGen `
 B )  = 
U. z )  <->  A. y  e.  ~P  ( topGen `  B
) ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) ) )
12 bastg 19571 . . . . . . 7  |-  ( B  e.  TopBases  ->  B  C_  ( topGen `
 B ) )
1312adantr 463 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  ->  B  C_  ( topGen `  B
) )
14 sspwb 4624 . . . . . 6  |-  ( B 
C_  ( topGen `  B
)  <->  ~P B  C_  ~P ( topGen `  B )
)
1513, 14sylib 196 . . . . 5  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  ->  ~P B  C_  ~P ( topGen `
 B ) )
16 ssralv 3491 . . . . 5  |-  ( ~P B  C_  ~P ( topGen `
 B )  -> 
( A. y  e. 
~P  ( topGen `  B
) ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z )  ->  A. y  e.  ~P  B ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) ) )
1715, 16syl 16 . . . 4  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. y  e. 
~P  ( topGen `  B
) ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z )  ->  A. y  e.  ~P  B ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) ) )
1811, 17sylbid 215 . . 3  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. y  e. 
~P  ( topGen `  B
) ( U. ( topGen `
 B )  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) U. ( topGen `
 B )  = 
U. z )  ->  A. y  e.  ~P  B ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z ) ) )
193, 18syl5 32 . 2  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( topGen `  B
)  e.  Comp  ->  A. y  e.  ~P  B
( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z ) ) )
20 elpwi 3949 . . . . 5  |-  ( u  e.  ~P ( topGen `  B )  ->  u  C_  ( topGen `  B )
)
21 simprr 755 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  =  U. u
)
22 simprl 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  u  C_  ( topGen `  B
) )
2322sselda 3430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  t  e.  u
)  ->  t  e.  ( topGen `  B )
)
2423adantrr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( t  e.  u  /\  y  e.  t ) )  -> 
t  e.  ( topGen `  B ) )
25 simprr 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( t  e.  u  /\  y  e.  t ) )  -> 
y  e.  t )
26 tg2 19570 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  ( topGen `  B )  /\  y  e.  t )  ->  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) )
2724, 25, 26syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( t  e.  u  /\  y  e.  t ) )  ->  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) )
2827expr 613 . . . . . . . . . . . . . 14  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  t  e.  u
)  ->  ( y  e.  t  ->  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) ) )
2928reximdva 2867 . . . . . . . . . . . . 13  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( E. t  e.  u  y  e.  t  ->  E. t  e.  u  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) ) )
30 eluni2 4180 . . . . . . . . . . . . 13  |-  ( y  e.  U. u  <->  E. t  e.  u  y  e.  t )
31 elunirab 4188 . . . . . . . . . . . . . 14  |-  ( y  e.  U. { w  e.  B  |  E. t  e.  u  w  C_  t }  <->  E. w  e.  B  ( y  e.  w  /\  E. t  e.  u  w  C_  t
) )
32 r19.42v 2950 . . . . . . . . . . . . . . 15  |-  ( E. t  e.  u  ( y  e.  w  /\  w  C_  t )  <->  ( y  e.  w  /\  E. t  e.  u  w  C_  t
) )
3332rexbii 2894 . . . . . . . . . . . . . 14  |-  ( E. w  e.  B  E. t  e.  u  (
y  e.  w  /\  w  C_  t )  <->  E. w  e.  B  ( y  e.  w  /\  E. t  e.  u  w  C_  t
) )
34 rexcom 2957 . . . . . . . . . . . . . 14  |-  ( E. w  e.  B  E. t  e.  u  (
y  e.  w  /\  w  C_  t )  <->  E. t  e.  u  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) )
3531, 33, 343bitr2i 273 . . . . . . . . . . . . 13  |-  ( y  e.  U. { w  e.  B  |  E. t  e.  u  w  C_  t }  <->  E. t  e.  u  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) )
3629, 30, 353imtr4g 270 . . . . . . . . . . . 12  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( y  e.  U. u  ->  y  e.  U. { w  e.  B  |  E. t  e.  u  w  C_  t } ) )
3736ssrdv 3436 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  U. u  C_  U. {
w  e.  B  |  E. t  e.  u  w  C_  t } )
3821, 37eqsstrd 3464 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  C_  U. { w  e.  B  |  E. t  e.  u  w  C_  t } )
39 ssrab2 3512 . . . . . . . . . . . 12  |-  { w  e.  B  |  E. t  e.  u  w  C_  t }  C_  B
4039unissi 4199 . . . . . . . . . . 11  |-  U. {
w  e.  B  |  E. t  e.  u  w  C_  t }  C_  U. B
41 simplr 753 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  =  U. B )
4240, 41syl5sseqr 3479 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  U. { w  e.  B  |  E. t  e.  u  w  C_  t }  C_  X )
4338, 42eqssd 3447 . . . . . . . . 9  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  =  U. { w  e.  B  |  E. t  e.  u  w  C_  t } )
44 elpw2g 4541 . . . . . . . . . . . 12  |-  ( B  e.  TopBases  ->  ( { w  e.  B  |  E. t  e.  u  w  C_  t }  e.  ~P B 
<->  { w  e.  B  |  E. t  e.  u  w  C_  t }  C_  B ) )
4544ad2antrr 723 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( { w  e.  B  |  E. t  e.  u  w  C_  t }  e.  ~P B  <->  { w  e.  B  |  E. t  e.  u  w  C_  t }  C_  B ) )
4639, 45mpbiri 233 . . . . . . . . . 10  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  { w  e.  B  |  E. t  e.  u  w  C_  t }  e.  ~P B )
47 unieq 4184 . . . . . . . . . . . . 13  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  U. y  =  U. { w  e.  B  |  E. t  e.  u  w  C_  t } )
4847eqeq2d 2406 . . . . . . . . . . . 12  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  ( X  = 
U. y  <->  X  =  U. { w  e.  B  |  E. t  e.  u  w  C_  t } ) )
49 pweq 3943 . . . . . . . . . . . . . 14  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  ~P y  =  ~P { w  e.  B  |  E. t  e.  u  w  C_  t } )
5049ineq1d 3626 . . . . . . . . . . . . 13  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  ( ~P y  i^i  Fin )  =  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) )
5150rexeqdv 2999 . . . . . . . . . . . 12  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  ( E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z  <->  E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z ) )
5248, 51imbi12d 318 . . . . . . . . . . 11  |-  ( y  =  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  ( ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  <->  ( X  = 
U. { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z ) ) )
5352rspcv 3144 . . . . . . . . . 10  |-  ( { w  e.  B  |  E. t  e.  u  w  C_  t }  e.  ~P B  ->  ( A. y  e.  ~P  B
( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z )  ->  ( X  =  U. { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z ) ) )
5446, 53syl 16 . . . . . . . . 9  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( A. y  e. 
~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  ( X  =  U. { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z ) ) )
5543, 54mpid 41 . . . . . . . 8  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( A. y  e. 
~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z ) )
56 elfpw 7755 . . . . . . . . . . . . 13  |-  ( z  e.  ( ~P {
w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  <->  ( z  C_  { w  e.  B  |  E. t  e.  u  w  C_  t }  /\  z  e.  Fin )
)
5756simprbi 462 . . . . . . . . . . . 12  |-  ( z  e.  ( ~P {
w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  ->  z  e.  Fin )
5857ad2antrl 725 . . . . . . . . . . 11  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  -> 
z  e.  Fin )
5956simplbi 458 . . . . . . . . . . . . 13  |-  ( z  e.  ( ~P {
w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  ->  z  C_  { w  e.  B  |  E. t  e.  u  w  C_  t } )
6059ad2antrl 725 . . . . . . . . . . . 12  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  -> 
z  C_  { w  e.  B  |  E. t  e.  u  w  C_  t } )
61 ssrab 3505 . . . . . . . . . . . . 13  |-  ( z 
C_  { w  e.  B  |  E. t  e.  u  w  C_  t } 
<->  ( z  C_  B  /\  A. w  e.  z  E. t  e.  u  w  C_  t ) )
6261simprbi 462 . . . . . . . . . . . 12  |-  ( z 
C_  { w  e.  B  |  E. t  e.  u  w  C_  t }  ->  A. w  e.  z  E. t  e.  u  w  C_  t )
6360, 62syl 16 . . . . . . . . . . 11  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  ->  A. w  e.  z  E. t  e.  u  w  C_  t )
64 sseq2 3452 . . . . . . . . . . . 12  |-  ( t  =  ( f `  w )  ->  (
w  C_  t  <->  w  C_  (
f `  w )
) )
6564ac6sfi 7697 . . . . . . . . . . 11  |-  ( ( z  e.  Fin  /\  A. w  e.  z  E. t  e.  u  w  C_  t )  ->  E. f
( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )
6658, 63, 65syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  ->  E. f ( f : z --> u  /\  A. w  e.  z  w  C_  ( f `  w
) ) )
67 frn 5658 . . . . . . . . . . . . 13  |-  ( f : z --> u  ->  ran  f  C_  u )
6867ad2antrl 725 . . . . . . . . . . . 12  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  ran  f  C_  u )
69 ffn 5652 . . . . . . . . . . . . . . 15  |-  ( f : z --> u  -> 
f  Fn  z )
70 dffn4 5722 . . . . . . . . . . . . . . 15  |-  ( f  Fn  z  <->  f :
z -onto-> ran  f )
7169, 70sylib 196 . . . . . . . . . . . . . 14  |-  ( f : z --> u  -> 
f : z -onto-> ran  f )
7271adantr 463 . . . . . . . . . . . . 13  |-  ( ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
)  ->  f :
z -onto-> ran  f )
73 fofi 7739 . . . . . . . . . . . . 13  |-  ( ( z  e.  Fin  /\  f : z -onto-> ran  f
)  ->  ran  f  e. 
Fin )
7458, 72, 73syl2an 475 . . . . . . . . . . . 12  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  ran  f  e.  Fin )
75 elfpw 7755 . . . . . . . . . . . 12  |-  ( ran  f  e.  ( ~P u  i^i  Fin )  <->  ( ran  f  C_  u  /\  ran  f  e.  Fin ) )
7668, 74, 75sylanbrc 662 . . . . . . . . . . 11  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  ran  f  e.  ( ~P u  i^i  Fin ) )
77 simplrr 760 . . . . . . . . . . . . 13  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  X  =  U. z )
78 uniiun 4309 . . . . . . . . . . . . . . . 16  |-  U. z  =  U_ w  e.  z  w
79 ss2iun 4272 . . . . . . . . . . . . . . . 16  |-  ( A. w  e.  z  w  C_  ( f `  w
)  ->  U_ w  e.  z  w  C_  U_ w  e.  z  ( f `  w ) )
8078, 79syl5eqss 3474 . . . . . . . . . . . . . . 15  |-  ( A. w  e.  z  w  C_  ( f `  w
)  ->  U. z  C_ 
U_ w  e.  z  ( f `  w
) )
8180ad2antll 726 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  U. z  C_ 
U_ w  e.  z  ( f `  w
) )
82 fniunfv 6076 . . . . . . . . . . . . . . . 16  |-  ( f  Fn  z  ->  U_ w  e.  z  ( f `  w )  =  U. ran  f )
8369, 82syl 16 . . . . . . . . . . . . . . 15  |-  ( f : z --> u  ->  U_ w  e.  z 
( f `  w
)  =  U. ran  f )
8483ad2antrl 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  U_ w  e.  z  ( f `  w )  =  U. ran  f )
8581, 84sseqtrd 3466 . . . . . . . . . . . . 13  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  U. z  C_ 
U. ran  f )
8677, 85eqsstrd 3464 . . . . . . . . . . . 12  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  X  C_ 
U. ran  f )
8768unissd 4200 . . . . . . . . . . . . 13  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  U. ran  f  C_  U. u )
8821ad2antrr 723 . . . . . . . . . . . . 13  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  X  =  U. u )
8987, 88sseqtr4d 3467 . . . . . . . . . . . 12  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  U. ran  f  C_  X )
9086, 89eqssd 3447 . . . . . . . . . . 11  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  X  =  U. ran  f )
91 unieq 4184 . . . . . . . . . . . . 13  |-  ( v  =  ran  f  ->  U. v  =  U. ran  f )
9291eqeq2d 2406 . . . . . . . . . . . 12  |-  ( v  =  ran  f  -> 
( X  =  U. v 
<->  X  =  U. ran  f ) )
9392rspcev 3148 . . . . . . . . . . 11  |-  ( ( ran  f  e.  ( ~P u  i^i  Fin )  /\  X  =  U. ran  f )  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v )
9476, 90, 93syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  /\  ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
) )  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v )
9566, 94exlimddv 1741 . . . . . . . . 9  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  ( z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  /\  X  =  U. z ) )  ->  E. v  e.  ( ~P u  i^i  Fin ) X  =  U. v
)
9695rexlimdvaa 2885 . . . . . . . 8  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( E. z  e.  ( ~P { w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin ) X  =  U. z  ->  E. v  e.  ( ~P u  i^i  Fin ) X  =  U. v ) )
9755, 96syld 44 . . . . . . 7  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  -> 
( A. y  e. 
~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) )
9897expr 613 . . . . . 6  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  u  C_  ( topGen `
 B ) )  ->  ( X  = 
U. u  ->  ( A. y  e.  ~P  B ( X  = 
U. y  ->  E. z  e.  ( ~P y  i^i 
Fin ) X  = 
U. z )  ->  E. v  e.  ( ~P u  i^i  Fin ) X  =  U. v
) ) )
9998com23 78 . . . . 5  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  u  C_  ( topGen `
 B ) )  ->  ( A. y  e.  ~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  ( X  =  U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) ) )
10020, 99sylan2 472 . . . 4  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  u  e.  ~P ( topGen `  B )
)  ->  ( A. y  e.  ~P  B
( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z )  ->  ( X  =  U. u  ->  E. v  e.  ( ~P u  i^i  Fin ) X  =  U. v ) ) )
101100ralrimdva 2810 . . 3  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. y  e. 
~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  A. u  e.  ~P  ( topGen `  B
) ( X  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) ) )
102 tgcl 19575 . . . . . 6  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )
103102adantr 463 . . . . 5  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( topGen `  B )  e.  Top )
1041iscmp 19993 . . . . . 6  |-  ( (
topGen `  B )  e. 
Comp 
<->  ( ( topGen `  B
)  e.  Top  /\  A. u  e.  ~P  ( topGen `
 B ) ( U. ( topGen `  B
)  =  U. u  ->  E. v  e.  ( ~P u  i^i  Fin ) U. ( topGen `  B
)  =  U. v
) ) )
105104baib 901 . . . . 5  |-  ( (
topGen `  B )  e. 
Top  ->  ( ( topGen `  B )  e.  Comp  <->  A. u  e.  ~P  ( topGen `
 B ) ( U. ( topGen `  B
)  =  U. u  ->  E. v  e.  ( ~P u  i^i  Fin ) U. ( topGen `  B
)  =  U. v
) ) )
106103, 105syl 16 . . . 4  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( topGen `  B
)  e.  Comp  <->  A. u  e.  ~P  ( topGen `  B
) ( U. ( topGen `
 B )  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) U. ( topGen `
 B )  = 
U. v ) ) )
1076eqeq1d 2394 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. u 
<->  X  =  U. u
) )
1086eqeq1d 2394 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. v 
<->  X  =  U. v
) )
109108rexbidv 2906 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( E. v  e.  ( ~P u  i^i 
Fin ) U. ( topGen `
 B )  = 
U. v  <->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) )
110107, 109imbi12d 318 . . . . 5  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( U. ( topGen `
 B )  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) U. ( topGen `
 B )  = 
U. v )  <->  ( X  =  U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) ) )
111110ralbidv 2831 . . . 4  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. u  e. 
~P  ( topGen `  B
) ( U. ( topGen `
 B )  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) U. ( topGen `
 B )  = 
U. v )  <->  A. u  e.  ~P  ( topGen `  B
) ( X  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) ) )
112106, 111bitrd 253 . . 3  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( topGen `  B
)  e.  Comp  <->  A. u  e.  ~P  ( topGen `  B
) ( X  = 
U. u  ->  E. v  e.  ( ~P u  i^i 
Fin ) X  = 
U. v ) ) )
113101, 112sylibrd 234 . 2  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( A. y  e. 
~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
)  ->  ( topGen `  B )  e.  Comp ) )
11419, 113impbid 191 1  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( ( topGen `  B
)  e.  Comp  <->  A. y  e.  ~P  B ( X  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) X  =  U. z
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399   E.wex 1627    e. wcel 1836   A.wral 2742   E.wrex 2743   {crab 2746    i^i cin 3401    C_ wss 3402   ~Pcpw 3940   U.cuni 4176   U_ciun 4256   ran crn 4927    Fn wfn 5504   -->wf 5505   -onto->wfo 5507   ` cfv 5509   Fincfn 7453   topGenctg 14864   Topctop 19498   TopBasesctb 19502   Compccmp 19991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-om 6618  df-1o 7066  df-er 7247  df-en 7454  df-dom 7455  df-fin 7457  df-topgen 14870  df-top 19503  df-bases 19505  df-cmp 19992
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator