Description: A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 .) (Contributed by Jeff Hankins, 2-Dec-2009) (Revised by Stefan O'Rear, 29-Jul-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | filssufil | |- ( F e. ( Fil ` X ) -> E. f e. ( UFil ` X ) F C_ f ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | filtop | |- ( F e. ( Fil ` X ) -> X e. F ) |
|
| 2 | pwexg | |- ( X e. F -> ~P X e. _V ) |
|
| 3 | pwexg | |- ( ~P X e. _V -> ~P ~P X e. _V ) |
|
| 4 | numth3 | |- ( ~P ~P X e. _V -> ~P ~P X e. dom card ) |
|
| 5 | 1 2 3 4 | 4syl | |- ( F e. ( Fil ` X ) -> ~P ~P X e. dom card ) |
| 6 | filssufilg | |- ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. f e. ( UFil ` X ) F C_ f ) |
|
| 7 | 5 6 | mpdan | |- ( F e. ( Fil ` X ) -> E. f e. ( UFil ` X ) F C_ f ) |