Metamath Proof Explorer


Theorem cfinufil

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 FUFilXF=x𝒫X|XxFinF

Proof

Step Hyp Ref Expression
1 elpwi x𝒫XxX
2 ufilb FUFilXxX¬xFXxF
3 2 adantr FUFilXxXXxFin¬xFXxF
4 ufilfil FUFilXFFilX
5 4 adantr FUFilXxXFFilX
6 filfinnfr FFilXXxFXxFinF
7 6 3exp FFilXXxFXxFinF
8 7 com23 FFilXXxFinXxFF
9 5 8 syl FUFilXxXXxFinXxFF
10 9 imp FUFilXxXXxFinXxFF
11 3 10 sylbid FUFilXxXXxFin¬xFF
12 11 necon4bd FUFilXxXXxFinF=xF
13 12 ex FUFilXxXXxFinF=xF
14 13 com23 FUFilXxXF=XxFinxF
15 1 14 sylan2 FUFilXx𝒫XF=XxFinxF
16 15 ralrimdva FUFilXF=x𝒫XXxFinxF
17 4 adantr FUFilXyFFFilX
18 uffixsn FUFilXyFyF
19 filelss FFilXyFyX
20 17 18 19 syl2anc FUFilXyFyX
21 dfss4 yXXXy=y
22 20 21 sylib FUFilXyFXXy=y
23 snfi yFin
24 22 23 eqeltrdi FUFilXyFXXyFin
25 difss XyX
26 filtop FFilXXF
27 elpw2g XFXy𝒫XXyX
28 17 26 27 3syl FUFilXyFXy𝒫XXyX
29 25 28 mpbiri FUFilXyFXy𝒫X
30 difeq2 x=XyXx=XXy
31 30 eleq1d x=XyXxFinXXyFin
32 eleq1 x=XyxFXyF
33 31 32 imbi12d x=XyXxFinxFXXyFinXyF
34 33 rspcv Xy𝒫Xx𝒫XXxFinxFXXyFinXyF
35 29 34 syl FUFilXyFx𝒫XXxFinxFXXyFinXyF
36 24 35 mpid FUFilXyFx𝒫XXxFinxFXyF
37 ufilb FUFilXyX¬yFXyF
38 20 37 syldan FUFilXyF¬yFXyF
39 18 pm2.24d FUFilXyF¬yF¬yF
40 38 39 sylbird FUFilXyFXyF¬yF
41 36 40 syld FUFilXyFx𝒫XXxFinxF¬yF
42 41 impancom FUFilXx𝒫XXxFinxFyF¬yF
43 42 pm2.01d FUFilXx𝒫XXxFinxF¬yF
44 43 eq0rdv FUFilXx𝒫XXxFinxFF=
45 44 ex FUFilXx𝒫XXxFinxFF=
46 16 45 impbid FUFilXF=x𝒫XXxFinxF
47 rabss x𝒫X|XxFinFx𝒫XXxFinxF
48 46 47 bitr4di FUFilXF=x𝒫X|XxFinF