ufilen

Description: Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)

		Ref	Expression
	Assertion	ufilen	$⊢ ω ≼ X \to \exists f \in UFil (X) \forall x \in f x \approx X$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ ω ≼ X \to X \in V$
3		numth3	$⊢ X \in V \to X \in dom card$
4	2 3	syl	$⊢ ω ≼ X \to X \in dom card$
5		csdfil	$⊢ (X \in dom card \land ω ≼ X) \to \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \in Fil (X)$
6	4 5	mpancom	$⊢ ω ≼ X \to \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \in Fil (X)$
7		filssufil	$⊢ \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \in Fil (X) \to \exists f \in UFil (X) \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f$
8	6 7	syl	$⊢ ω ≼ X \to \exists f \in UFil (X) \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f$
9		elfvex	$⊢ f \in UFil (X) \to X \in V$
10	9	ad2antlr	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to X \in V$
11		ufilfil	$⊢ f \in UFil (X) \to f \in Fil (X)$
12		filelss	$⊢ (f \in Fil (X) \land x \in f) \to x \subseteq X$
13	11 12	sylan	$⊢ (f \in UFil (X) \land x \in f) \to x \subseteq X$
14	13	adantll	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to x \subseteq X$
15		ssdomg	$⊢ X \in V \to (x \subseteq X \to x ≼ X)$
16	10 14 15	sylc	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to x ≼ X$
17		filfbas	$⊢ f \in Fil (X) \to f \in fBas (X)$
18	11 17	syl	$⊢ f \in UFil (X) \to f \in fBas (X)$
19	18	adantl	$⊢ (ω ≼ X \land f \in UFil (X)) \to f \in fBas (X)$
20		fbncp	$⊢ (f \in fBas (X) \land x \in f) \to \neg X ∖ x \in f$
21	19 20	sylan	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to \neg X ∖ x \in f$
22		difeq2	$⊢ y = X ∖ x \to X ∖ y = X ∖ (X ∖ x)$
23	22	breq1d	$⊢ y = X ∖ x \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ (X ∖ x)) ≺ X)$
24		difss	$⊢ X ∖ x \subseteq X$
25		elpw2g	$⊢ X \in V \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
26	24 25	mpbiri	$⊢ X \in V \to X ∖ x \in 𝒫 X$
27	26	3ad2ant1	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to X ∖ x \in 𝒫 X$
28		simp2	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to x \subseteq X$
29		dfss4	$⊢ x \subseteq X \leftrightarrow X ∖ (X ∖ x) = x$
30	28 29	sylib	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to X ∖ (X ∖ x) = x$
31		simp3	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to x ≺ X$
32	30 31	eqbrtrd	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to (X ∖ (X ∖ x)) ≺ X$
33	23 27 32	elrabd	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to X ∖ x \in \{y \in 𝒫 X \| (X ∖ y) ≺ X\}$
34		ssel	$⊢ \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to (X ∖ x \in \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \to X ∖ x \in f)$
35	33 34	syl5com	$⊢ (X \in V \land x \subseteq X \land x ≺ X) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to X ∖ x \in f)$
36	35	3expa	$⊢ ((X \in V \land x \subseteq X) \land x ≺ X) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to X ∖ x \in f)$
37	36	impancom	$⊢ ((X \in V \land x \subseteq X) \land \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f) \to (x ≺ X \to X ∖ x \in f)$
38	37	con3d	$⊢ ((X \in V \land x \subseteq X) \land \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f) \to (\neg X ∖ x \in f \to \neg x ≺ X)$
39	38	impancom	$⊢ ((X \in V \land x \subseteq X) \land \neg X ∖ x \in f) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to \neg x ≺ X)$
40	10 14 21 39	syl21anc	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to \neg x ≺ X)$
41		bren2	$⊢ x \approx X \leftrightarrow (x ≼ X \land \neg x ≺ X)$
42	41	simplbi2	$⊢ x ≼ X \to (\neg x ≺ X \to x \approx X)$
43	16 40 42	sylsyld	$⊢ ((ω ≼ X \land f \in UFil (X)) \land x \in f) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to x \approx X)$
44	43	ralrimdva	$⊢ (ω ≼ X \land f \in UFil (X)) \to (\{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to \forall x \in f x \approx X)$
45	44	reximdva	$⊢ ω ≼ X \to (\exists f \in UFil (X) \{y \in 𝒫 X \| (X ∖ y) ≺ X\} \subseteq f \to \exists f \in UFil (X) \forall x \in f x \approx X)$
46	8 45	mpd	$⊢ ω ≼ X \to \exists f \in UFil (X) \forall x \in f x \approx X$

Metamath Proof Explorer

Theorem ufilen

Proof