Metamath Proof Explorer


Theorem fixufil

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 XVAXx𝒫X|AxUFilX

Proof

Step Hyp Ref Expression
1 uffix XVAXAfBasXx𝒫X|Ax=XfilGenA
2 1 simprd XVAXx𝒫X|Ax=XfilGenA
3 1 simpld XVAXAfBasX
4 fgcl AfBasXXfilGenAFilX
5 3 4 syl XVAXXfilGenAFilX
6 2 5 eqeltrd XVAXx𝒫X|AxFilX
7 undif2 yXy=yX
8 elpwi y𝒫XyX
9 ssequn1 yXyX=X
10 8 9 sylib y𝒫XyX=X
11 7 10 eqtr2id y𝒫XX=yXy
12 11 eleq2d y𝒫XAXAyXy
13 12 biimpac AXy𝒫XAyXy
14 elun AyXyAyAXy
15 13 14 sylib AXy𝒫XAyAXy
16 15 adantll XVAXy𝒫XAyAXy
17 ibar y𝒫XAyy𝒫XAy
18 17 adantl XVAXy𝒫XAyy𝒫XAy
19 difss XyX
20 elpw2g XVXy𝒫XXyX
21 19 20 mpbiri XVXy𝒫X
22 21 ad2antrr XVAXy𝒫XXy𝒫X
23 22 biantrurd XVAXy𝒫XAXyXy𝒫XAXy
24 18 23 orbi12d XVAXy𝒫XAyAXyy𝒫XAyXy𝒫XAXy
25 16 24 mpbid XVAXy𝒫Xy𝒫XAyXy𝒫XAXy
26 25 ralrimiva XVAXy𝒫Xy𝒫XAyXy𝒫XAXy
27 eleq2 x=yAxAy
28 27 elrab yx𝒫X|Axy𝒫XAy
29 eleq2 x=XyAxAXy
30 29 elrab Xyx𝒫X|AxXy𝒫XAXy
31 28 30 orbi12i yx𝒫X|AxXyx𝒫X|Axy𝒫XAyXy𝒫XAXy
32 31 ralbii y𝒫Xyx𝒫X|AxXyx𝒫X|Axy𝒫Xy𝒫XAyXy𝒫XAXy
33 26 32 sylibr XVAXy𝒫Xyx𝒫X|AxXyx𝒫X|Ax
34 isufil x𝒫X|AxUFilXx𝒫X|AxFilXy𝒫Xyx𝒫X|AxXyx𝒫X|Ax
35 6 33 34 sylanbrc XVAXx𝒫X|AxUFilX