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

Theorem fgcl 19576
Description: A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
fgcl  |-  ( F  e.  ( fBas `  X
)  ->  ( X filGen F )  e.  ( Fil `  X ) )

Proof of Theorem fgcl
Dummy variables  v  u  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfg 19569 . 2  |-  ( F  e.  ( fBas `  X
)  ->  ( z  e.  ( X filGen F )  <-> 
( z  C_  X  /\  E. y  e.  F  y  C_  z ) ) )
2 elfvex 5819 . 2  |-  ( F  e.  ( fBas `  X
)  ->  X  e.  _V )
3 fbasne0 19528 . . . . . 6  |-  ( F  e.  ( fBas `  X
)  ->  F  =/=  (/) )
4 n0 3747 . . . . . 6  |-  ( F  =/=  (/)  <->  E. y  y  e.  F )
53, 4sylib 196 . . . . 5  |-  ( F  e.  ( fBas `  X
)  ->  E. y 
y  e.  F )
6 fbelss 19531 . . . . . . . 8  |-  ( ( F  e.  ( fBas `  X )  /\  y  e.  F )  ->  y  C_  X )
76ex 434 . . . . . . 7  |-  ( F  e.  ( fBas `  X
)  ->  ( y  e.  F  ->  y  C_  X ) )
87ancld 553 . . . . . 6  |-  ( F  e.  ( fBas `  X
)  ->  ( y  e.  F  ->  ( y  e.  F  /\  y  C_  X ) ) )
98eximdv 1677 . . . . 5  |-  ( F  e.  ( fBas `  X
)  ->  ( E. y  y  e.  F  ->  E. y ( y  e.  F  /\  y  C_  X ) ) )
105, 9mpd 15 . . . 4  |-  ( F  e.  ( fBas `  X
)  ->  E. y
( y  e.  F  /\  y  C_  X ) )
11 df-rex 2801 . . . 4  |-  ( E. y  e.  F  y 
C_  X  <->  E. y
( y  e.  F  /\  y  C_  X ) )
1210, 11sylibr 212 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  E. y  e.  F  y  C_  X )
13 elfvdm 5818 . . . 4  |-  ( F  e.  ( fBas `  X
)  ->  X  e.  dom  fBas )
14 sseq2 3479 . . . . . 6  |-  ( z  =  X  ->  (
y  C_  z  <->  y  C_  X ) )
1514rexbidv 2855 . . . . 5  |-  ( z  =  X  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1615sbcieg 3320 . . . 4  |-  ( X  e.  dom  fBas  ->  (
[. X  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1713, 16syl 16 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  ( [. X  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1812, 17mpbird 232 . 2  |-  ( F  e.  ( fBas `  X
)  ->  [. X  / 
z ]. E. y  e.  F  y  C_  z
)
19 0nelfb 19529 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  -.  (/)  e.  F
)
20 0ex 4523 . . . . 5  |-  (/)  e.  _V
21 sseq2 3479 . . . . . 6  |-  ( z  =  (/)  ->  ( y 
C_  z  <->  y  C_  (/) ) )
2221rexbidv 2855 . . . . 5  |-  ( z  =  (/)  ->  ( E. y  e.  F  y 
C_  z  <->  E. y  e.  F  y  C_  (/) ) )
2320, 22sbcie 3322 . . . 4  |-  ( [. (/)  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  (/) )
24 ss0 3769 . . . . . . 7  |-  ( y 
C_  (/)  ->  y  =  (/) )
2524eleq1d 2520 . . . . . 6  |-  ( y 
C_  (/)  ->  ( y  e.  F  <->  (/)  e.  F ) )
2625biimpac 486 . . . . 5  |-  ( ( y  e.  F  /\  y  C_  (/) )  ->  (/)  e.  F
)
2726rexlimiva 2935 . . . 4  |-  ( E. y  e.  F  y 
C_  (/)  ->  (/)  e.  F
)
2823, 27sylbi 195 . . 3  |-  ( [. (/)  /  z ]. E. y  e.  F  y  C_  z  ->  (/)  e.  F
)
2919, 28nsyl 121 . 2  |-  ( F  e.  ( fBas `  X
)  ->  -.  [. (/)  /  z ]. E. y  e.  F  y  C_  z )
30 sstr 3465 . . . . . 6  |-  ( ( y  C_  v  /\  v  C_  u )  -> 
y  C_  u )
3130expcom 435 . . . . 5  |-  ( v 
C_  u  ->  (
y  C_  v  ->  y 
C_  u ) )
3231reximdv 2926 . . . 4  |-  ( v 
C_  u  ->  ( E. y  e.  F  y  C_  v  ->  E. y  e.  F  y  C_  u ) )
33323ad2ant3 1011 . . 3  |-  ( ( F  e.  ( fBas `  X )  /\  u  C_  X  /\  v  C_  u )  ->  ( E. y  e.  F  y  C_  v  ->  E. y  e.  F  y  C_  u ) )
34 vex 3074 . . . 4  |-  v  e. 
_V
35 sseq2 3479 . . . . 5  |-  ( z  =  v  ->  (
y  C_  z  <->  y  C_  v ) )
3635rexbidv 2855 . . . 4  |-  ( z  =  v  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  v ) )
3734, 36sbcie 3322 . . 3  |-  ( [. v  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  v )
38 vex 3074 . . . 4  |-  u  e. 
_V
39 sseq2 3479 . . . . 5  |-  ( z  =  u  ->  (
y  C_  z  <->  y  C_  u ) )
4039rexbidv 2855 . . . 4  |-  ( z  =  u  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  u ) )
4138, 40sbcie 3322 . . 3  |-  ( [. u  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  u )
4233, 37, 413imtr4g 270 . 2  |-  ( ( F  e.  ( fBas `  X )  /\  u  C_  X  /\  v  C_  u )  ->  ( [. v  /  z ]. E. y  e.  F  y  C_  z  ->  [. u  /  z ]. E. y  e.  F  y  C_  z ) )
43 fbasssin 19534 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( fBas `  X )  /\  z  e.  F  /\  w  e.  F )  ->  E. y  e.  F  y  C_  ( z  i^i  w
) )
44433expib 1191 . . . . . . . . . . . 12  |-  ( F  e.  ( fBas `  X
)  ->  ( (
z  e.  F  /\  w  e.  F )  ->  E. y  e.  F  y  C_  ( z  i^i  w ) ) )
45 ss2in 3678 . . . . . . . . . . . . . 14  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( z  i^i  w
)  C_  ( u  i^i  v ) )
46 sstr2 3464 . . . . . . . . . . . . . . . 16  |-  ( y 
C_  ( z  i^i  w )  ->  (
( z  i^i  w
)  C_  ( u  i^i  v )  ->  y  C_  ( u  i^i  v
) ) )
4746com12 31 . . . . . . . . . . . . . . 15  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
y  C_  ( z  i^i  w )  ->  y  C_  ( u  i^i  v
) ) )
4847reximdv 2926 . . . . . . . . . . . . . 14  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  ( E. y  e.  F  y  C_  ( z  i^i  w )  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) )
4945, 48syl 16 . . . . . . . . . . . . 13  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( E. y  e.  F  y  C_  (
z  i^i  w )  ->  E. y  e.  F  y  C_  ( u  i^i  v ) ) )
5049com12 31 . . . . . . . . . . . 12  |-  ( E. y  e.  F  y 
C_  ( z  i^i  w )  ->  (
( z  C_  u  /\  w  C_  v )  ->  E. y  e.  F  y  C_  ( u  i^i  v ) ) )
5144, 50syl6 33 . . . . . . . . . . 11  |-  ( F  e.  ( fBas `  X
)  ->  ( (
z  e.  F  /\  w  e.  F )  ->  ( ( z  C_  u  /\  w  C_  v
)  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) ) )
5251exp5c 616 . . . . . . . . . 10  |-  ( F  e.  ( fBas `  X
)  ->  ( z  e.  F  ->  ( w  e.  F  ->  (
z  C_  u  ->  ( w  C_  v  ->  E. y  e.  F  y 
C_  ( u  i^i  v ) ) ) ) ) )
5352imp31 432 . . . . . . . . 9  |-  ( ( ( F  e.  (
fBas `  X )  /\  z  e.  F
)  /\  w  e.  F )  ->  (
z  C_  u  ->  ( w  C_  v  ->  E. y  e.  F  y 
C_  ( u  i^i  v ) ) ) )
5453impancom 440 . . . . . . . 8  |-  ( ( ( F  e.  (
fBas `  X )  /\  z  e.  F
)  /\  z  C_  u )  ->  (
w  e.  F  -> 
( w  C_  v  ->  E. y  e.  F  y  C_  ( u  i^i  v ) ) ) )
5554rexlimdv 2939 . . . . . . 7  |-  ( ( ( F  e.  (
fBas `  X )  /\  z  e.  F
)  /\  z  C_  u )  ->  ( E. w  e.  F  w  C_  v  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) )
5655ex 434 . . . . . 6  |-  ( ( F  e.  ( fBas `  X )  /\  z  e.  F )  ->  (
z  C_  u  ->  ( E. w  e.  F  w  C_  v  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) ) )
5756rexlimdva 2940 . . . . 5  |-  ( F  e.  ( fBas `  X
)  ->  ( E. z  e.  F  z  C_  u  ->  ( E. w  e.  F  w  C_  v  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) ) )
5857impd 431 . . . 4  |-  ( F  e.  ( fBas `  X
)  ->  ( ( E. z  e.  F  z  C_  u  /\  E. w  e.  F  w  C_  v )  ->  E. y  e.  F  y  C_  ( u  i^i  v
) ) )
59583ad2ant1 1009 . . 3  |-  ( ( F  e.  ( fBas `  X )  /\  u  C_  X  /\  v  C_  X )  ->  (
( E. z  e.  F  z  C_  u  /\  E. w  e.  F  w  C_  v )  ->  E. y  e.  F  y  C_  ( u  i^i  v ) ) )
60 sseq1 3478 . . . . . 6  |-  ( y  =  z  ->  (
y  C_  u  <->  z  C_  u ) )
6160cbvrexv 3047 . . . . 5  |-  ( E. y  e.  F  y 
C_  u  <->  E. z  e.  F  z  C_  u )
6241, 61bitri 249 . . . 4  |-  ( [. u  /  z ]. E. y  e.  F  y  C_  z  <->  E. z  e.  F  z  C_  u )
63 sseq1 3478 . . . . . 6  |-  ( y  =  w  ->  (
y  C_  v  <->  w  C_  v
) )
6463cbvrexv 3047 . . . . 5  |-  ( E. y  e.  F  y 
C_  v  <->  E. w  e.  F  w  C_  v
)
6537, 64bitri 249 . . . 4  |-  ( [. v  /  z ]. E. y  e.  F  y  C_  z  <->  E. w  e.  F  w  C_  v )
6662, 65anbi12i 697 . . 3  |-  ( (
[. u  /  z ]. E. y  e.  F  y  C_  z  /\  [. v  /  z ]. E. y  e.  F  y  C_  z )  <->  ( E. z  e.  F  z  C_  u  /\  E. w  e.  F  w  C_  v
) )
6738inex1 4534 . . . 4  |-  ( u  i^i  v )  e. 
_V
68 sseq2 3479 . . . . 5  |-  ( z  =  ( u  i^i  v )  ->  (
y  C_  z  <->  y  C_  ( u  i^i  v
) ) )
6968rexbidv 2855 . . . 4  |-  ( z  =  ( u  i^i  v )  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  ( u  i^i  v
) ) )
7067, 69sbcie 3322 . . 3  |-  ( [. ( u  i^i  v
)  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  ( u  i^i  v
) )
7159, 66, 703imtr4g 270 . 2  |-  ( ( F  e.  ( fBas `  X )  /\  u  C_  X  /\  v  C_  X )  ->  (
( [. u  /  z ]. E. y  e.  F  y  C_  z  /\  [. v  /  z ]. E. y  e.  F  y  C_  z )  ->  [. (
u  i^i  v )  /  z ]. E. y  e.  F  y  C_  z ) )
721, 2, 18, 29, 42, 71isfild 19556 1  |-  ( F  e.  ( fBas `  X
)  ->  ( X filGen F )  e.  ( Fil `  X ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370   E.wex 1587    e. wcel 1758    =/= wne 2644   E.wrex 2796   [.wsbc 3287    i^i cin 3428    C_ wss 3429   (/)c0 3738   dom cdm 4941   ` cfv 5519  (class class class)co 6193   fBascfbas 17922   filGencfg 17923   Filcfil 19543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-fbas 17932  df-fg 17933  df-fil 19544
This theorem is referenced by:  fgabs  19577  trfg  19589  isufil2  19606  ssufl  19616  ufileu  19617  filufint  19618  fixufil  19620  uffixfr  19621  fmfil  19642  fmfg  19647  elfm3  19648  rnelfm  19651  fmfnfmlem2  19653  fmfnfm  19656  fbflim  19674  hausflim  19679  flimclslem  19682  flffbas  19693  fclsbas  19719  fclsfnflim  19725  flimfnfcls  19726  fclscmp  19728  haustsms  19831  tsmscls  19833  tsmsmhm  19845  tsmsadd  19846  cfilufg  19993  metustOLD  20267  metust  20268  fgcfil  20907  cmetcaulem  20924  cmetss  20950  minveclem4a  21042  minveclem4  21044
  Copyright terms: Public domain W3C validator