| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ufilfil | Structured version Visualization version GIF version | ||
| Description: An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
| Ref | Expression |
|---|---|
| ufilfil | ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isufil 24031 | . 2 ⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹))) | |
| 2 | 1 | simplbi 501 | 1 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 860 ∈ wcel 2149 ∀wral 3085 ∖ cdif 3910 𝒫 cpw 4567 ‘cfv 6539 Filcfil 23973 UFilcufil 24027 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5273 ax-pr 5407 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5559 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-iota 6495 df-fun 6541 df-fv 6547 df-ufil 24029 |
| This theorem is referenced by: ufilb 24034 isufil2 24036 ufprim 24037 trufil 24038 ufileu 24047 filufint 24048 uffixfr 24051 uffix2 24052 uffixsn 24053 uffinfix 24055 cfinufil 24056 ufilen 24058 ufildr 24059 fmufil 24087 ufldom 24090 uffclsflim 24159 ufilcmp 24160 uffcfflf 24167 alexsublem 24172 |
| Copyright terms: Public domain | W3C validator |