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 = ( ~P X \ Fin )
Assertion fin1aufil 
|- ( X e. ( Fin1a \ Fin ) -> ( F e. ( UFil ` X ) /\ |^| F = (/) ) )

Proof

Step Hyp Ref Expression
1 fin1aufil.1 
 |-  F = ( ~P X \ Fin )
2 1 eleq2i 
 |-  ( x e. F <-> x e. ( ~P X \ Fin ) )
3 eldif 
 |-  ( x e. ( ~P X \ Fin ) <-> ( x e. ~P X /\ -. x e. Fin ) )
4 velpw 
 |-  ( x e. ~P X <-> x C_ X )
5 4 anbi1i 
 |-  ( ( x e. ~P X /\ -. x e. Fin ) <-> ( x C_ X /\ -. x e. Fin ) )
6 2 3 5 3bitri 
 |-  ( x e. F <-> ( x C_ X /\ -. x e. Fin ) )
7 6 a1i 
 |-  ( X e. ( Fin1a \ Fin ) -> ( x e. F <-> ( x C_ X /\ -. x e. Fin ) ) )
8 id 
 |-  ( X e. ( Fin1a \ Fin ) -> X e. ( Fin1a \ Fin ) )
9 eldifn 
 |-  ( X e. ( Fin1a \ Fin ) -> -. X e. Fin )
10 eleq1 
 |-  ( x = X -> ( x e. Fin <-> X e. Fin ) )
11 10 notbid 
 |-  ( x = X -> ( -. x e. Fin <-> -. X e. Fin ) )
12 11 sbcieg 
 |-  ( X e. ( Fin1a \ Fin ) -> ( [. X / x ]. -. x e. Fin <-> -. X e. Fin ) )
13 9 12 mpbird 
 |-  ( X e. ( Fin1a \ Fin ) -> [. X / x ]. -. x e. Fin )
14 0fin 
 |-  (/) e. Fin
15 0ex 
 |-  (/) e. _V
16 eleq1 
 |-  ( x = (/) -> ( x e. Fin <-> (/) e. Fin ) )
17 16 notbid 
 |-  ( x = (/) -> ( -. x e. Fin <-> -. (/) e. Fin ) )
18 15 17 sbcie 
 |-  ( [. (/) / x ]. -. x e. Fin <-> -. (/) e. Fin )
19 18 con2bii 
 |-  ( (/) e. Fin <-> -. [. (/) / x ]. -. x e. Fin )
20 14 19 mpbi 
 |-  -. [. (/) / x ]. -. x e. Fin
21 20 a1i 
 |-  ( X e. ( Fin1a \ Fin ) -> -. [. (/) / x ]. -. x e. Fin )
22 ssfi 
 |-  ( ( y e. Fin /\ z C_ y ) -> z e. Fin )
23 22 expcom 
 |-  ( z C_ y -> ( y e. Fin -> z e. Fin ) )
24 23 3ad2ant3 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ y ) -> ( y e. Fin -> z e. Fin ) )
25 24 con3d 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ y ) -> ( -. z e. Fin -> -. y e. Fin ) )
26 vex 
 |-  z e. _V
27 eleq1 
 |-  ( x = z -> ( x e. Fin <-> z e. Fin ) )
28 27 notbid 
 |-  ( x = z -> ( -. x e. Fin <-> -. z e. Fin ) )
29 26 28 sbcie 
 |-  ( [. z / x ]. -. x e. Fin <-> -. z e. Fin )
30 vex 
 |-  y e. _V
31 eleq1 
 |-  ( x = y -> ( x e. Fin <-> y e. Fin ) )
32 31 notbid 
 |-  ( x = y -> ( -. x e. Fin <-> -. y e. Fin ) )
33 30 32 sbcie 
 |-  ( [. y / x ]. -. x e. Fin <-> -. y e. Fin )
34 25 29 33 3imtr4g 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ y ) -> ( [. z / x ]. -. x e. Fin -> [. y / x ]. -. x e. Fin ) )
35 eldifi 
 |-  ( X e. ( Fin1a \ Fin ) -> X e. Fin1a )
36 fin1ai 
 |-  ( ( X e. Fin1a /\ y C_ X ) -> ( y e. Fin \/ ( X \ y ) e. Fin ) )
37 35 36 sylan 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X ) -> ( y e. Fin \/ ( X \ y ) e. Fin ) )
38 37 3adant3 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) -> ( y e. Fin \/ ( X \ y ) e. Fin ) )
39 inundif 
 |-  ( ( z i^i y ) u. ( z \ y ) ) = z
40 incom 
 |-  ( z i^i y ) = ( y i^i z )
41 simprl 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( y i^i z ) e. Fin )
42 40 41 eqeltrid 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( z i^i y ) e. Fin )
43 simprr 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( X \ y ) e. Fin )
44 simpl3 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> z C_ X )
45 44 ssdifd 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( z \ y ) C_ ( X \ y ) )
46 43 45 ssfid 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( z \ y ) e. Fin )
47 unfi 
 |-  ( ( ( z i^i y ) e. Fin /\ ( z \ y ) e. Fin ) -> ( ( z i^i y ) u. ( z \ y ) ) e. Fin )
48 42 46 47 syl2anc 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> ( ( z i^i y ) u. ( z \ y ) ) e. Fin )
49 39 48 eqeltrrid 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( ( y i^i z ) e. Fin /\ ( X \ y ) e. Fin ) ) -> z e. Fin )
50 49 expr 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( y i^i z ) e. Fin ) -> ( ( X \ y ) e. Fin -> z e. Fin ) )
51 50 orim2d 
 |-  ( ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) /\ ( y i^i z ) e. Fin ) -> ( ( y e. Fin \/ ( X \ y ) e. Fin ) -> ( y e. Fin \/ z e. Fin ) ) )
52 51 ex 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) -> ( ( y i^i z ) e. Fin -> ( ( y e. Fin \/ ( X \ y ) e. Fin ) -> ( y e. Fin \/ z e. Fin ) ) ) )
53 38 52 mpid 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) -> ( ( y i^i z ) e. Fin -> ( y e. Fin \/ z e. Fin ) ) )
54 53 con3d 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) -> ( -. ( y e. Fin \/ z e. Fin ) -> -. ( y i^i z ) e. Fin ) )
55 33 29 anbi12i 
 |-  ( ( [. y / x ]. -. x e. Fin /\ [. z / x ]. -. x e. Fin ) <-> ( -. y e. Fin /\ -. z e. Fin ) )
56 ioran 
 |-  ( -. ( y e. Fin \/ z e. Fin ) <-> ( -. y e. Fin /\ -. z e. Fin ) )
57 55 56 bitr4i 
 |-  ( ( [. y / x ]. -. x e. Fin /\ [. z / x ]. -. x e. Fin ) <-> -. ( y e. Fin \/ z e. Fin ) )
58 30 inex1 
 |-  ( y i^i z ) e. _V
59 eleq1 
 |-  ( x = ( y i^i z ) -> ( x e. Fin <-> ( y i^i z ) e. Fin ) )
60 59 notbid 
 |-  ( x = ( y i^i z ) -> ( -. x e. Fin <-> -. ( y i^i z ) e. Fin ) )
61 58 60 sbcie 
 |-  ( [. ( y i^i z ) / x ]. -. x e. Fin <-> -. ( y i^i z ) e. Fin )
62 54 57 61 3imtr4g 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ y C_ X /\ z C_ X ) -> ( ( [. y / x ]. -. x e. Fin /\ [. z / x ]. -. x e. Fin ) -> [. ( y i^i z ) / x ]. -. x e. Fin ) )
63 7 8 13 21 34 62 isfild 
 |-  ( X e. ( Fin1a \ Fin ) -> F e. ( Fil ` X ) )
64 9 adantr 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> -. X e. Fin )
65 unfi 
 |-  ( ( x e. Fin /\ ( X \ x ) e. Fin ) -> ( x u. ( X \ x ) ) e. Fin )
