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

Theorem fgcl 20942
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 20935 . 2  |-  ( F  e.  ( fBas `  X
)  ->  ( z  e.  ( X filGen F )  <-> 
( z  C_  X  /\  E. y  e.  F  y  C_  z ) ) )
2 elfvex 5915 . 2  |-  ( F  e.  ( fBas `  X
)  ->  X  e.  _V )
3 fbasne0 20894 . . . . . 6  |-  ( F  e.  ( fBas `  X
)  ->  F  =/=  (/) )
4 n0 3753 . . . . . 6  |-  ( F  =/=  (/)  <->  E. y  y  e.  F )
53, 4sylib 201 . . . . 5  |-  ( F  e.  ( fBas `  X
)  ->  E. y 
y  e.  F )
6 fbelss 20897 . . . . . . . 8  |-  ( ( F  e.  ( fBas `  X )  /\  y  e.  F )  ->  y  C_  X )
76ex 440 . . . . . . 7  |-  ( F  e.  ( fBas `  X
)  ->  ( y  e.  F  ->  y  C_  X ) )
87ancld 560 . . . . . 6  |-  ( F  e.  ( fBas `  X
)  ->  ( y  e.  F  ->  ( y  e.  F  /\  y  C_  X ) ) )
98eximdv 1775 . . . . 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 2755 . . . 4  |-  ( E. y  e.  F  y 
C_  X  <->  E. y
( y  e.  F  /\  y  C_  X ) )
1210, 11sylibr 217 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  E. y  e.  F  y  C_  X )
13 elfvdm 5914 . . . 4  |-  ( F  e.  ( fBas `  X
)  ->  X  e.  dom  fBas )
14 sseq2 3466 . . . . . 6  |-  ( z  =  X  ->  (
y  C_  z  <->  y  C_  X ) )
1514rexbidv 2913 . . . . 5  |-  ( z  =  X  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1615sbcieg 3312 . . . 4  |-  ( X  e.  dom  fBas  ->  (
[. X  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1713, 16syl 17 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  ( [. X  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  X ) )
1812, 17mpbird 240 . 2  |-  ( F  e.  ( fBas `  X
)  ->  [. X  / 
z ]. E. y  e.  F  y  C_  z
)
19 0nelfb 20895 . . 3  |-  ( F  e.  ( fBas `  X
)  ->  -.  (/)  e.  F
)
20 0ex 4549 . . . . 5  |-  (/)  e.  _V
21 sseq2 3466 . . . . . 6  |-  ( z  =  (/)  ->  ( y 
C_  z  <->  y  C_  (/) ) )
2221rexbidv 2913 . . . . 5  |-  ( z  =  (/)  ->  ( E. y  e.  F  y 
C_  z  <->  E. y  e.  F  y  C_  (/) ) )
2320, 22sbcie 3314 . . . 4  |-  ( [. (/)  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  (/) )
24 ss0 3777 . . . . . . 7  |-  ( y 
C_  (/)  ->  y  =  (/) )
2524eleq1d 2524 . . . . . 6  |-  ( y 
C_  (/)  ->  ( y  e.  F  <->  (/)  e.  F ) )
2625biimpac 493 . . . . 5  |-  ( ( y  e.  F  /\  y  C_  (/) )  ->  (/)  e.  F
)
2726rexlimiva 2887 . . . 4  |-  ( E. y  e.  F  y 
C_  (/)  ->  (/)  e.  F
)
2823, 27sylbi 200 . . 3  |-  ( [. (/)  /  z ]. E. y  e.  F  y  C_  z  ->  (/)  e.  F
)
2919, 28nsyl 126 . 2  |-  ( F  e.  ( fBas `  X
)  ->  -.  [. (/)  /  z ]. E. y  e.  F  y  C_  z )
30 sstr 3452 . . . . . 6  |-  ( ( y  C_  v  /\  v  C_  u )  -> 
y  C_  u )
3130expcom 441 . . . . 5  |-  ( v 
C_  u  ->  (
y  C_  v  ->  y 
C_  u ) )
3231reximdv 2873 . . . 4  |-  ( v 
C_  u  ->  ( E. y  e.  F  y  C_  v  ->  E. y  e.  F  y  C_  u ) )
33323ad2ant3 1037 . . 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 3060 . . . 4  |-  v  e. 
_V
35 sseq2 3466 . . . . 5  |-  ( z  =  v  ->  (
y  C_  z  <->  y  C_  v ) )
3635rexbidv 2913 . . . 4  |-  ( z  =  v  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  v ) )
3734, 36sbcie 3314 . . 3  |-  ( [. v  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  v )
38 vex 3060 . . . 4  |-  u  e. 
_V
39 sseq2 3466 . . . . 5  |-  ( z  =  u  ->  (
y  C_  z  <->  y  C_  u ) )
4039rexbidv 2913 . . . 4  |-  ( z  =  u  ->  ( E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  u ) )
4138, 40sbcie 3314 . . 3  |-  ( [. u  /  z ]. E. y  e.  F  y  C_  z  <->  E. y  e.  F  y  C_  u )
4233, 37, 413imtr4g 278 . 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 20900 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( fBas `  X )  /\  z  e.  F  /\  w  e.  F )  ->  E. y  e.  F  y  C_  ( z  i^i  w
) )
44433expib 1218 . . . . . . . . . . . 12  |-  ( F  e.  ( fBas `  X
)  ->  ( (
z  e.  F  /\  w  e.  F )  ->  E. y  e.  F  y  C_  ( z  i^i  w ) ) )
45 ss2in 3671 . . . . . . . . . . . . . 14  |-  ( ( z  C_  u  /\  w  C_  v )  -> 
( z  i^i  w
)  C_  ( u  i^i  v ) )
46 sstr2 3451 . . . . . . . . . . . . . . . 16  |-  ( y 
C_  ( z  i^i  w )  ->  (
( z  i^i  w
)  C_  ( u  i^i  v )  ->  y  C_  ( u  i^i  v
) ) )
4746com12 32 . . . . . . . . . . . . . . 15  |-  ( ( z  i^i  w ) 
C_  ( u  i^i  v )  ->  (
y  C_  ( z  i^i  w )  ->  y  C_  ( u  i^i  v
) ) )
4847reximdv 2873 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 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 32 . . . . . . . . . . . 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 34 . . . . . . . . . . 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 625 . . . . . . . . . 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 438 . . . . . . . . 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 446 . . . . . . . 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 2889 . . . . . . 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 440 . . . . . 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 2891 . . . . 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 437 . . . 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 1035 . . 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 3465 . . . . . 6  |-  ( y  =  z  ->  (
y  C_  u  <->  z  C_  u ) )
6160cbvrexv 3032 . . . . 5  |-  ( E. y  e.  F  y 
C_  u  <->  E. z  e.  F  z  C_  u )
6241, 61bitri 257 . . . 4  |-  ( [. u  /  z ]. E. y  e.  F  y  C_  z  <->  E. z  e.  F  z  C_  u )
63 sseq1 3465 . . . . . 6  |-  ( y  =  w  ->  (
y  C_  v  <->  w  C_  v
) )
6463cbvrexv 3032 . . . . 5  |-  ( E. y  e.  F  y 
C_  v  <->  E. w  e.  F  w  C_  v
)
6537, 64bitri 257 . . . 4  |-  ( [. v  /  z ]. E. y  e.  F  y  C_  z  <->  E. w  e.  F  w  C_  v )
6662, 65anbi12i 708 . . 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 4558 . . . 4  |-  ( u  i^i  v )  e. 
_V
68 sseq2 3466 . . . . 5  |-  ( z  =  ( u  i^i  v )  ->  (
y  C_  z  <->  y  C_  ( u  i^i  v
) ) )
6968rexbidv 2913 . . . 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 3314 . . 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 278 . 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 20922 1  |-  ( F  e.  ( fBas `  X
)  ->  ( X filGen F )  e.  ( Fil `  X ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   E.wrex 2750   [.wsbc 3279    i^i cin 3415    C_ wss 3416   (/)c0 3743   dom cdm 4853   ` cfv 5601  (class class class)co 6315   fBascfbas 19007   filGencfg 19008   Filcfil 20909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-fbas 19016  df-fg 19017  df-fil 20910
This theorem is referenced by:  fgabs  20943  trfg  20955  isufil2  20972  ssufl  20982  ufileu  20983  filufint  20984  fixufil  20986  uffixfr  20987  fmfil  21008  fmfg  21013  elfm3  21014  rnelfm  21017  fmfnfmlem2  21019  fmfnfm  21022  fbflim  21040  hausflim  21045  flimclslem  21048  flffbas  21059  fclsbas  21085  fclsfnflim  21091  flimfnfcls  21092  fclscmp  21094  haustsms  21199  tsmscls  21201  tsmsmhm  21209  tsmsadd  21210  cfilufg  21357  metust  21622  fgcfil  22290  cmetcaulem  22307  cmetss  22333  minveclem4a  22421  minveclem4  22423  minveclem4aOLD  22433  minveclem4OLD  22435
  Copyright terms: Public domain W3C validator