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

Theorem alexsublem 20629
Description: Lemma for alexsub 20630. (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 3399 . . . . . . . . . 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 2452 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( y  e.  J  <->  y  e.  ( topGen `  ( fi `  B ) ) ) )
43anbi1d 702 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( y  e.  J  /\  x  e.  y )  <->  ( y  e.  ( topGen `  ( fi `  B ) )  /\  x  e.  y )
) )
54biimpa 482 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
( y  e.  (
topGen `  ( fi `  B ) )  /\  x  e.  y )
)
65adantlr 712 . . . . . . . . . . . . . . . 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 19551 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( topGen `  ( fi `  B
) )  /\  x  e.  y )  ->  E. z  e.  ( fi `  B
) ( x  e.  z  /\  z  C_  y ) )
86, 7syl 16 . . . . . . . . . . . . . . 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 20490 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  ( UFil `  X
)  ->  F  e.  ( Fil `  X ) )
119, 10syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e.  ( Fil `  X ) )
1211ad3antrrr 727 . . . . . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  X  e.  _V )
1513, 14eqeltrrd 2471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  e.  _V )
16 uniexb 6509 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  e.  _V  <->  U. B  e. 
_V )
1715, 16sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  _V )
18 elfi2 7789 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B  e.  _V  ->  (
z  e.  ( fi
`  B )  <->  E. y  e.  ( ( ~P B  i^i  Fin )  \  { (/)
} ) z  = 
|^| y ) )
1917, 18syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( fi `  B )  <->  E. y  e.  (
( ~P B  i^i  Fin )  \  { (/) } ) z  =  |^| y ) )
2019adantr 463 . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  y  ->  |^| y  C_  z )
2423adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  |^| y  C_  z
)
25 simplr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  |^| y
)
2624, 25sseldd 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  z )
2726ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  <->  ( y  e.  ( ~P B  i^i  Fin )  /\  y  =/=  (/) ) )
2928simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  e.  ( ~P B  i^i  Fin )
)
3029ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ~P B  i^i  Fin )  <->  ( y  C_  B  /\  y  e. 
Fin ) )
3231simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  ( ~P B  i^i  Fin )  ->  y  C_  B )
3330, 32syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  C_  B )
3433sselda 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  ( B  \  F )  <->  ( z  e.  B  /\  -.  z  e.  F ) )
3836, 37sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  z  /\  z  e.  ( B  \  F ) )  ->  x  e.  U. ( B  \  F ) )
4027, 38, 39syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 125 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  C_  F )
4528simprbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  =/=  (/) )
4645ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  =/=  (/) )
4731simprbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ~P B  i^i  Fin )  ->  y  e.  Fin )
4830, 47syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 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 7790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  ( Fil `  X )  /\  (
y  C_  F  /\  y  =/=  (/)  /\  y  e. 
Fin ) )  ->  |^| y  e.  ( fi `  F ) )
5021, 44, 46, 48, 49syl13anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 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 20445 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F  e.  ( Fil `  X
)  ->  ( fi `  F )  =  F )
5221, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  |^| y  e.  F )
5453expr 613 . . . . . . . . . . . . . . . . . . . . . 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 2455 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( x  e.  z  <-> 
x  e.  |^| y
) )
56 eleq1 2454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( z  e.  F  <->  |^| y  e.  F ) )
5755, 56imbi12d 318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  |^| y  -> 
( ( x  e.  z  ->  z  e.  F )  <->  ( x  e.  |^| y  ->  |^| y  e.  F ) ) )
5854, 57syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . 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 2874 . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  ( z  e.  ( fi `  B
)  ->  ( x  e.  z  ->  z  e.  F ) ) )
6160imp32 431 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  x  e.  z ) )  -> 
z  e.  F )
6261adantrrr 722 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  (
x  e.  z  /\  z  C_  y ) ) )  ->  z  e.  F )
6362adantlr 712 . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  J  ->  y  C_ 
U. J )
6564ad2antrl 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  U. J )
66 fibas 19564 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( fi
`  B )  e.  TopBases
67 tgtopon 19558 . . . . . . . . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  J  e.  (TopOn `  U. ( fi `  B
) ) )
70 fiuni 7803 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  e.  _V  ->  U. B  =  U. ( fi `  B ) )
7117, 70syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  =  U. ( fi `  B ) )
7213, 71eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  =  U. ( fi `  B ) )
7372fveq2d 5778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  (TopOn `  X )  =  (TopOn `  U. ( fi
`  B ) ) )
7469, 73eleqtrrd 2473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  e.  (TopOn `  X ) )
75 toponuni 19513 . . . . . . . . . . . . . . . . . . . 20  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
7674, 75syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  =  U. J
)
7776ad2antrr 723 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  ->  X  =  U. J )
7865, 77sseqtr4d 3454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  X )
7978adantr 463 . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . 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 20439 . . . . . . . . . . . . . . . 16  |-  ( ( F  e.  ( Fil `  X )  /\  (
z  e.  F  /\  y  C_  X  /\  z  C_  y ) )  -> 
y  e.  F )
8212, 63, 79, 80, 81syl13anc 1228 . . . . . . . . . . . . . . 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 2878 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  e.  F )
8483expr 613 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  y  e.  J )  ->  (
x  e.  y  -> 
y  e.  F ) )
8584ralrimiva 2796 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) )
8685expr 613 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  X )  ->  ( -.  x  e.  U. ( B  \  F )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) )
8786imdistanda 691 . . . . . . . . . 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 217 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) ) )
89 flimopn 20561 . . . . . . . . . 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 659 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( J  fLim  F )  <->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  -> 
y  e.  F ) ) ) )
9188, 90sylibrd 234 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  x  e.  ( J  fLim  F )
) )
9291ssrdv 3423 . . . . . . 7  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F ) )
93 alexsub.6 . . . . . . 7  |-  ( ph  ->  ( J  fLim  F
)  =  (/) )
94 sseq0 3744 . . . . . . 7  |-  ( ( ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F )  /\  ( J  fLim  F )  =  (/) )  ->  ( X 
\  U. ( B  \  F ) )  =  (/) )
9592, 93, 94syl2anc 659 . . . . . 6  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  =  (/) )
96 ssdif0 3801 . . . . . 6  |-  ( X 
C_  U. ( B  \  F )  <->  ( X  \ 
U. ( B  \  F ) )  =  (/) )
9795, 96sylibr 212 . . . . 5  |-  ( ph  ->  X  C_  U. ( B  \  F ) )
98 difss 3545 . . . . . . 7  |-  ( B 
\  F )  C_  B
9998unissi 4186 . . . . . 6  |-  U. ( B  \  F )  C_  U. B
10099, 13syl5sseqr 3466 . . . . 5  |-  ( ph  ->  U. ( B  \  F )  C_  X
)
10197, 100eqssd 3434 . . . 4  |-  ( ph  ->  X  =  U. ( B  \  F ) )
102101, 98jctil 535 . . 3  |-  ( ph  ->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )
103 difexg 4513 . . . . . 6  |-  ( B  e.  _V  ->  ( B  \  F )  e. 
_V )
10417, 103syl 16 . . . . 5  |-  ( ph  ->  ( B  \  F
)  e.  _V )
105104adantr 463 . . . 4  |-  ( (
ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  ( B  \  F )  e. 
_V )
106 sseq1 3438 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  (
x  C_  B  <->  ( B  \  F )  C_  B
) )
107 unieq 4171 . . . . . . . . 9  |-  ( x  =  ( B  \  F )  ->  U. x  =  U. ( B  \  F ) )
108107eqeq2d 2396 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ( X  =  U. x  <->  X  =  U. ( B 
\  F ) ) )
109106, 108anbi12d 708 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  (
( x  C_  B  /\  X  =  U. x )  <->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) )
110109anbi2d 701 . . . . . 6  |-  ( x  =  ( B  \  F )  ->  (
( ph  /\  (
x  C_  B  /\  X  =  U. x
) )  <->  ( ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) ) )
111 pweq 3930 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ~P x  =  ~P ( B  \  F ) )
112111ineq1d 3613 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  ( ~P x  i^i  Fin )  =  ( ~P ( B  \  F )  i^i 
Fin ) )
113112rexeqdv 2986 . . . . . 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 318 . . . . 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 3092 . . . 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 36 . . 3  |-  ( (
ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y )
118102, 117mpdan 666 . 2  |-  ( ph  ->  E. y  e.  ( ~P ( B  \  F )  i^i  Fin ) X  =  U. y )
119 unieq 4171 . . . . . . 7  |-  ( y  =  (/)  ->  U. y  =  U. (/) )
120 uni0 4190 . . . . . . 7  |-  U. (/)  =  (/)
121119, 120syl6eq 2439 . . . . . 6  |-  ( y  =  (/)  ->  U. y  =  (/) )
122121neeq2d 2660 . . . . 5  |-  ( y  =  (/)  ->  ( X  =/=  U. y  <->  X  =/=  (/) ) )
123 difssd 3546 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  ( X  \  z )  C_  X )
124123ralrimivw 2797 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  A. z  e.  y  ( X  \  z )  C_  X
)
125 riinn0 4318 . . . . . . . . . 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 469 . . . . . . . . 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 723 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  e.  _V )
128 difexg 4513 . . . . . . . . . . . . 13  |-  ( X  e.  _V  ->  ( X  \  z )  e. 
_V )
129127, 128syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  \  z )  e. 
_V )
130129ralrimivw 2797 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  A. z  e.  y  ( X  \  z )  e.  _V )
131 dfiin2g 4276 . . . . . . . . . . 11  |-  ( A. z  e.  y  ( X  \  z )  e. 
_V  ->  |^|_ z  e.  y  ( X  \  z
)  =  |^| { x  |  E. z  e.  y  x  =  ( X 
\  z ) } )
132130, 131syl 16 . . . . . . . . . 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 2382 . . . . . . . . . . . 12  |-  ( z  e.  y  |->  ( X 
\  z ) )  =  ( z  e.  y  |->  ( X  \ 
z ) )
134133rnmpt 5161 . . . . . . . . . . 11  |-  ran  (
z  e.  y  |->  ( X  \  z ) )  =  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }
135134inteqi 4203 . . . . . . . . . 10  |-  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =  |^| { x  |  E. z  e.  y  x  =  ( X  \  z
) }
136132, 135syl6eqr 2441 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^|_ z  e.  y  ( X  \  z )  =  |^| ran  ( z  e.  y 
|->  ( X  \  z
) ) )
137126, 136eqtrd 2423 . . . . . . . 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 723 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  F  e.  ( Fil `  X
) )
139 elfpw 7737 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  <->  ( y  C_  ( B  \  F
)  /\  y  e.  Fin ) )
140139simplbi 458 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  C_  ( B  \  F
) )
141140ad2antlr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  ( B  \  F
) )
142141sselda 3417 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  ( B 
\  F ) )
143142eldifbd 3402 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  -.  z  e.  F
)
1449ad3antrrr 727 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  F  e.  ( UFil `  X ) )
145141difss2d 3548 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  B )
146145sselda 3417 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  B )
147 elssuni 4192 . . . . . . . . . . . . . . 15  |-  ( z  e.  B  ->  z  C_ 
U. B )
148146, 147syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  C_  U. B )
14913ad3antrrr 727 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  X  =  U. B
)
150148, 149sseqtr4d 3454 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  C_  X )
151 ufilb 20492 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( UFil `  X )  /\  z  C_  X )  ->  ( -.  z  e.  F  <->  ( X  \  z )  e.  F ) )
152144, 150, 151syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( -.  z  e.  F  <->  ( X  \ 
z )  e.  F
) )
153143, 152mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  z
)  e.  F )
154153, 133fmptd 5957 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  (
z  e.  y  |->  ( X  \  z ) ) : y --> F )
155 frn 5645 . . . . . . . . . 10  |-  ( ( z  e.  y  |->  ( X  \  z ) ) : y --> F  ->  ran  ( z  e.  y  |->  ( X 
\  z ) ) 
C_  F )
156154, 155syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  C_  F
)
157133, 153dmmptd 5619 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =  y )
158 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  =/=  (/) )
159157, 158eqnetrd 2675 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
160 dm0rn0 5132 . . . . . . . . . . 11  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =  (/)  <->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =  (/) )
161160necon3bii 2650 . . . . . . . . . 10  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/)  <->  ran  ( z  e.  y  |->  ( X 
\  z ) )  =/=  (/) )
162159, 161sylib 196 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
163139simprbi 462 . . . . . . . . . . 11  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  e.  Fin )
164163ad2antlr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  e.  Fin )
165 abrexfi 7735 . . . . . . . . . . 11  |-  ( y  e.  Fin  ->  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }  e.  Fin )
166134, 165syl5eqel 2474 . . . . . . . . . 10  |-  ( y  e.  Fin  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  e.  Fin )
167164, 166syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  e.  Fin )
168 filintn0 20447 . . . . . . . . 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 1228 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
170137, 169eqnetrd 2675 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =/=  (/) )
171 disj3 3787 . . . . . . . 8  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =  (/) 
<->  X  =  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
172171necon3bii 2650 . . . . . . 7  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =/=  (/) 
<->  X  =/=  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
173170, 172sylib 196 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  ( X  \  |^|_ z  e.  y  ( X  \  z ) ) )
174 iundif2 4310 . . . . . . 7  |-  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  ( X  \  |^|_ z  e.  y  ( X  \  z ) )
175 dfss4 3657 . . . . . . . . . 10  |-  ( z 
C_  X  <->  ( X  \  ( X  \  z
) )  =  z )
176150, 175sylib 196 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  ( X  \  z ) )  =  z )
177176iuneq2dv 4265 . . . . . . . 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 4296 . . . . . . . 8  |-  U. y  =  U_ z  e.  y  z
179177, 178syl6eqr 2441 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  U. y )
180174, 179syl5eqr 2437 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  \  |^|_ z  e.  y  ( X  \  z
) )  =  U. y )
181173, 180neeqtrd 2677 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  U. y )
18211adantr 463 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  F  e.  ( Fil `  X
) )
183 filtop 20441 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
184 fileln0 20436 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  X  =/=  (/) )
185183, 184mpdan 666 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  =/=  (/) )
186182, 185syl 16 . . . . 5  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  (/) )
187122, 181, 186pm2.61ne 2697 . . . 4  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  U. y )
188187neneqd 2584 . . 3  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  -.  X  =  U. y
)
189188nrexdv 2838 . 2  |-  ( ph  ->  -.  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y )
190118, 189pm2.65i 173 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826   {cab 2367    =/= wne 2577   A.wral 2732   E.wrex 2733   _Vcvv 3034    \ cdif 3386    i^i cin 3388    C_ wss 3389   (/)c0 3711   ~Pcpw 3927   {csn 3944   U.cuni 4163   |^|cint 4199   U_ciun 4243   |^|_ciin 4244    |-> cmpt 4425   dom cdm 4913   ran crn 4914   -->wf 5492   ` cfv 5496  (class class class)co 6196   Fincfn 7435   ficfi 7785   topGenctg 14845  TopOnctopon 19480   TopBasesctb 19483   Filcfil 20431   UFilcufil 20485  UFLcufl 20486    fLim cflim 20520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
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 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-1o 7048  df-oadd 7052  df-er 7229  df-en 7436  df-dom 7437  df-fin 7439  df-fi 7786  df-topgen 14851  df-fbas 18529  df-top 19484  df-bases 19486  df-topon 19487  df-ntr 19606  df-nei 19685  df-fil 20432  df-ufil 20487  df-flim 20525
This theorem is referenced by:  alexsub  20630
  Copyright terms: Public domain W3C validator