Description: The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009) (Revised by Mario Carneiro, 12-Dec-2013) (Revised by Stefan O'Rear, 29-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fixufil | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uffix | |
|
2 | 1 | simprd | |
3 | 1 | simpld | |
4 | fgcl | |
|
5 | 3 4 | syl | |
6 | 2 5 | eqeltrd | |
7 | undif2 | |
|
8 | elpwi | |
|
9 | ssequn1 | |
|
10 | 8 9 | sylib | |
11 | 7 10 | eqtr2id | |
12 | 11 | eleq2d | |
13 | 12 | biimpac | |
14 | elun | |
|
15 | 13 14 | sylib | |
16 | 15 | adantll | |
17 | ibar | |
|
18 | 17 | adantl | |
19 | difss | |
|
20 | elpw2g | |
|
21 | 19 20 | mpbiri | |
22 | 21 | ad2antrr | |
23 | 22 | biantrurd | |
24 | 18 23 | orbi12d | |
25 | 16 24 | mpbid | |
26 | 25 | ralrimiva | |
27 | eleq2 | |
|
28 | 27 | elrab | |
29 | eleq2 | |
|
30 | 29 | elrab | |
31 | 28 30 | orbi12i | |
32 | 31 | ralbii | |
33 | 26 32 | sylibr | |
34 | isufil | |
|
35 | 6 33 34 | sylanbrc | |