cfinufil

Description: An ultrafilter is free iff it contains the Fréchet filter cfinfil as a subset. (Contributed by NM, 14-Jul-2008) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	cfinufil	$⊢ F \in UFil (X) \to (⋂ F = \emptyset \leftrightarrow \{x \in 𝒫 X \| X ∖ x \in Fin\} \subseteq F)$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
2		ufilb	$⊢ (F \in UFil (X) \land x \subseteq X) \to (\neg x \in F \leftrightarrow X ∖ x \in F)$
3	2	adantr	$⊢ ((F \in UFil (X) \land x \subseteq X) \land X ∖ x \in Fin) \to (\neg x \in F \leftrightarrow X ∖ x \in F)$
4		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
5	4	adantr	$⊢ (F \in UFil (X) \land x \subseteq X) \to F \in Fil (X)$
6		filfinnfr	$⊢ (F \in Fil (X) \land X ∖ x \in F \land X ∖ x \in Fin) \to ⋂ F \neq \emptyset$
7	6	3exp	$⊢ F \in Fil (X) \to (X ∖ x \in F \to (X ∖ x \in Fin \to ⋂ F \neq \emptyset))$
8	7	com23	$⊢ F \in Fil (X) \to (X ∖ x \in Fin \to (X ∖ x \in F \to ⋂ F \neq \emptyset))$
9	5 8	syl	$⊢ (F \in UFil (X) \land x \subseteq X) \to (X ∖ x \in Fin \to (X ∖ x \in F \to ⋂ F \neq \emptyset))$
10	9	imp	$⊢ ((F \in UFil (X) \land x \subseteq X) \land X ∖ x \in Fin) \to (X ∖ x \in F \to ⋂ F \neq \emptyset)$
11	3 10	sylbid	$⊢ ((F \in UFil (X) \land x \subseteq X) \land X ∖ x \in Fin) \to (\neg x \in F \to ⋂ F \neq \emptyset)$
12	11	necon4bd	$⊢ ((F \in UFil (X) \land x \subseteq X) \land X ∖ x \in Fin) \to (⋂ F = \emptyset \to x \in F)$
13	12	ex	$⊢ (F \in UFil (X) \land x \subseteq X) \to (X ∖ x \in Fin \to (⋂ F = \emptyset \to x \in F))$
14	13	com23	$⊢ (F \in UFil (X) \land x \subseteq X) \to (⋂ F = \emptyset \to (X ∖ x \in Fin \to x \in F))$
15	1 14	sylan2	$⊢ (F \in UFil (X) \land x \in 𝒫 X) \to (⋂ F = \emptyset \to (X ∖ x \in Fin \to x \in F))$
16	15	ralrimdva	$⊢ F \in UFil (X) \to (⋂ F = \emptyset \to \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F))$
17	4	adantr	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to F \in Fil (X)$
18		uffixsn	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to \{y\} \in F$
19		filelss	$⊢ (F \in Fil (X) \land \{y\} \in F) \to \{y\} \subseteq X$
20	17 18 19	syl2anc	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to \{y\} \subseteq X$
21		dfss4	$⊢ \{y\} \subseteq X \leftrightarrow X ∖ (X ∖ \{y\}) = \{y\}$
22	20 21	sylib	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to X ∖ (X ∖ \{y\}) = \{y\}$
23		snfi	$⊢ \{y\} \in Fin$
24	22 23	eqeltrdi	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to X ∖ (X ∖ \{y\}) \in Fin$
25		difss	$⊢ X ∖ \{y\} \subseteq X$
26		filtop	$⊢ F \in Fil (X) \to X \in F$
27		elpw2g	$⊢ X \in F \to (X ∖ \{y\} \in 𝒫 X \leftrightarrow X ∖ \{y\} \subseteq X)$
28	17 26 27	3syl	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (X ∖ \{y\} \in 𝒫 X \leftrightarrow X ∖ \{y\} \subseteq X)$
29	25 28	mpbiri	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to X ∖ \{y\} \in 𝒫 X$
30		difeq2	$⊢ x = X ∖ \{y\} \to X ∖ x = X ∖ (X ∖ \{y\})$
31	30	eleq1d	$⊢ x = X ∖ \{y\} \to (X ∖ x \in Fin \leftrightarrow X ∖ (X ∖ \{y\}) \in Fin)$
32		eleq1	$⊢ x = X ∖ \{y\} \to (x \in F \leftrightarrow X ∖ \{y\} \in F)$
33	31 32	imbi12d	$⊢ x = X ∖ \{y\} \to ((X ∖ x \in Fin \to x \in F) \leftrightarrow (X ∖ (X ∖ \{y\}) \in Fin \to X ∖ \{y\} \in F))$
34	33	rspcv	$⊢ X ∖ \{y\} \in 𝒫 X \to (\forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F) \to (X ∖ (X ∖ \{y\}) \in Fin \to X ∖ \{y\} \in F))$
35	29 34	syl	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (\forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F) \to (X ∖ (X ∖ \{y\}) \in Fin \to X ∖ \{y\} \in F))$
36	24 35	mpid	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (\forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F) \to X ∖ \{y\} \in F)$
37		ufilb	$⊢ (F \in UFil (X) \land \{y\} \subseteq X) \to (\neg \{y\} \in F \leftrightarrow X ∖ \{y\} \in F)$
38	20 37	syldan	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (\neg \{y\} \in F \leftrightarrow X ∖ \{y\} \in F)$
39	18	pm2.24d	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (\neg \{y\} \in F \to \neg y \in ⋂ F)$
40	38 39	sylbird	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (X ∖ \{y\} \in F \to \neg y \in ⋂ F)$
41	36 40	syld	$⊢ (F \in UFil (X) \land y \in ⋂ F) \to (\forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F) \to \neg y \in ⋂ F)$
42	41	impancom	$⊢ (F \in UFil (X) \land \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F)) \to (y \in ⋂ F \to \neg y \in ⋂ F)$
43	42	pm2.01d	$⊢ (F \in UFil (X) \land \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F)) \to \neg y \in ⋂ F$
44	43	eq0rdv	$⊢ (F \in UFil (X) \land \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F)) \to ⋂ F = \emptyset$
45	44	ex	$⊢ F \in UFil (X) \to (\forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F) \to ⋂ F = \emptyset)$
46	16 45	impbid	$⊢ F \in UFil (X) \to (⋂ F = \emptyset \leftrightarrow \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F))$
47		rabss	$⊢ \{x \in 𝒫 X \| X ∖ x \in Fin\} \subseteq F \leftrightarrow \forall x \in 𝒫 X (X ∖ x \in Fin \to x \in F)$
48	46 47	bitr4di	$⊢ F \in UFil (X) \to (⋂ F = \emptyset \leftrightarrow \{x \in 𝒫 X \| X ∖ x \in Fin\} \subseteq F)$

Metamath Proof Explorer

Theorem cfinufil

Proof