Theorem ufilfil 22490

Description: An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)

Assertion

Ref	Expression
ufilfil	⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))

Proof of Theorem ufilfil

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isufil 22489	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)))
2	1	simplbi 500	1 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))

Syntax hints:   → wi 4   ∨ wo 843   ∈ wcel 2114  ∀wral 3133   ∖ cdif 3916  𝒫 cpw 4520  ‘cfv 6336  Filcfil 22431  UFilcufil 22485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fv 6344  df-ufil 22487

This theorem is referenced by:  ufilb  22492  isufil2  22494  ufprim  22495  trufil  22496  ufileu  22505  filufint  22506  uffixfr  22509  uffix2  22510  uffixsn  22511  uffinfix  22513  cfinufil  22514  ufilen  22516  ufildr  22517  fmufil  22545  ufldom  22548  uffclsflim  22617  ufilcmp  22618  uffcfflf  22625  alexsublem  22630