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

Theorem filtop 22464
 Description: The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
Assertion
Ref Expression
filtop (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)

Proof of Theorem filtop
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 filfbas 22457 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
2 fbasne0 22439 . . 3 (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
31, 2syl 17 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
4 n0 4263 . . 3 (𝐹 ≠ ∅ ↔ ∃𝑥 𝑥𝐹)
5 filelss 22461 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝐹) → 𝑥𝑋)
6 ssid 3940 . . . . . . 7 𝑋𝑋
7 filss 22462 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥𝐹𝑋𝑋𝑥𝑋)) → 𝑋𝐹)
873exp2 1351 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝐹 → (𝑋𝑋 → (𝑥𝑋𝑋𝐹))))
98imp 410 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝐹) → (𝑋𝑋 → (𝑥𝑋𝑋𝐹)))
106, 9mpi 20 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝐹) → (𝑥𝑋𝑋𝐹))
115, 10mpd 15 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝐹) → 𝑋𝐹)
1211ex 416 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝐹𝑋𝐹))
1312exlimdv 1934 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∃𝑥 𝑥𝐹𝑋𝐹))
144, 13syl5bi 245 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ≠ ∅ → 𝑋𝐹))
153, 14mpd 15 1 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2112   ≠ wne 2990   ⊆ wss 3884  ∅c0 4246  ‘cfv 6328  fBascfbas 20083  Filcfil 22454 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fv 6336  df-fbas 20092  df-fil 22455 This theorem is referenced by:  isfil2  22465  filn0  22471  infil  22472  filunibas  22490  filuni  22494  trfil1  22495  trfil2  22496  fgtr  22499  trfg  22500  isufil2  22517  filssufil  22521  ssufl  22527  ufileu  22528  filufint  22529  uffixfr  22532  cfinufil  22537  rnelfmlem  22561  rnelfm  22562  fmfnfmlem1  22563  fmfnfmlem2  22564  fmfnfmlem4  22566  fmfnfm  22567  flfval  22599  fclsfnflim  22636  flimfnfcls  22637  fcfval  22642  alexsublem  22653  metust  23169  cmetss  23924  minveclem4a  24038  filnetlem3  33842  filnetlem4  33843
 Copyright terms: Public domain W3C validator