Description: Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ufilen | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldom | |
|
2 | 1 | brrelex2i | |
3 | numth3 | |
|
4 | 2 3 | syl | |
5 | csdfil | |
|
6 | 4 5 | mpancom | |
7 | filssufil | |
|
8 | 6 7 | syl | |
9 | elfvex | |
|
10 | 9 | ad2antlr | |
11 | ufilfil | |
|
12 | filelss | |
|
13 | 11 12 | sylan | |
14 | 13 | adantll | |
15 | ssdomg | |
|
16 | 10 14 15 | sylc | |
17 | filfbas | |
|
18 | 11 17 | syl | |
19 | 18 | adantl | |
20 | fbncp | |
|
21 | 19 20 | sylan | |
22 | difeq2 | |
|
23 | 22 | breq1d | |
24 | difss | |
|
25 | elpw2g | |
|
26 | 24 25 | mpbiri | |
27 | 26 | 3ad2ant1 | |
28 | simp2 | |
|
29 | dfss4 | |
|
30 | 28 29 | sylib | |
31 | simp3 | |
|
32 | 30 31 | eqbrtrd | |
33 | 23 27 32 | elrabd | |
34 | ssel | |
|
35 | 33 34 | syl5com | |
36 | 35 | 3expa | |
37 | 36 | impancom | |
38 | 37 | con3d | |
39 | 38 | impancom | |
40 | 10 14 21 39 | syl21anc | |
41 | bren2 | |
|
42 | 41 | simplbi2 | |
43 | 16 40 42 | sylsyld | |
44 | 43 | ralrimdva | |
45 | 44 | reximdva | |
46 | 8 45 | mpd | |