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

Theorem fgcl 23229
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 23222 . 2 (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧𝑋 ∧ ∃𝑦𝐹 𝑦𝑧)))
2 elfvex 6880 . 2 (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V)
3 fbasne0 23181 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
4 n0 4306 . . . . . 6 (𝐹 ≠ ∅ ↔ ∃𝑦 𝑦𝐹)
53, 4sylib 217 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦𝐹)
6 fbelss 23184 . . . . . . . 8 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
76ex 413 . . . . . . 7 (𝐹 ∈ (fBas‘𝑋) → (𝑦𝐹𝑦𝑋))
87ancld 551 . . . . . 6 (𝐹 ∈ (fBas‘𝑋) → (𝑦𝐹 → (𝑦𝐹𝑦𝑋)))
98eximdv 1920 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦𝐹 → ∃𝑦(𝑦𝐹𝑦𝑋)))
105, 9mpd 15 . . . 4 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦𝐹𝑦𝑋))
11 df-rex 3074 . . . 4 (∃𝑦𝐹 𝑦𝑋 ↔ ∃𝑦(𝑦𝐹𝑦𝑋))
1210, 11sylibr 233 . . 3 (𝐹 ∈ (fBas‘𝑋) → ∃𝑦𝐹 𝑦𝑋)
13 elfvdm 6879 . . . 4 (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas)
14 sseq2 3970 . . . . . 6 (𝑧 = 𝑋 → (𝑦𝑧𝑦𝑋))
1514rexbidv 3175 . . . . 5 (𝑧 = 𝑋 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1615sbcieg 3779 . . . 4 (𝑋 ∈ dom fBas → ([𝑋 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1713, 16syl 17 . . 3 (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑋))
1812, 17mpbird 256 . 2 (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]𝑦𝐹 𝑦𝑧)
19 0nelfb 23182 . . 3 (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐹)
20 0ex 5264 . . . . 5 ∅ ∈ V
21 sseq2 3970 . . . . . 6 (𝑧 = ∅ → (𝑦𝑧𝑦 ⊆ ∅))
2221rexbidv 3175 . . . . 5 (𝑧 = ∅ → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ ∅))
2320, 22sbcie 3782 . . . 4 ([∅ / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ ∅)
24 ss0 4358 . . . . . . 7 (𝑦 ⊆ ∅ → 𝑦 = ∅)
2524eleq1d 2822 . . . . . 6 (𝑦 ⊆ ∅ → (𝑦𝐹 ↔ ∅ ∈ 𝐹))
2625biimpac 479 . . . . 5 ((𝑦𝐹𝑦 ⊆ ∅) → ∅ ∈ 𝐹)
2726rexlimiva 3144 . . . 4 (∃𝑦𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹)
2823, 27sylbi 216 . . 3 ([∅ / 𝑧]𝑦𝐹 𝑦𝑧 → ∅ ∈ 𝐹)
2919, 28nsyl 140 . 2 (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ / 𝑧]𝑦𝐹 𝑦𝑧)
30 sstr 3952 . . . . . 6 ((𝑦𝑣𝑣𝑢) → 𝑦𝑢)
3130expcom 414 . . . . 5 (𝑣𝑢 → (𝑦𝑣𝑦𝑢))
3231reximdv 3167 . . . 4 (𝑣𝑢 → (∃𝑦𝐹 𝑦𝑣 → ∃𝑦𝐹 𝑦𝑢))
33323ad2ant3 1135 . . 3 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑢) → (∃𝑦𝐹 𝑦𝑣 → ∃𝑦𝐹 𝑦𝑢))
34 vex 3449 . . . 4 𝑣 ∈ V
35 sseq2 3970 . . . . 5 (𝑧 = 𝑣 → (𝑦𝑧𝑦𝑣))
3635rexbidv 3175 . . . 4 (𝑧 = 𝑣 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑣))
3734, 36sbcie 3782 . . 3 ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑣)
38 vex 3449 . . . 4 𝑢 ∈ V
39 sseq2 3970 . . . . 5 (𝑧 = 𝑢 → (𝑦𝑧𝑦𝑢))
4039rexbidv 3175 . . . 4 (𝑧 = 𝑢 → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑢))
4138, 40sbcie 3782 . . 3 ([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦𝑢)
4233, 37, 413imtr4g 295 . 2 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑢) → ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧[𝑢 / 𝑧]𝑦𝐹 𝑦𝑧))
43 fbasssin 23187 . . . . . . . . . . . 12 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹𝑤𝐹) → ∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤))
44433expib 1122 . . . . . . . . . . 11 (𝐹 ∈ (fBas‘𝑋) → ((𝑧𝐹𝑤𝐹) → ∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤)))
45 sstr2 3951 . . . . . . . . . . . . . 14 (𝑦 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑦 ⊆ (𝑢𝑣)))
4645com12 32 . . . . . . . . . . . . 13 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑦 ⊆ (𝑧𝑤) → 𝑦 ⊆ (𝑢𝑣)))
4746reximdv 3167 . . . . . . . . . . . 12 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
48 ss2in 4196 . . . . . . . . . . . 12 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
4947, 48syl11 33 . . . . . . . . . . 11 (∃𝑦𝐹 𝑦 ⊆ (𝑧𝑤) → ((𝑧𝑢𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
5044, 49syl6 35 . . . . . . . . . 10 (𝐹 ∈ (fBas‘𝑋) → ((𝑧𝐹𝑤𝐹) → ((𝑧𝑢𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5150exp5c 445 . . . . . . . . 9 (𝐹 ∈ (fBas‘𝑋) → (𝑧𝐹 → (𝑤𝐹 → (𝑧𝑢 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))))
5251imp31 418 . . . . . . . 8 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑤𝐹) → (𝑧𝑢 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5352impancom 452 . . . . . . 7 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑧𝑢) → (𝑤𝐹 → (𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5453rexlimdv 3150 . . . . . 6 (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧𝐹) ∧ 𝑧𝑢) → (∃𝑤𝐹 𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
5554rexlimdva2 3154 . . . . 5 (𝐹 ∈ (fBas‘𝑋) → (∃𝑧𝐹 𝑧𝑢 → (∃𝑤𝐹 𝑤𝑣 → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))))
5655impd 411 . . . 4 (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
57563ad2ant1 1133 . . 3 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑋) → ((∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣) → ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
58 sseq1 3969 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝑢𝑧𝑢))
5958cbvrexvw 3226 . . . . 5 (∃𝑦𝐹 𝑦𝑢 ↔ ∃𝑧𝐹 𝑧𝑢)
6041, 59bitri 274 . . . 4 ([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑧𝐹 𝑧𝑢)
61 sseq1 3969 . . . . . 6 (𝑦 = 𝑤 → (𝑦𝑣𝑤𝑣))
6261cbvrexvw 3226 . . . . 5 (∃𝑦𝐹 𝑦𝑣 ↔ ∃𝑤𝐹 𝑤𝑣)
6337, 62bitri 274 . . . 4 ([𝑣 / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑤𝐹 𝑤𝑣)
6460, 63anbi12i 627 . . 3 (([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧[𝑣 / 𝑧]𝑦𝐹 𝑦𝑧) ↔ (∃𝑧𝐹 𝑧𝑢 ∧ ∃𝑤𝐹 𝑤𝑣))
6538inex1 5274 . . . 4 (𝑢𝑣) ∈ V
66 sseq2 3970 . . . . 5 (𝑧 = (𝑢𝑣) → (𝑦𝑧𝑦 ⊆ (𝑢𝑣)))
6766rexbidv 3175 . . . 4 (𝑧 = (𝑢𝑣) → (∃𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣)))
6865, 67sbcie 3782 . . 3 ([(𝑢𝑣) / 𝑧]𝑦𝐹 𝑦𝑧 ↔ ∃𝑦𝐹 𝑦 ⊆ (𝑢𝑣))
6957, 64, 683imtr4g 295 . 2 ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢𝑋𝑣𝑋) → (([𝑢 / 𝑧]𝑦𝐹 𝑦𝑧[𝑣 / 𝑧]𝑦𝐹 𝑦𝑧) → [(𝑢𝑣) / 𝑧]𝑦𝐹 𝑦𝑧))
701, 2, 18, 29, 42, 69isfild 23209 1 (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  [wsbc 3739  cin 3909  wss 3910  c0 4282  dom cdm 5633  cfv 6496  (class class class)co 7357  fBascfbas 20784  filGencfg 20785  Filcfil 23196
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 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-fbas 20793  df-fg 20794  df-fil 23197
This theorem is referenced by:  fgabs  23230  trfg  23242  isufil2  23259  ssufl  23269  ufileu  23270  filufint  23271  fixufil  23273  uffixfr  23274  fmfil  23295  fmfg  23300  elfm3  23301  rnelfm  23304  fmfnfmlem2  23306  fmfnfm  23309  fbflim  23327  hausflim  23332  flimclslem  23335  flffbas  23346  fclsbas  23372  fclsfnflim  23378  flimfnfcls  23379  fclscmp  23381  haustsms  23487  tsmscls  23489  tsmsmhm  23497  tsmsadd  23498  cfilufg  23645  metust  23914  fgcfil  24635  cmetcaulem  24652  cmetss  24680  minveclem4a  24794  minveclem4  24796
  Copyright terms: Public domain W3C validator