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

Theorem tgcmp 19771
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 20415, 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 2441 . . . . 5  |-  U. ( topGen `
 B )  = 
U. ( topGen `  B
)
21iscmp 19758 . . . 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 464 . . 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 19338 . . . . . . . 8  |-  ( B  e.  TopBases  ->  U. ( topGen `  B
)  =  U. B
)
5 eqtr3 2469 . . . . . . . 8  |-  ( ( U. ( topGen `  B
)  =  U. B  /\  X  =  U. B )  ->  U. ( topGen `
 B )  =  X )
64, 5sylan 471 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  ->  U. ( topGen `  B )  =  X )
76eqeq1d 2443 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. y 
<->  X  =  U. y
) )
86eqeq1d 2443 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. z 
<->  X  =  U. z
) )
98rexbidv 2952 . . . . . 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 320 . . . . 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 2880 . . . 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 19337 . . . . . . 7  |-  ( B  e.  TopBases  ->  B  C_  ( topGen `
 B ) )
1312adantr 465 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  ->  B  C_  ( topGen `  B
) )
14 sspwb 4683 . . . . . 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 3547 . . . . 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 4003 . . . . 5  |-  ( u  e.  ~P ( topGen `  B )  ->  u  C_  ( topGen `  B )
)
21 simprr 756 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  =  U. u
)
22 simprl 755 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  u  C_  ( topGen `  B
) )
2322sselda 3487 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( B  e.  TopBases 
/\  X  =  U. B )  /\  (
u  C_  ( topGen `  B )  /\  X  =  U. u ) )  /\  t  e.  u
)  ->  t  e.  ( topGen `  B )
)
2423adantrr 716 . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . 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 19336 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  ( topGen `  B )  /\  y  e.  t )  ->  E. w  e.  B  ( y  e.  w  /\  w  C_  t ) )
2724, 25, 26syl2anc 661 . . . . . . . . . . . . . . 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 615 . . . . . . . . . . . . . 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 2916 . . . . . . . . . . . . 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 4235 . . . . . . . . . . . . 13  |-  ( y  e.  U. u  <->  E. t  e.  u  y  e.  t )
31 elunirab 4243 . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . . 15  |-  ( E. t  e.  u  ( y  e.  w  /\  w  C_  t )  <->  ( y  e.  w  /\  E. t  e.  u  w  C_  t
) )
3332rexbii 2943 . . . . . . . . . . . . . 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 3003 . . . . . . . . . . . . . 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 3493 . . . . . . . . . . 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 3521 . . . . . . . . . 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 3568 . . . . . . . . . . . 12  |-  { w  e.  B  |  E. t  e.  u  w  C_  t }  C_  B
4039unissi 4254 . . . . . . . . . . 11  |-  U. {
w  e.  B  |  E. t  e.  u  w  C_  t }  C_  U. B
41 simplr 754 . . . . . . . . . . 11  |-  ( ( ( B  e.  TopBases  /\  X  =  U. B )  /\  ( u  C_  ( topGen `  B )  /\  X  =  U. u ) )  ->  X  =  U. B )
4240, 41syl5sseqr 3536 . . . . . . . . . 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 3504 . . . . . . . . 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 4597 . . . . . . . . . . . 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 725 . . . . . . . . . . 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 4239 . . . . . . . . . . . . 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 2455 . . . . . . . . . . . 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 3997 . . . . . . . . . . . . . 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 3682 . . . . . . . . . . . . 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 3045 . . . . . . . . . . . 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 320 . . . . . . . . . . 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 3190 . . . . . . . . . 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 7821 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 12  |-  ( z  e.  ( ~P {
w  e.  B  |  E. t  e.  u  w  C_  t }  i^i  Fin )  ->  z  e.  Fin )
5857ad2antrl 727 . . . . . . . . . . 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 460 . . . . . . . . . . . . 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 727 . . . . . . . . . . . 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 3561 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 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 3509 . . . . . . . . . . . 12  |-  ( t  =  ( f `  w )  ->  (
w  C_  t  <->  w  C_  (
f `  w )
) )
6564ac6sfi 7763 . . . . . . . . . . 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 661 . . . . . . . . . 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 5724 . . . . . . . . . . . . 13  |-  ( f : z --> u  ->  ran  f  C_  u )
6867ad2antrl 727 . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . 15  |-  ( f : z --> u  -> 
f  Fn  z )
70 dffn4 5788 . . . . . . . . . . . . . . 15  |-  ( f  Fn  z  <->  f :
z -onto-> ran  f )
7169, 70sylib 196 . . . . . . . . . . . . . 14  |-  ( f : z --> u  -> 
f : z -onto-> ran  f )
7271adantr 465 . . . . . . . . . . . . 13  |-  ( ( f : z --> u  /\  A. w  e.  z  w  C_  (
f `  w )
)  ->  f :
z -onto-> ran  f )
73 fofi 7805 . . . . . . . . . . . . 13  |-  ( ( z  e.  Fin  /\  f : z -onto-> ran  f
)  ->  ran  f  e. 
Fin )
7458, 72, 73syl2an 477 . . . . . . . . . . . 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 7821 . . . . . . . . . . . 12  |-  ( ran  f  e.  ( ~P u  i^i  Fin )  <->  ( ran  f  C_  u  /\  ran  f  e.  Fin ) )
7668, 74, 75sylanbrc 664 . . . . . . . . . . 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 4365 . . . . . . . . . . . . . . . 16  |-  U. z  =  U_ w  e.  z  w
79 ss2iun 4328 . . . . . . . . . . . . . . . 16  |-  ( A. w  e.  z  w  C_  ( f `  w
)  ->  U_ w  e.  z  w  C_  U_ w  e.  z  ( f `  w ) )
8078, 79syl5eqss 3531 . . . . . . . . . . . . . . 15  |-  ( A. w  e.  z  w  C_  ( f `  w
)  ->  U. z  C_ 
U_ w  e.  z  ( f `  w
) )
8180ad2antll 728 . . . . . . . . . . . . . 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 6141 . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . 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 3523 . . . . . . . . . . . . 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 3521 . . . . . . . . . . . 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 4255 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . 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 3524 . . . . . . . . . . . 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 3504 . . . . . . . . . . 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 4239 . . . . . . . . . . . . 13  |-  ( v  =  ran  f  ->  U. v  =  U. ran  f )
9291eqeq2d 2455 . . . . . . . . . . . 12  |-  ( v  =  ran  f  -> 
( X  =  U. v 
<->  X  =  U. ran  f ) )
9392rspcev 3194 . . . . . . . . . . 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 661 . . . . . . . . . 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 1711 . . . . . . . . 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 2934 . . . . . . . 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 615 . . . . . 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 474 . . . 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 2859 . . 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 19341 . . . . . 6  |-  ( B  e.  TopBases  ->  ( topGen `  B
)  e.  Top )
103102adantr 465 . . . . 5  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( topGen `  B )  e.  Top )
1041iscmp 19758 . . . . . 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 2443 . . . . . 6  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. u 
<->  X  =  U. u
) )
1086eqeq1d 2443 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  X  =  U. B )  -> 
( U. ( topGen `  B )  =  U. v 
<->  X  =  U. v
) )
109108rexbidv 2952 . . . . . 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 320 . . . . 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 2880 . . . 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 369    = wceq 1381   E.wex 1597    e. wcel 1802   A.wral 2791   E.wrex 2792   {crab 2795    i^i cin 3458    C_ wss 3459   ~Pcpw 3994   U.cuni 4231   U_ciun 4312   ran crn 4987    Fn wfn 5570   -->wf 5571   -onto->wfo 5573   ` cfv 5575   Fincfn 7515   topGenctg 14709   Topctop 19264   TopBasesctb 19268   Compccmp 19756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-uni 4232  df-iun 4314  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-om 6683  df-1o 7129  df-er 7310  df-en 7516  df-dom 7517  df-fin 7519  df-topgen 14715  df-top 19269  df-bases 19271  df-cmp 19757
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator