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

Theorem alexsublem 21137
Description: Lemma for alexsub 21138. (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 3400 . . . . . . . . . 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 2534 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( y  e.  J  <->  y  e.  ( topGen `  ( fi `  B ) ) ) )
43anbi1d 719 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( y  e.  J  /\  x  e.  y )  <->  ( y  e.  ( topGen `  ( fi `  B ) )  /\  x  e.  y )
) )
54biimpa 492 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
( y  e.  (
topGen `  ( fi `  B ) )  /\  x  e.  y )
)
65adantlr 729 . . . . . . . . . . . . . . . 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 20057 . . . . . . . . . . . . . . . 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 20997 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  ( UFil `  X
)  ->  F  e.  ( Fil `  X ) )
119, 10syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e.  ( Fil `  X ) )
1211ad3antrrr 744 . . . . . . . . . . . . . . . 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 5907 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  X  e.  _V )
1513, 14eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  e.  _V )
16 uniexb 6620 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  e.  _V  <->  U. B  e. 
_V )
1715, 16sylibr 217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  _V )
18 elfi2 7946 . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  y  ->  |^| y  C_  z )
2423adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  |^| y  C_  z
)
25 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  |^| y
)
2624, 25sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e. 
|^| y )  /\  z  e.  y )  ->  x  e.  z )
2726ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  <->  ( y  e.  ( ~P B  i^i  Fin )  /\  y  =/=  (/) ) )
2928simplbi 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  e.  ( ~P B  i^i  Fin )
)
3029ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ~P B  i^i  Fin )  <->  ( y  C_  B  /\  y  e. 
Fin ) )
3231simplbi 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  ( B  \  F )  <->  ( z  e.  B  /\  -.  z  e.  F ) )
3836, 37sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  z  /\  z  e.  ( B  \  F ) )  ->  x  e.  U. ( B  \  F ) )
4027, 38, 39syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 130 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 626 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  C_  F )
4528simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  -> 
y  =/=  (/) )
4645ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  y  =/=  (/) )
4731simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7947 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F  e.  ( Fil `  X )  /\  (
y  C_  F  /\  y  =/=  (/)  /\  y  e. 
Fin ) )  ->  |^| y  e.  ( fi `  F ) )
5021, 44, 46, 48, 49syl13anc 1294 . . . . . . . . . . . . . . . . . . . . . . . 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 20952 . . . . . . . . . . . . . . . . . . . . . . . . 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 2551 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  ( ( ~P B  i^i  Fin )  \  { (/) } )  /\  x  e.  |^| y ) )  ->  |^| y  e.  F )
5453expr 626 . . . . . . . . . . . . . . . . . . . . . 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 2538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( x  e.  z  <-> 
x  e.  |^| y
) )
56 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  |^| y  -> 
( z  e.  F  <->  |^| y  e.  F ) )
5755, 56imbi12d 327 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  |^| y  -> 
( ( x  e.  z  ->  z  e.  F )  <->  ( x  e.  |^| y  ->  |^| y  e.  F ) ) )
5854, 57syl5ibrcom 230 . . . . . . . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  ( z  e.  ( fi `  B
)  ->  ( x  e.  z  ->  z  e.  F ) ) )
6160imp32 440 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  x  e.  z ) )  -> 
z  e.  F )
6261adantrrr 739 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( z  e.  ( fi `  B )  /\  (
x  e.  z  /\  z  C_  y ) ) )  ->  z  e.  F )
6362adantlr 729 . . . . . . . . . . . . . . . 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 4219 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  J  ->  y  C_ 
U. J )
6564ad2antrl 742 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  U. J )
66 fibas 20070 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( fi
`  B )  e.  TopBases
67 tgtopon 20064 . . . . . . . . . . . . . . . . . . . . . . 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 2557 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  J  e.  (TopOn `  U. ( fi `  B
) ) )
70 fiuni 7960 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  e.  _V  ->  U. B  =  U. ( fi `  B ) )
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  U. B  =  U. ( fi `  B ) )
7213, 71eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  =  U. ( fi `  B ) )
7372fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  (TopOn `  X )  =  (TopOn `  U. ( fi
`  B ) ) )
7469, 73eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  e.  (TopOn `  X ) )
75 toponuni 20019 . . . . . . . . . . . . . . . . . . . 20  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  =  U. J
)
7776ad2antrr 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  ->  X  =  U. J )
7865, 77sseqtr4d 3455 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  C_  X )
7978adantr 472 . . . . . . . . . . . . . . . 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 783 . . . . . . . . . . . . . . . 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 20946 . . . . . . . . . . . . . . . 16  |-  ( ( F  e.  ( Fil `  X )  /\  (
z  e.  F  /\  y  C_  X  /\  z  C_  y ) )  -> 
y  e.  F )
8212, 63, 79, 80, 81syl13anc 1294 . . . . . . . . . . . . . . 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 2875 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  ( y  e.  J  /\  x  e.  y ) )  -> 
y  e.  F )
8483expr 626 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  /\  y  e.  J )  ->  (
x  e.  y  -> 
y  e.  F ) )
8584ralrimiva 2809 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  X  /\  -.  x  e.  U. ( B  \  F ) ) )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) )
8685expr 626 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  X )  ->  ( -.  x  e.  U. ( B  \  F )  ->  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) )
8786imdistanda 707 . . . . . . . . . 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 225 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  ->  y  e.  F ) ) ) )
89 flimopn 21068 . . . . . . . . . 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 673 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( J  fLim  F )  <->  ( x  e.  X  /\  A. y  e.  J  ( x  e.  y  -> 
y  e.  F ) ) ) )
9188, 90sylibrd 242 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( X  \  U. ( B  \  F ) )  ->  x  e.  ( J  fLim  F )
) )
9291ssrdv 3424 . . . . . . 7  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F ) )
93 alexsub.6 . . . . . . 7  |-  ( ph  ->  ( J  fLim  F
)  =  (/) )
94 sseq0 3769 . . . . . . 7  |-  ( ( ( X  \  U. ( B  \  F ) )  C_  ( J  fLim  F )  /\  ( J  fLim  F )  =  (/) )  ->  ( X 
\  U. ( B  \  F ) )  =  (/) )
9592, 93, 94syl2anc 673 . . . . . 6  |-  ( ph  ->  ( X  \  U. ( B  \  F ) )  =  (/) )
96 ssdif0 3741 . . . . . 6  |-  ( X 
C_  U. ( B  \  F )  <->  ( X  \ 
U. ( B  \  F ) )  =  (/) )
9795, 96sylibr 217 . . . . 5  |-  ( ph  ->  X  C_  U. ( B  \  F ) )
98 difss 3549 . . . . . . 7  |-  ( B 
\  F )  C_  B
9998unissi 4213 . . . . . 6  |-  U. ( B  \  F )  C_  U. B
10099, 13syl5sseqr 3467 . . . . 5  |-  ( ph  ->  U. ( B  \  F )  C_  X
)
10197, 100eqssd 3435 . . . 4  |-  ( ph  ->  X  =  U. ( B  \  F ) )
102101, 98jctil 546 . . 3  |-  ( ph  ->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )
103 difexg 4545 . . . . . 6  |-  ( B  e.  _V  ->  ( B  \  F )  e. 
_V )
10417, 103syl 17 . . . . 5  |-  ( ph  ->  ( B  \  F
)  e.  _V )
105104adantr 472 . . . 4  |-  ( (
ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) )  ->  ( B  \  F )  e. 
_V )
106 sseq1 3439 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  (
x  C_  B  <->  ( B  \  F )  C_  B
) )
107 unieq 4198 . . . . . . . . 9  |-  ( x  =  ( B  \  F )  ->  U. x  =  U. ( B  \  F ) )
108107eqeq2d 2481 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ( X  =  U. x  <->  X  =  U. ( B 
\  F ) ) )
109106, 108anbi12d 725 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  (
( x  C_  B  /\  X  =  U. x )  <->  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) )
110109anbi2d 718 . . . . . 6  |-  ( x  =  ( B  \  F )  ->  (
( ph  /\  (
x  C_  B  /\  X  =  U. x
) )  <->  ( ph  /\  ( ( B  \  F )  C_  B  /\  X  =  U. ( B  \  F ) ) ) ) )
111 pweq 3945 . . . . . . . 8  |-  ( x  =  ( B  \  F )  ->  ~P x  =  ~P ( B  \  F ) )
112111ineq1d 3624 . . . . . . 7  |-  ( x  =  ( B  \  F )  ->  ( ~P x  i^i  Fin )  =  ( ~P ( B  \  F )  i^i 
Fin ) )
113112rexeqdv 2980 . . . . . 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 327 . . . . 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 3093 . . . 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 681 . 2  |-  ( ph  ->  E. y  e.  ( ~P ( B  \  F )  i^i  Fin ) X  =  U. y )
119 unieq 4198 . . . . . . 7  |-  ( y  =  (/)  ->  U. y  =  U. (/) )
120 uni0 4217 . . . . . . 7  |-  U. (/)  =  (/)
121119, 120syl6eq 2521 . . . . . 6  |-  ( y  =  (/)  ->  U. y  =  (/) )
122121neeq2d 2703 . . . . 5  |-  ( y  =  (/)  ->  ( X  =/=  U. y  <->  X  =/=  (/) ) )
123 difssd 3550 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  ( X  \  z )  C_  X )
124123ralrimivw 2810 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  A. z  e.  y  ( X  \  z )  C_  X
)
125 riinn0 4344 . . . . . . . . . 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 479 . . . . . . . . 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 740 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  e.  _V )
128 difexg 4545 . . . . . . . . . . . . 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 2810 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  A. z  e.  y  ( X  \  z )  e.  _V )
131 dfiin2g 4302 . . . . . . . . . . 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 2471 . . . . . . . . . . . 12  |-  ( z  e.  y  |->  ( X 
\  z ) )  =  ( z  e.  y  |->  ( X  \ 
z ) )
134133rnmpt 5086 . . . . . . . . . . 11  |-  ran  (
z  e.  y  |->  ( X  \  z ) )  =  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }
135134inteqi 4230 . . . . . . . . . 10  |-  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =  |^| { x  |  E. z  e.  y  x  =  ( X  \  z
) }
136132, 135syl6eqr 2523 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^|_ z  e.  y  ( X  \  z )  =  |^| ran  ( z  e.  y 
|->  ( X  \  z
) ) )
137126, 136eqtrd 2505 . . . . . . . 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 740 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  F  e.  ( Fil `  X
) )
139 elfpw 7894 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  <->  ( y  C_  ( B  \  F
)  /\  y  e.  Fin ) )
140139simplbi 467 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  C_  ( B  \  F
) )
141140ad2antlr 741 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  ( B  \  F
) )
142141sselda 3418 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  ( B 
\  F ) )
143142eldifbd 3403 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  -.  z  e.  F
)
1449ad3antrrr 744 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  F  e.  ( UFil `  X ) )
145141difss2d 3552 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  C_  B )
146145sselda 3418 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  e.  B )
147 elssuni 4219 . . . . . . . . . . . . . . 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 744 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  X  =  U. B
)
150148, 149sseqtr4d 3455 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  z  C_  X )
151 ufilb 20999 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( UFil `  X )  /\  z  C_  X )  ->  ( -.  z  e.  F  <->  ( X  \  z )  e.  F ) )
152144, 150, 151syl2anc 673 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( -.  z  e.  F  <->  ( X  \ 
z )  e.  F
) )
153143, 152mpbid 215 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  z
)  e.  F )
154153, 133fmptd 6061 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  (
z  e.  y  |->  ( X  \  z ) ) : y --> F )
155 frn 5747 . . . . . . . . . 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 5718 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =  y )
158 simpr 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  =/=  (/) )
159157, 158eqnetrd 2710 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
160 dm0rn0 5057 . . . . . . . . . . 11  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =  (/)  <->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =  (/) )
161160necon3bii 2695 . . . . . . . . . 10  |-  ( dom  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/)  <->  ran  ( z  e.  y  |->  ( X 
\  z ) )  =/=  (/) )
162159, 161sylib 201 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
163139simprbi 471 . . . . . . . . . . 11  |-  ( y  e.  ( ~P ( B  \  F )  i^i 
Fin )  ->  y  e.  Fin )
164163ad2antlr 741 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  y  e.  Fin )
165 abrexfi 7892 . . . . . . . . . . 11  |-  ( y  e.  Fin  ->  { x  |  E. z  e.  y  x  =  ( X 
\  z ) }  e.  Fin )
166134, 165syl5eqel 2553 . . . . . . . . . 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 20954 . . . . . . . . 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 1294 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  |^| ran  ( z  e.  y 
|->  ( X  \  z
) )  =/=  (/) )
170137, 169eqnetrd 2710 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  i^i  |^|_ z  e.  y  ( X  \  z
) )  =/=  (/) )
171 disj3 3813 . . . . . . . 8  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =  (/) 
<->  X  =  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
172171necon3bii 2695 . . . . . . 7  |-  ( ( X  i^i  |^|_ z  e.  y  ( X  \  z ) )  =/=  (/) 
<->  X  =/=  ( X 
\  |^|_ z  e.  y  ( X  \  z
) ) )
173170, 172sylib 201 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  ( X  \  |^|_ z  e.  y  ( X  \  z ) ) )
174 iundif2 4336 . . . . . . 7  |-  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  ( X  \  |^|_ z  e.  y  ( X  \  z ) )
175 dfss4 3668 . . . . . . . . . 10  |-  ( z 
C_  X  <->  ( X  \  ( X  \  z
) )  =  z )
176150, 175sylib 201 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  /\  y  =/=  (/) )  /\  z  e.  y )  ->  ( X  \  ( X  \  z ) )  =  z )
177176iuneq2dv 4291 . . . . . . . 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 4322 . . . . . . . 8  |-  U. y  =  U_ z  e.  y  z
179177, 178syl6eqr 2523 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  U_ z  e.  y  ( X  \  ( X  \  z
) )  =  U. y )
180174, 179syl5eqr 2519 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  ( X  \  |^|_ z  e.  y  ( X  \  z
) )  =  U. y )
181173, 180neeqtrd 2712 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) )  /\  y  =/=  (/) )  ->  X  =/=  U. y )
18211adantr 472 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  F  e.  ( Fil `  X
) )
183 filtop 20948 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
184 fileln0 20943 . . . . . . 7  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  X  =/=  (/) )
185183, 184mpdan 681 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  =/=  (/) )
186182, 185syl 17 . . . . 5  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  (/) )
187122, 181, 186pm2.61ne 2728 . . . 4  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  X  =/=  U. y )
188187neneqd 2648 . . 3  |-  ( (
ph  /\  y  e.  ( ~P ( B  \  F )  i^i  Fin ) )  ->  -.  X  =  U. y
)
189188nrexdv 2842 . 2  |-  ( ph  ->  -.  E. y  e.  ( ~P ( B 
\  F )  i^i 
Fin ) X  = 
U. y )
190118, 189pm2.65i 178 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   {cab 2457    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031    \ cdif 3387    i^i cin 3389    C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   U.cuni 4190   |^|cint 4226   U_ciun 4269   |^|_ciin 4270    |-> cmpt 4454   dom cdm 4839   ran crn 4840   -->wf 5585   ` cfv 5589  (class class class)co 6308   Fincfn 7587   ficfi 7942   topGenctg 15414  TopOnctopon 19995   TopBasesctb 19997   Filcfil 20938   UFilcufil 20992  UFLcufl 20993    fLim cflim 21027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-dom 7589  df-fin 7591  df-fi 7943  df-topgen 15420  df-fbas 19044  df-top 19998  df-bases 19999  df-topon 20000  df-ntr 20112  df-nei 20191  df-fil 20939  df-ufil 20994  df-flim 21032
This theorem is referenced by:  alexsub  21138
  Copyright terms: Public domain W3C validator