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

Theorem filss 22165
Description: A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
Assertion
Ref Expression
filss ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐵𝐹)

Proof of Theorem filss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 isfil 22159 . . . 4 (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹)))
21simprbi 489 . . 3 (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹))
32adantr 473 . 2 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹))
4 elfvdm 6531 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ dom Fil)
5 simp2 1117 . . 3 ((𝐴𝐹𝐵𝑋𝐴𝐵) → 𝐵𝑋)
6 elpw2g 5103 . . . 4 (𝑋 ∈ dom Fil → (𝐵 ∈ 𝒫 𝑋𝐵𝑋))
76biimpar 470 . . 3 ((𝑋 ∈ dom Fil ∧ 𝐵𝑋) → 𝐵 ∈ 𝒫 𝑋)
84, 5, 7syl2an 586 . 2 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐵 ∈ 𝒫 𝑋)
9 simpr1 1174 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐴𝐹)
10 simpr3 1176 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐴𝐵)
119, 10elpwd 4431 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐴 ∈ 𝒫 𝐵)
12 inelcm 4297 . . 3 ((𝐴𝐹𝐴 ∈ 𝒫 𝐵) → (𝐹 ∩ 𝒫 𝐵) ≠ ∅)
139, 11, 12syl2anc 576 . 2 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → (𝐹 ∩ 𝒫 𝐵) ≠ ∅)
14 pweq 4425 . . . . . 6 (𝑥 = 𝐵 → 𝒫 𝑥 = 𝒫 𝐵)
1514ineq2d 4076 . . . . 5 (𝑥 = 𝐵 → (𝐹 ∩ 𝒫 𝑥) = (𝐹 ∩ 𝒫 𝐵))
1615neeq1d 3026 . . . 4 (𝑥 = 𝐵 → ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ ↔ (𝐹 ∩ 𝒫 𝐵) ≠ ∅))
17 eleq1 2853 . . . 4 (𝑥 = 𝐵 → (𝑥𝐹𝐵𝐹))
1816, 17imbi12d 337 . . 3 (𝑥 = 𝐵 → (((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹) ↔ ((𝐹 ∩ 𝒫 𝐵) ≠ ∅ → 𝐵𝐹)))
1918rspccv 3532 . 2 (∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹) → (𝐵 ∈ 𝒫 𝑋 → ((𝐹 ∩ 𝒫 𝐵) ≠ ∅ → 𝐵𝐹)))
203, 8, 13, 19syl3c 66 1 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴𝐹𝐵𝑋𝐴𝐵)) → 𝐵𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2967  wral 3088  cin 3828  wss 3829  c0 4178  𝒫 cpw 4422  dom cdm 5407  cfv 6188  fBascfbas 20235  Filcfil 22157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fv 6196  df-fil 22158
This theorem is referenced by:  filin  22166  filtop  22167  isfil2  22168  infil  22175  fgfil  22187  fgabs  22191  filconn  22195  filuni  22197  trfil2  22199  trfg  22203  isufil2  22220  ufprim  22221  ufileu  22231  filufint  22232  elfm3  22262  rnelfm  22265  fmfnfmlem2  22267  fmfnfmlem4  22269  flimopn  22287  flimrest  22295  flimfnfcls  22340  fclscmpi  22341  alexsublem  22356  metust  22871  cfil3i  23575  cfilfcls  23580  iscmet3lem2  23598  equivcfil  23605  relcmpcmet  23624  minveclem4  23738  fgmin  33245
  Copyright terms: Public domain W3C validator