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 ∖ Fin$
	Assertion	fin1aufil	$⊢ X \in ({Fin}^{Ia} ∖ Fin) \to (F \in UFil (X) \land ⋂ F = \emptyset)$

Proof

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

Metamath Proof Explorer

Theorem fin1aufil

Proof