66 ssun2 
 |-  X C_ ( x u. X )
67 undif2 
 |-  ( x u. ( X \ x ) ) = ( x u. X )
68 66 67 sseqtrri 
 |-  X C_ ( x u. ( X \ x ) )
69 ssfi 
 |-  ( ( ( x u. ( X \ x ) ) e. Fin /\ X C_ ( x u. ( X \ x ) ) ) -> X e. Fin )
70 65 68 69 sylancl 
 |-  ( ( x e. Fin /\ ( X \ x ) e. Fin ) -> X e. Fin )
71 64 70 nsyl 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> -. ( x e. Fin /\ ( X \ x ) e. Fin ) )
72 ianor 
 |-  ( -. ( x e. Fin /\ ( X \ x ) e. Fin ) <-> ( -. x e. Fin \/ -. ( X \ x ) e. Fin ) )
73 71 72 sylib 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( -. x e. Fin \/ -. ( X \ x ) e. Fin ) )
74 elpwi 
 |-  ( x e. ~P X -> x C_ X )
75 74 adantl 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> x C_ X )
76 6 baib 
 |-  ( x C_ X -> ( x e. F <-> -. x e. Fin ) )
77 75 76 syl 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( x e. F <-> -. x e. Fin ) )
78 1 eleq2i 
 |-  ( ( X \ x ) e. F <-> ( X \ x ) e. ( ~P X \ Fin ) )
