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

Theorem alexsublem 21071
Description: Lemma for alexsub 21072. (Contributed by Mario Carneiro, 26-Aug-2015.)
Hypotheses
Ref Expression
alexsub.1  |-  ( ph  ->  X  e. UFL )
alexsub.2  |-  ( ph  ->  X  =  U. B
)
alexsub.3  |-  ( ph  ->  J  =  ( topGen `  ( fi `  B
) ) )
alexsub.4  |-  ( (
ph  /\  ( x  C_  B  /\  X  = 
U. x ) )  ->  E. y  e.  ( ~P x  i^i  Fin ) X  =  U. y )
alexsub.5  |-  ( ph  ->  F  e.  ( UFil `  X ) )
alexsub.6  |-  ( ph  ->  ( J  fLim  F
)  =  (/) )
Assertion
Ref Expression
alexsublem  |-  -.  ph
Distinct variable groups:    x, y, B    x, J, y    ph, x, y    x, X, y    x, F, y

Proof of Theorem alexsublem
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 eldif 3416 . . . . . . . . . 10  |-  ( x  e.  ( X  \  U. ( B  \  F
) )  <->  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  =  ( topGen `  ( fi `  B
) ) )
32eleq2d 2516 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( y  e.  J  <->  y  e.  ( topGen `  ( fi `  B ) ) ) )
43anbi1d 712 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( y  e.  J  /\  x  e.  y )  <->  ( y  e.  ( topGen `  ( fi `  B ) )  /\  x  e.  y )
) )
54biimpa 487 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
( y  e.  (
topGen `  ( fi `  B ) )  /\  x  e.  y )
)
65adantlr 722 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
( y  e.  (
topGen `  ( fi `  B ) )  /\  x  e.  y )
)
7 tg2 19992 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( topGen `  ( fi `  B
) )  /\  x  e.  y )  ->  E. z  e.  ( fi `  B
) ( x  e.  z  /\  z  C_  y ) )
86, 7syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  ->  E. z  e.  ( fi `  B ) ( x  e.  z  /\  z  C_  y ) )
9 alexsub.5 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F  e.  ( UFil `  X ) )
10 ufilfil 20931 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  ( UFil `  X
)  ->  F  e.  ( Fil `  X ) )
119, 10syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e.  ( Fil `  X ) )
1211ad3antrrr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  J  /\  x  e.  y )
)  /\  ( z  e.  ( fi `  B
)  /\  ( x  e.  z  /\  z  C_  y ) ) )  ->  F  e.  ( Fil `  X ) )
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  X  =  U. B
)
149elfvexd 5898 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  X  e.  _V )
1513, 14eqeltrrd 2532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  e.  _V )
16 uniexb 6606 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  e.  _V  <->  U. B  e. 
_V )
1715, 16sylibr 216 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  _V )
18 elfi2 7933 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B  e.  _V  ->  (
z  e.  ( fi
`  B )  <->  E. y  e.  ( ( ~P B  i^i  Fin )  \  { (/)
} ) z  = 
|^| y ) )
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( fi `  B )  <->  E. y  e.  (
( ~P B  i^i  Fin )  \  { (/) } ) z  =  |^| y ) )
2019adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  ( z  e.  ( fi `  B
)  <->  E. y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } ) z  =  |^| y ) )
2111ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  F  e.  ( Fil `  X ) )
22 simplrr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y )  /\  z  e.  y ) )  ->  -.  x  e.  U. ( B  \  F ) )
23 intss1 4252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  y  ->  |^| y  C_  z )
2423adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  |^| y  C_  z
)
25 simplr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  |^| y
)
2624, 25sseldd 3435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  z )
2726ad2antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )
)  /\  -.  z  e.  F )  ->  x  e.  z )
28 eldifsn 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  <->  ( y  e.  ( ~P B  i^i  Fin )  /\  y  =/=  (/) ) )
2928simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  e.  ( ~P B  i^i  Fin )
)
3029ad2antrl 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  e.  ( ~P B  i^i  Fin ) )
31 elfpw 7881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ~P B  i^i  Fin )  <->  ( y  C_  B  /\  y  e. 
Fin ) )
3231simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  ( ~P B  i^i  Fin )  ->  y  C_  B )
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  C_  B )
3433sselda 3434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  /\  z  e.  y )  ->  z  e.  B )
3534anasss 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y )  /\  z  e.  y ) )  -> 
z  e.  B )
3635anim1i 572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )
)  /\  -.  z  e.  F )  ->  (
z  e.  B  /\  -.  z  e.  F
) )
37 eldif 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  ( B  \  F )  <->  ( z  e.  B  /\  -.  z  e.  F ) )
3836, 37sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )
)  /\  -.  z  e.  F )  ->  z  e.  ( B  \  F
) )
39 elunii 4206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  z  /\  z  e.  ( B  \  F ) )  ->  x  e.  U. ( B  \  F ) )
4027, 38, 39syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )
)  /\  -.  z  e.  F )  ->  x  e.  U. ( B  \  F ) )
4140ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y )  /\  z  e.  y ) )  -> 
( -.  z  e.  F  ->  x  e.  U. ( B  \  F
) ) )
4222, 41mt3d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y )  /\  z  e.  y ) )  -> 
z  e.  F )
4342expr 620 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  ( z  e.  y  ->  z  e.  F ) )
4443ssrdv 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  C_  F )
4528simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  =/=  (/) )
4645ad2antrl 735 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  =/=  (/) )
4731simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ~P B  i^i  Fin )  ->  y  e.  Fin )
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  e.  Fin )
49 elfir 7934 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  ( Fil `  X )  /\  (
y  C_  F  /\  y  =/=  (/)  /\  y  e. 
Fin ) )  ->  |^| y  e.  ( fi `  F ) )
5021, 44, 46, 48, 49syl13anc 1271 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  |^| y  e.  ( fi `  F
) )
51 filfi 20886 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F  e.  ( Fil `  X
)  ->  ( fi `  F )  =  F )
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  ( fi `  F )  =  F )
5350, 52eleqtrd 2533 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  |^| y  e.  F )
5453expr 620 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  y  e.  ( ( ~P B  i^i  Fin )  \  { (/)
} ) )  -> 
( x  e.  |^| y  ->  |^| y  e.  F
) )
55 eleq2 2520 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( x  e.  z  <-> 
x  e.  |^| y
) )
56 eleq1 2519 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( z  e.  F  <->  |^| y  e.  F ) )
5755, 56imbi12d 322 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  |^| y  -> 
( ( x  e.  z  ->  z  e.  F )  <->  ( x  e.  |^| y  ->  |^| y  e.  F ) ) )
5854, 57syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  y  e.  ( ( ~P B  i^i  Fin )  \  { (/)
} ) )  -> 
( z  =  |^| y  ->  ( x  e.  z  ->  z  e.  F ) ) )
5958rexlimdva 2881 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  ( E. y  e.  ( ( ~P B  i^i  Fin )  \  { (/)
} ) z  = 
|^| y  ->  (
x  e.  z  -> 
z  e.  F ) ) )
6020, 59sylbid 219 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  ( z  e.  ( fi `  B
)  ->  ( x  e.  z  ->  z  e.  F ) ) )
6160imp32 435 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  x  e.  z ) )  -> 
z  e.  F )
6261adantrrr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  (
x  e.  z  /\  z  C_  y ) ) )  ->  z  e.  F )
6362adantlr 722 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  J  /\  x  e.  y )
)  /\  ( z  e.  ( fi `  B
)  /\  ( x  e.  z  /\  z  C_  y ) ) )  ->  z  e.  F
)
64 elssuni 4230 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  J  ->  y  C_ 
U. J )
6564ad2antrl 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  U. J )
66 fibas 20005 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( fi
`  B )  e.  TopBases
67 tgtopon 19999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( fi `  B )  e.  TopBases  ->  ( topGen `  ( fi `  B ) )  e.  (TopOn `  U. ( fi `  B ) ) )
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen `  ( fi `  B
) )  e.  (TopOn `  U. ( fi `  B ) )
692, 68syl6eqel 2539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  J  e.  (TopOn `  U. ( fi `  B
) ) )
70 fiuni 7947 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  e.  _V  ->  U. B  =  U. ( fi `  B ) )
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  =  U. ( fi `  B ) )
7213, 71eqtrd 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  =  U. ( fi `  B ) )
7372fveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  (TopOn `  X )  =  (TopOn `  U. ( fi
`  B ) ) )
7469, 73eleqtrrd 2534 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  e.  (TopOn `  X ) )
75 toponuni 19954 . . . . . . . . . . . . . . . . . . . 20  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  =  U. J
)
7776ad2antrr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  ->  X  =  U. J )
7865, 77sseqtr4d 3471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  X )
7978adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  J  /\  x  e.  y )
)  /\  ( z  e.  ( fi `  B
)  /\  ( x  e.  z  /\  z  C_  y ) ) )  ->  y  C_  X
)
80 simprrr 776 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  J  /\  x  e.  y )
)  /\  ( z  e.  ( fi `  B
)  /\  ( x  e.  z  /\  z  C_  y ) ) )  ->  z  C_  y
)
81 filss 20880 . . . . . . . . . . . . . . . 16  |-  ( ( F  e.  ( Fil `  X )  /\  (
z  e.  F  /\  y  C_  X  /\  z  C_  y ) )  -> 
y  e.  F )
8212, 63, 79, 80, 81syl13anc 1271 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  (
y  e.  J  /\  x  e.  y )
)  /\  ( z  e.  ( fi `  B
)  /\  ( x  e.  z  /\  z  C_  y ) ) )  ->  y  e.  F
)
838, 82rexlimddv 2885 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  e.  F )
8483expr 620 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  y  e.  J )  ->  (
x  e.  y  -> 
y  e.  F ) )
8584ralrimiva 2804 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) )
8685expr 620 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  X )  ->  ( -.  x  e.  U. ( B  \  F )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) )
8786imdistanda 700 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) )  -> 
( x  e.  X  /\  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) ) )
881, 87syl5bi 221 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) ) )
89 flimopn 21002 . . . . . . . . . 10  |-  ( ( J  e.  (TopOn `  X )  /\  F  e.  ( Fil `  X
) )  ->  (
x  e.  ( J 
fLim  F )  <->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) ) )
9074, 11, 89syl2anc 667 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( J  fLim  F )  <->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  -> 
y  e.  F ) ) ) )
9188, 90sylibrd 238 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  x  e.  ( J  fLim  F )
) )
9291ssrdv 3440 . . . . . . 7  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F ) )
93 alexsub.6 . . . . . . 7  |-  ( ph  ->  ( J  fLim  F
)  =  (/) )
94 sseq0 3768 . . . . . . 7  |-  ( ( ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F )  /\  ( J  fLim  F )  =  (/) )  ->  ( X 
\  U. ( B  \  F ) )  =  (/) )
9592, 93, 94syl2anc 667 . . . . . 6  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  =  (/) )
96 ssdif0 3825 . . . . . 6  |-  ( X 
C_  U. ( B  \  F )  <->  ( X  \ 
U. ( B  \  F ) )  =  (/) )
9795, 96sylibr 216 . . . . 5  |-  ( ph  ->  X  C_  U. ( B  \  F ) )
98 difss 3562 . . . . . . 7  |-  ( B 
\  F )  C_  B
9998unissi 4224 . . . . . 6  |-  U. ( B  \  F )  C_  U. B
10099, 13syl5sseqr 3483 . . . . 5  |-  ( ph  ->  U. ( B  \  F )  C_  X
)
10197, 100eqssd 3451 . . . 4  |-  ( ph  ->  X  =  U. ( B  \  F ) )
102101, 98jctil 540 . . 3  |-  ( ph  ->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )
103 difexg 4554 . . . . . 6  |-  ( B  e.  _V  ->  ( B  \  F )  e. 
_V )
10417, 103syl 17 . . . . 5  |-  ( ph  ->  ( B  \  F
)  e.  _V )
105104adantr 467 . . . 4  |-  ( (
ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  ( B  \  F )  e. 
_V )
106 sseq1 3455 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  (
x  C_  B  <->  ( B  \  F )  C_  B
) )
107 unieq 4209 . . . . . . . . 9  |-  ( x  =  ( B  \  F )  ->  U. x  =  U. ( B  \  F ) )
108107eqeq2d 2463 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ( X  =  U. x  <->  X  =  U. ( B 
\  F ) ) )
109106, 108anbi12d 718 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  (
( x  C_  B  /\  X  =  U. x )  <->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) )
110109anbi2d 711 . . . . . 6  |-  ( x  =  ( B  \  F )  ->  (
( ph  /\  (
x  C_  B  /\  X  =  U. x
) )  <->  ( ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) ) )
111 pweq 3956 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ~P x  =  ~P ( B  \  F ) )
112111ineq1d 3635 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  ( ~P x  i^i  Fin )  =  ( ~P ( B  \  F )  i^i 
Fin ) )
113112rexeqdv 2996 . . . . . 6  |-  ( x  =  ( B  \  F )  ->  ( E. y  e.  ( ~P x  i^i  Fin ) X  =  U. y  <->  E. y  e.  ( ~P ( B  \  F
)  i^i  Fin ) X  =  U. y
) )
114110, 113imbi12d 322 . . . . 5  |-  ( x  =  ( B  \  F )  ->  (
( ( ph  /\  ( x  C_  B  /\  X  =  U. x
) )  ->  E. y  e.  ( ~P x  i^i 
Fin ) X  = 
U. y )  <->  ( ( ph  /\  ( ( B 
\  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y ) ) )
115 alexsub.4 . . . . 5  |-  ( (
ph  /\  ( x  C_  B  /\  X  = 
U. x ) )  ->  E. y  e.  ( ~P x  i^i  Fin ) X  =  U. y )
116114, 115vtoclg 3109 . . . 4  |-  ( ( B  \  F )  e.  _V  ->  (
( ph  /\  (
( B  \  F
)  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y ) )
117105, 116mpcom 37 . . 3  |-  ( (
ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y )
118102, 117mpdan 675 . 2  |-  ( ph  ->  E. y  e.  ( ~P ( B  \  F )  i^i  Fin ) X  =  U. y )
119 unieq 4209 . . . . . . 7  |-  ( y  =  (/)  ->  U. y  =  U. (/) )
120 uni0 4228 . . . . . . 7  |-  U. (/)  =  (/)
121119, 120syl6eq 2503 . . . . . 6  |-  ( y  =  (/)  ->  U. y  =  (/) )
122121neeq2d 2686 . . . . 5  |-  ( y  =  (/)  ->  ( X  =/=  U. y  <->  X  =/=  (/) ) )
123 difssd 3563 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  ( X  \  z )  C_  X )
124123ralrimivw 2805 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  A. z  e.  y  ( X  \  z )  C_  X
)
125 riinn0 4356 . . . . . . . . . 10  |-  ( ( A. z  e.  y  ( X  \  z
)  C_  X  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =  |^|_ z  e.  y  ( X  \  z ) )
126124, 125sylan 474 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =  |^|_ z  e.  y  ( X  \  z ) )
12714ad2antrr 733 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  e.  _V )
128 difexg 4554 . . . . . . . . . . . . 13  |-  ( X  e.  _V  ->  ( X  \  z )  e. 
_V )
129127, 128syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  \  z )  e. 
_V )
130129ralrimivw 2805 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  A. z  e.  y  ( X  \  z )  e.  _V )
131 dfiin2g 4314 . . . . . . . . . . 11  |-  ( A. z  e.  y  ( X  \  z )  e. 
_V  ->  |^|_ z  e.  y  ( X  \  z
)  =  |^| { x  |  E. z  e.  y  x  =  ( X 
\  z ) } )
132130, 131syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^|_ z  e.  y  ( X  \  z )  =  |^| { x  |  E. z  e.  y  x  =  ( X  \  z
) } )
133 eqid 2453 . . . . . . . . . . . 12  |-  ( z  e.  y  |->  ( X 
\  z ) )  =  ( z  e.  y  |->  ( X  \ 
z ) )
134133rnmpt 5083 . . . . . . . . . . 11  |-  ran  (
z  e.  y  |->  ( X  \  z ) )  =  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }
135134inteqi 4241 . . . . . . . . . 10  |-  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =  |^| { x  |  E. z  e.  y  x  =  ( X  \  z
) }
136132, 135syl6eqr 2505 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^|_ z  e.  y  ( X  \  z )  =  |^| ran  ( z  e.  y 
|->  ( X  \  z
) ) )
137126, 136eqtrd 2487 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =  |^| ran  ( z  e.  y 
|->  ( X  \  z
) ) )
13811ad2antrr 733 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  F  e.  ( Fil `  X
) )
139 elfpw 7881 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  <->  ( y  C_  ( B  \  F
)  /\  y  e.  Fin ) )
140139simplbi 462 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  C_  ( B  \  F
) )
141140ad2antlr 734 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  ( B  \  F
) )
142141sselda 3434 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  ( B 
\  F ) )
143142eldifbd 3419 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  -.  z  e.  F
)
1449ad3antrrr 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  F  e.  ( UFil `  X ) )
145141difss2d 3565 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  B )
146145sselda 3434 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  B )
147 elssuni 4230 . . . . . . . . . . . . . . 15  |-  ( z  e.  B  ->  z  C_ 
U. B )
148146, 147syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  C_  U. B )
14913ad3antrrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  X  =  U. B
)
150148, 149sseqtr4d 3471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  C_  X )
151 ufilb 20933 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( UFil `  X )  /\  z  C_  X )  ->  ( -.  z  e.  F  <->  ( X  \  z )  e.  F ) )
152144, 150, 151syl2anc 667 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( -.  z  e.  F  <->  ( X  \ 
z )  e.  F
) )
153143, 152mpbid 214 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  z
)  e.  F )
154153, 133fmptd 6051 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  (
z  e.  y  |->  ( X  \  z ) ) : y --> F )
155 frn 5740 . . . . . . . . . 10  |-  ( ( z  e.  y  |->  ( X  \  z ) ) : y --> F  ->  ran  ( z  e.  y  |->  ( X 
\  z ) ) 
C_  F )
156154, 155syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  C_  F
)
157133, 153dmmptd 5713 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =  y )
158 simpr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  =/=  (/) )
159157, 158eqnetrd 2693 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
160 dm0rn0 5054 . . . . . . . . . . 11  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =  (/)  <->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =  (/) )
161160necon3bii 2678 . . . . . . . . . 10  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/)  <->  ran  ( z  e.  y  |->  ( X 
\  z ) )  =/=  (/) )
162159, 161sylib 200 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
163139simprbi 466 . . . . . . . . . . 11  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  e.  Fin )
164163ad2antlr 734 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  e.  Fin )
165 abrexfi 7879 . . . . . . . . . . 11  |-  ( y  e.  Fin  ->  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }  e.  Fin )
166134, 165syl5eqel 2535 . . . . . . . . . 10  |-  ( y  e.  Fin  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  e.  Fin )
167164, 166syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  e.  Fin )
168 filintn0 20888 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  X )  /\  ( ran  ( z  e.  y 
|->  ( X  \  z
) )  C_  F  /\  ran  ( z  e.  y  |->  ( X  \ 
z ) )  =/=  (/)  /\  ran  ( z  e.  y  |->  ( X 
\  z ) )  e.  Fin ) )  ->  |^| ran  ( z  e.  y  |->  ( X 
\  z ) )  =/=  (/) )
169138, 156, 162, 167, 168syl13anc 1271 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
170137, 169eqnetrd 2693 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =/=  (/) )
171 disj3 3811 . . . . . . . 8  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =  (/) 
<->  X  =  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
172171necon3bii 2678 . . . . . . 7  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =/=  (/) 
<->  X  =/=  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
173170, 172sylib 200 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  ( X  \  |^|_ z  e.  y  ( X  \  z ) ) )
174 iundif2 4348 . . . . . . 7  |-  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  ( X  \  |^|_ z  e.  y  ( X  \  z ) )
175 dfss4 3679 . . . . . . . . . 10  |-  ( z 
C_  X  <->  ( X  \  ( X  \  z
) )  =  z )
176150, 175sylib 200 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  ( X  \  z ) )  =  z )
177176iuneq2dv 4303 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  U_ z  e.  y  z
)
178 uniiun 4334 . . . . . . . 8  |-  U. y  =  U_ z  e.  y  z
179177, 178syl6eqr 2505 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  U. y )
180174, 179syl5eqr 2501 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  \  |^|_ z  e.  y  ( X  \  z
) )  =  U. y )
181173, 180neeqtrd 2695 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  U. y )
18211adantr 467 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  F  e.  ( Fil `  X
) )
183 filtop 20882 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
184 fileln0 20877 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  X  =/=  (/) )
185183, 184mpdan 675 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  =/=  (/) )
186182, 185syl 17 . . . . 5  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  (/) )
187122, 181, 186pm2.61ne 2711 . . . 4  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  U. y )
188187neneqd 2631 . . 3  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  -.  X  =  U. y
)
189188nrexdv 2845 . 2  |-  ( ph  ->  -.  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y )
190118, 189pm2.65i 177 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446    e. wcel 1889   {cab 2439    =/= wne 2624   A.wral 2739   E.wrex 2740   _Vcvv 3047    \ cdif 3403    i^i cin 3405    C_ wss 3406   (/)c0 3733   ~Pcpw 3953   {csn 3970   U.cuni 4201   |^|cint 4237   U_ciun 4281   |^|_ciin 4282    |-> cmpt 4464   dom cdm 4837   ran crn 4838   -->wf 5581   ` cfv 5585  (class class class)co 6295   Fincfn 7574   ficfi 7929   topGenctg 15348  TopOnctopon 19930   TopBasesctb 19932   Filcfil 20872   UFilcufil 20926  UFLcufl 20927    fLim cflim 20961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-iin 4284  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-fin 7578  df-fi 7930  df-topgen 15354  df-fbas 18979  df-top 19933  df-bases 19934  df-topon 19935  df-ntr 20047  df-nei 20126  df-fil 20873  df-ufil 20928  df-flim 20966
This theorem is referenced by:  alexsub  21072
  Copyright terms: Public domain W3C validator