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}=𝒫{X}\setminus \mathrm{Fin}$
Assertion fin1aufil ${⊢}{X}\in \left({\mathrm{Fin}}^{Ia}\setminus \mathrm{Fin}\right)\to \left({F}\in \mathrm{UFil}\left({X}\right)\wedge \bigcap {F}=\varnothing \right)$

Proof

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