Metamath Proof Explorer


Theorem fin1aufil

Description: There are no definable free ultrafilters in ZFC. However, there are free ultrafilters in some choice-denying constructions. Here we show that given an amorphous set (a.k.a. a Ia-finite I-infinite set) X , the set of infinite subsets of X is a free ultrafilter on X . (Contributed by Mario Carneiro, 20-May-2015)

Ref Expression
Hypothesis fin1aufil.1 F=𝒫XFin
Assertion fin1aufil XFinIaFinFUFilXF=

Proof

Step Hyp Ref Expression
1 fin1aufil.1 F=𝒫XFin
2 1 eleq2i xFx𝒫XFin
3 eldif x𝒫XFinx𝒫X¬xFin
4 velpw x𝒫XxX
5 4 anbi1i x𝒫X¬xFinxX¬xFin
6 2 3 5 3bitri xFxX¬xFin
7 6 a1i XFinIaFinxFxX¬xFin
8 id XFinIaFinXFinIaFin
9 eldifn XFinIaFin¬XFin
10 eleq1 x=XxFinXFin
11 10 notbid x=X¬xFin¬XFin
12 11 sbcieg XFinIaFin[˙X/x]˙¬xFin¬XFin
13 9 12 mpbird XFinIaFin[˙X/x]˙¬xFin
14 0fin Fin
15 0ex V
16 eleq1 x=xFinFin
17 16 notbid x=¬xFin¬Fin
18 15 17 sbcie [˙/x]˙¬xFin¬Fin
19 18 con2bii Fin¬[˙/x]˙¬xFin
20 14 19 mpbi ¬[˙/x]˙¬xFin
21 20 a1i XFinIaFin¬[˙/x]˙¬xFin
22 ssfi yFinzyzFin
23 22 expcom zyyFinzFin
24 23 3ad2ant3 XFinIaFinyXzyyFinzFin
25 24 con3d XFinIaFinyXzy¬zFin¬yFin
26 vex zV
27 eleq1 x=zxFinzFin
28 27 notbid x=z¬xFin¬zFin
29 26 28 sbcie [˙z/x]˙¬xFin¬zFin
30 vex yV
31 eleq1 x=yxFinyFin
32 31 notbid x=y¬xFin¬yFin
33 30 32 sbcie [˙y/x]˙¬xFin¬yFin
34 25 29 33 3imtr4g XFinIaFinyXzy[˙z/x]˙¬xFin[˙y/x]˙¬xFin
35 eldifi XFinIaFinXFinIa
36 fin1ai XFinIayXyFinXyFin
37 35 36 sylan XFinIaFinyXyFinXyFin
38 37 3adant3 XFinIaFinyXzXyFinXyFin
39 inundif zyzy=z
40 incom zy=yz
41 simprl XFinIaFinyXzXyzFinXyFinyzFin
42 40 41 eqeltrid XFinIaFinyXzXyzFinXyFinzyFin
43 simprr XFinIaFinyXzXyzFinXyFinXyFin
44 simpl3 XFinIaFinyXzXyzFinXyFinzX
45 44 ssdifd XFinIaFinyXzXyzFinXyFinzyXy
46 43 45 ssfid XFinIaFinyXzXyzFinXyFinzyFin
47 unfi zyFinzyFinzyzyFin
48 42 46 47 syl2anc XFinIaFinyXzXyzFinXyFinzyzyFin
49 39 48 eqeltrrid XFinIaFinyXzXyzFinXyFinzFin
50 49 expr XFinIaFinyXzXyzFinXyFinzFin
51 50 orim2d XFinIaFinyXzXyzFinyFinXyFinyFinzFin
52 51 ex XFinIaFinyXzXyzFinyFinXyFinyFinzFin
53 38 52 mpid XFinIaFinyXzXyzFinyFinzFin
54 53 con3d XFinIaFinyXzX¬yFinzFin¬yzFin
55 33 29 anbi12i [˙y/x]˙¬xFin[˙z/x]˙¬xFin¬yFin¬zFin
56 ioran ¬yFinzFin¬yFin¬zFin
57 55 56 bitr4i [˙y/x]˙¬xFin[˙z/x]˙¬xFin¬yFinzFin
58 30 inex1 yzV
59 eleq1 x=yzxFinyzFin
60 59 notbid x=yz¬xFin¬yzFin
61 58 60 sbcie [˙yz/x]˙¬xFin¬yzFin
62 54 57 61 3imtr4g XFinIaFinyXzX[˙y/x]˙¬xFin[˙z/x]˙¬xFin[˙yz/x]˙¬xFin
63 7 8 13 21 34 62 isfild XFinIaFinFFilX
64 9 adantr XFinIaFinx𝒫X¬XFin
65 unfi xFinXxFinxXxFin
66 ssun2 XxX
67 undif2 xXx=xX
68 66 67 sseqtrri XxXx
69 ssfi xXxFinXxXxXFin
70 65 68 69 sylancl xFinXxFinXFin
71 64 70 nsyl XFinIaFinx𝒫X¬xFinXxFin
72 ianor ¬xFinXxFin¬xFin¬XxFin
73 71 72 sylib XFinIaFinx𝒫X¬xFin¬XxFin
74 elpwi x𝒫XxX
75 74 adantl XFinIaFinx𝒫XxX
76 6 baib xXxF¬xFin
77 75 76 syl XFinIaFinx𝒫XxF¬xFin
78 1 eleq2i XxFXx𝒫XFin
79 difss XxX
80 elpw2g XFinIaFinXx𝒫XXxX
81 80 adantr XFinIaFinx𝒫XXx𝒫XXxX
82 79 81 mpbiri XFinIaFinx𝒫XXx𝒫X
83 eldif Xx𝒫XFinXx𝒫X¬XxFin
84 83 baib Xx𝒫XXx𝒫XFin¬XxFin
85 82 84 syl XFinIaFinx𝒫XXx𝒫XFin¬XxFin
86 78 85 syl5bb XFinIaFinx𝒫XXxF¬XxFin
87 77 86 orbi12d XFinIaFinx𝒫XxFXxF¬xFin¬XxFin
88 73 87 mpbird XFinIaFinx𝒫XxFXxF
89 88 ralrimiva XFinIaFinx𝒫XxFXxF
90 isufil FUFilXFFilXx𝒫XxFXxF
91 63 89 90 sylanbrc XFinIaFinFUFilX
92 snfi xFin
93 eldifn x𝒫XFin¬xFin
94 93 1 eleq2s xF¬xFin
95 92 94 mt2 ¬xF
96 uffixsn FUFilXxFxF
97 91 96 sylan XFinIaFinxFxF
98 97 ex XFinIaFinxFxF
99 95 98 mtoi XFinIaFin¬xF
100 99 eq0rdv XFinIaFinF=
101 91 100 jca XFinIaFinFUFilXF=