79 difss 
 |-  ( X \ x ) C_ X
80 elpw2g 
 |-  ( X e. ( Fin1a \ Fin ) -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
81 80 adantr 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
82 79 81 mpbiri 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( X \ x ) e. ~P X )
83 eldif 
 |-  ( ( X \ x ) e. ( ~P X \ Fin ) <-> ( ( X \ x ) e. ~P X /\ -. ( X \ x ) e. Fin ) )
84 83 baib 
 |-  ( ( X \ x ) e. ~P X -> ( ( X \ x ) e. ( ~P X \ Fin ) <-> -. ( X \ x ) e. Fin ) )
85 82 84 syl 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( ( X \ x ) e. ( ~P X \ Fin ) <-> -. ( X \ x ) e. Fin ) )
86 78 85 syl5bb 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( ( X \ x ) e. F <-> -. ( X \ x ) e. Fin ) )
87 77 86 orbi12d 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( ( x e. F \/ ( X \ x ) e. F ) <-> ( -. x e. Fin \/ -. ( X \ x ) e. Fin ) ) )
88 73 87 mpbird 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. ~P X ) -> ( x e. F \/ ( X \ x ) e. F ) )
89 88 ralrimiva 
 |-  ( X e. ( Fin1a \ Fin ) -> A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) )
90 isufil 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
91 63 89 90 sylanbrc 
 |-  ( X e. ( Fin1a \ Fin ) -> F e. ( UFil ` X ) )
92 snfi 
 |-  { x } e. Fin
93 eldifn 
 |-  ( { x } e. ( ~P X \ Fin ) -> -. { x } e. Fin )
94 93 1 eleq2s 
 |-  ( { x } e. F -> -. { x } e. Fin )
95 92 94 mt2 
 |-  -. { x } e. F
96 uffixsn 
 |-  ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> { x } e. F )
97 91 96 sylan 
 |-  ( ( X e. ( Fin1a \ Fin ) /\ x e. |^| F ) -> { x } e. F )
98 97 ex 
 |-  ( X e. ( Fin1a \ Fin ) -> ( x e. |^| F -> { x } e. F ) )
99 95 98 mtoi 
 |-  ( X e. ( Fin1a \ Fin ) -> -. x e. |^| F )
100 99 eq0rdv 
 |-  ( X e. ( Fin1a \ Fin ) -> |^| F = (/) )
101 91 100 jca 
 |-  ( X e. ( Fin1a \ Fin ) -> ( F e. ( UFil ` X ) /\ |^| F = (/) ) )