Description: An ultrafilter is free iff it contains the Fréchet filter cfinfil as a subset. (Contributed by NM, 14-Jul-2008) (Revised by Stefan O'Rear, 2-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cfinufil | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi | |
|
2 | ufilb | |
|
3 | 2 | adantr | |
4 | ufilfil | |
|
5 | 4 | adantr | |
6 | filfinnfr | |
|
7 | 6 | 3exp | |
8 | 7 | com23 | |
9 | 5 8 | syl | |
10 | 9 | imp | |
11 | 3 10 | sylbid | |
12 | 11 | necon4bd | |
13 | 12 | ex | |
14 | 13 | com23 | |
15 | 1 14 | sylan2 | |
16 | 15 | ralrimdva | |
17 | 4 | adantr | |
18 | uffixsn | |
|
19 | filelss | |
|
20 | 17 18 19 | syl2anc | |
21 | dfss4 | |
|
22 | 20 21 | sylib | |
23 | snfi | |
|
24 | 22 23 | eqeltrdi | |
25 | difss | |
|
26 | filtop | |
|
27 | elpw2g | |
|
28 | 17 26 27 | 3syl | |
29 | 25 28 | mpbiri | |
30 | difeq2 | |
|
31 | 30 | eleq1d | |
32 | eleq1 | |
|
33 | 31 32 | imbi12d | |
34 | 33 | rspcv | |
35 | 29 34 | syl | |
36 | 24 35 | mpid | |
37 | ufilb | |
|
38 | 20 37 | syldan | |
39 | 18 | pm2.24d | |
40 | 38 39 | sylbird | |
41 | 36 40 | syld | |
42 | 41 | impancom | |
43 | 42 | pm2.01d | |
44 | 43 | eq0rdv | |
45 | 44 | ex | |
46 | 16 45 | impbid | |
47 | rabss | |
|
48 | 46 47 | bitr4di | |