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

Theorem fgcl 23135
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 (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))

Proof of Theorem fgcl
Dummy variables 𝑣 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfg 23128 . 2 (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧𝑋 ∧ ∃𝑦𝐹 𝑦𝑧)))
2 elfvex 6868 . 2 (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V)
3 fbasne0 23087 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
4 n0 4298 . . . . . 6 (𝐹 ≠ ∅ ↔ ∃𝑦 𝑦𝐹)
53, 4sylib 217 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦𝐹)
6 fbelss 23090 . . . . . . . 8 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
76ex 414 . . . . . . 7 (𝐹 ∈ (fBas‘𝑋) → (𝑦𝐹𝑦𝑋))
87ancld 552 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → (𝑦𝐹 → (𝑦𝐹𝑦𝑋)))
98eximdv 1920 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦𝐹 → ∃𝑦(𝑦𝐹𝑦𝑋)))
105, 9mpd 15 . . . 4 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦𝐹𝑦𝑋))
11 df-rex 3072 . . . 4 (∃𝑦𝐹 𝑦𝑋 ↔ ∃𝑦(𝑦𝐹𝑦𝑋))
1210, 11sylibr 233 . . 3 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦𝐹 𝑦𝑋)
13 elfvdm 6867 . . . 4 (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas)
14 sseq2 3962 . . . . . 6 (𝑧 = 𝑋 → (𝑦𝑧𝑦𝑋))
1514rexbidv 3172 . . . . 5 (𝑧 = 𝑋 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1615sbcieg 3771 . . . 4 (𝑋 ∈ dom fBas → ([𝑋 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1713, 16syl 17 . . 3 (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1812, 17mpbird 257 . 2 (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]𝑦𝐹 𝑦𝑧)
19 0nelfb 23088 . . 3 (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐹)
20 0ex 5256 . . . . 5 ∅ ∈ V
21 sseq2 3962 . . . . . 6 (𝑧 = ∅ → (𝑦𝑧𝑦 ⊆ ∅))
2221rexbidv 3172 . . . . 5 (𝑧 = ∅ → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ ∅))
2320, 22sbcie 3774 . . . 4 ([∅ / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ ∅)
24 ss0 4350 . . . . . . 7 (𝑦 ⊆ ∅ → 𝑦 = ∅)
2524eleq1d 2822 . . . . . 6 (𝑦 ⊆ ∅ → (𝑦𝐹 ↔ ∅ ∈ 𝐹))
2625biimpac 480 . . . . 5 ((𝑦𝐹𝑦 ⊆ ∅) → ∅ ∈ 𝐹)
2726rexlimiva 3141 . . . 4 (∃𝑦𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹)
2823, 27sylbi 216 . . 3 ([∅ / 𝑧]𝑦𝐹 𝑦𝑧 → ∅ ∈ 𝐹)
2919, 28nsyl 140 . 2 (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ / 𝑧]𝑦𝐹 𝑦𝑧)
30 sstr 3944 . . . . . 6 ((𝑦𝑣𝑣𝑢) → 𝑦𝑢)
3130expcom 415 . . . . 5 (𝑣𝑢 → (𝑦𝑣𝑦𝑢))
3231reximdv 3164 . . . 4 (𝑣𝑢 → (∃𝑦𝐹 𝑦𝑣 → ∃𝑦𝐹 𝑦𝑢))
33323ad2ant3 1135 . . 3 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑢) → (∃𝑦𝐹 𝑦𝑣 → ∃𝑦𝐹 𝑦𝑢))
34 vex 3446 . . . 4 𝑣 ∈ V
35 sseq2 3962 . . . . 5 (𝑧 = 𝑣 → (𝑦𝑧𝑦𝑣))
3635rexbidv 3172 . . . 4 (𝑧 = 𝑣 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑣))
3734, 36sbcie 3774 . . 3 ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑣)
38 vex 3446 . . . 4 𝑢 ∈ V
39 sseq2 3962 . . . . 5 (𝑧 = 𝑢 → (𝑦𝑧𝑦𝑢))
4039rexbidv 3172 . . . 4 (𝑧 = 𝑢 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑢))
4138, 40sbcie 3774 . . 3 ([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑢)
4233, 37, 413imtr4g 296 . 2 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑢) → ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧[𝑢 / 𝑧]𝑦𝐹 𝑦𝑧))
43 fbasssin 23093 . . . . . . . . . . . 12 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹𝑤𝐹) → ∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤))
44433expib 1122 . . . . . . . . . . 11 (𝐹 ∈ (fBas‘𝑋) → ((𝑧𝐹𝑤𝐹) → ∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤)))
45 sstr2 3943 . . . . . . . . . . . . . 14 (𝑦 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑦 ⊆ (𝑢𝑣)))
4645com12 32 . . . . . . . . . . . . 13 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑦 ⊆ (𝑧𝑤) → 𝑦 ⊆ (𝑢𝑣)))
4746reximdv 3164 . . . . . . . . . . . 12 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
48 ss2in 4188 . . . . . . . . . . . 12 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
4947, 48syl11 33 . . . . . . . . . . 11 (∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤) → ((𝑧𝑢𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
5044, 49syl6 35 . . . . . . . . . 10 (𝐹 ∈ (fBas‘𝑋) → ((𝑧𝐹𝑤𝐹) → ((𝑧𝑢𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5150exp5c 446 . . . . . . . . 9 (𝐹 ∈ (fBas‘𝑋) → (𝑧𝐹 → (𝑤𝐹 → (𝑧𝑢 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))))
5251imp31 419 . . . . . . . 8 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑤𝐹) → (𝑧𝑢 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5352impancom 453 . . . . . . 7 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑧𝑢) → (𝑤𝐹 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5453rexlimdv 3147 . . . . . 6 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑧𝑢) → (∃𝑤𝐹 𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
5554rexlimdva2 3151 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → (∃𝑧𝐹 𝑧𝑢 → (∃𝑤𝐹 𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5655impd 412 . . . 4 (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
57563ad2ant1 1133 . . 3 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑋) → ((∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
58 sseq1 3961 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
5958cbvrexvw 3223 . . . . 5 (∃𝑦𝐹 𝑦𝑢 ↔ ∃𝑧𝐹 𝑧𝑢)
6041, 59bitri 275 . . . 4 ([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑧𝐹 𝑧𝑢)
61 sseq1 3961 . . . . . 6 (𝑦 = 𝑤 → (𝑦𝑣𝑤𝑣))
6261cbvrexvw 3223 . . . . 5 (∃𝑦𝐹 𝑦𝑣 ↔ ∃𝑤𝐹 𝑤𝑣)
6337, 62bitri 275 . . . 4 ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑤𝐹 𝑤𝑣)
6460, 63anbi12i 628 . . 3 (([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧[𝑣 / 𝑧]𝑦𝐹 𝑦𝑧) ↔ (∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣))
6538inex1 5266 . . . 4 (𝑢𝑣) ∈ V
66 sseq2 3962 . . . . 5 (𝑧 = (𝑢𝑣) → (𝑦𝑧𝑦 ⊆ (𝑢𝑣)))
6766rexbidv 3172 . . . 4 (𝑧 = (𝑢𝑣) → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
6865, 67sbcie 3774 . . 3 ([(𝑢𝑣) / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))
6957, 64, 683imtr4g 296 . 2 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑋) → (([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧[𝑣 / 𝑧]𝑦𝐹 𝑦𝑧) → [(𝑢𝑣) / 𝑧]𝑦𝐹 𝑦𝑧))
701, 2, 18, 29, 42, 69isfild 23115 1 (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2941  wrex 3071  Vcvv 3442  [wsbc 3731  cin 3901  wss 3902  c0 4274  dom cdm 5625  cfv 6484  (class class class)co 7342  fBascfbas 20691  filGencfg 20692  Filcfil 23102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fun 6486  df-fv 6492  df-ov 7345  df-oprab 7346  df-mpo 7347  df-fbas 20700  df-fg 20701  df-fil 23103
This theorem is referenced by:  fgabs  23136  trfg  23148  isufil2  23165  ssufl  23175  ufileu  23176  filufint  23177  fixufil  23179  uffixfr  23180  fmfil  23201  fmfg  23206  elfm3  23207  rnelfm  23210  fmfnfmlem2  23212  fmfnfm  23215  fbflim  23233  hausflim  23238  flimclslem  23241  flffbas  23252  fclsbas  23278  fclsfnflim  23284  flimfnfcls  23285  fclscmp  23287  haustsms  23393  tsmscls  23395  tsmsmhm  23403  tsmsadd  23404  cfilufg  23551  metust  23820  fgcfil  24541  cmetcaulem  24558  cmetss  24586  minveclem4a  24700  minveclem4  24702
  Copyright terms: Public domain W3C validator