Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Mario Carneiro, 4-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | ufinffr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ominf | |
|
2 | domfi | |
|
3 | 2 | expcom | |
4 | 1 3 | mtoi | |
5 | cfinfil | |
|
6 | 4 5 | syl3an3 | |
7 | filssufil | |
|
8 | 6 7 | syl | |
9 | difeq2 | |
|
10 | difid | |
|
11 | 9 10 | eqtrdi | |
12 | 11 | eleq1d | |
13 | elpw2g | |
|
14 | 13 | biimpar | |
15 | 14 | 3adant3 | |
16 | 0fin | |
|
17 | 16 | a1i | |
18 | 12 15 17 | elrabd | |
19 | ssel | |
|
20 | 18 19 | syl5com | |
21 | intss | |
|
22 | neldifsn | |
|
23 | elinti | |
|
24 | 22 23 | mtoi | |
25 | difeq2 | |
|
26 | 25 | eleq1d | |
27 | simp2 | |
|
28 | 27 | ssdifssd | |
29 | elpw2g | |
|
30 | 29 | 3ad2ant1 | |
31 | 28 30 | mpbird | |
32 | snfi | |
|
33 | eldif | |
|
34 | eldif | |
|
35 | 34 | notbii | |
36 | iman | |
|
37 | 35 36 | bitr4i | |
38 | 37 | anbi2i | |
39 | 33 38 | bitri | |
40 | pm3.35 | |
|
41 | 39 40 | sylbi | |
42 | 41 | ssriv | |
43 | ssfi | |
|
44 | 32 42 43 | mp2an | |
45 | 44 | a1i | |
46 | 26 31 45 | elrabd | |
47 | 24 46 | nsyl3 | |
48 | 47 | eq0rdv | |
49 | 48 | sseq2d | |
50 | 21 49 | syl5ib | |
51 | ss0 | |
|
52 | 50 51 | syl6 | |
53 | 20 52 | jcad | |
54 | 53 | reximdv | |
55 | 8 54 | mpd | |