uffixfr

Description: An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element A ), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	uffixfr	$⊢ F \in UFil (X) \to (A \in ⋂ F \leftrightarrow F = \{x \in 𝒫 X \| A \in x\})$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F \in UFil (X)$
2		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
3		filtop	$⊢ F \in Fil (X) \to X \in F$
4	2 3	syl	$⊢ F \in UFil (X) \to X \in F$
5		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
6		intssuni	$⊢ F \neq \emptyset \to ⋂ F \subseteq ⋃ F$
7	2 5 6	3syl	$⊢ F \in UFil (X) \to ⋂ F \subseteq ⋃ F$
8		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
9	2 8	syl	$⊢ F \in UFil (X) \to ⋃ F = X$
10	7 9	sseqtrd	$⊢ F \in UFil (X) \to ⋂ F \subseteq X$
11	10	sselda	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to A \in X$
12		uffix	$⊢ (X \in F \land A \in X) \to (\{\{A\}\} \in fBas (X) \land \{x \in 𝒫 X \| A \in x\} = X filGen \{\{A\}\})$
13	4 11 12	syl2an2r	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to (\{\{A\}\} \in fBas (X) \land \{x \in 𝒫 X \| A \in x\} = X filGen \{\{A\}\})$
14	13	simprd	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{x \in 𝒫 X \| A \in x\} = X filGen \{\{A\}\}$
15	13	simpld	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{\{A\}\} \in fBas (X)$
16		fgcl	$⊢ \{\{A\}\} \in fBas (X) \to X filGen \{\{A\}\} \in Fil (X)$
17	15 16	syl	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to X filGen \{\{A\}\} \in Fil (X)$
18	14 17	eqeltrd	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{x \in 𝒫 X \| A \in x\} \in Fil (X)$
19	2	adantr	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F \in Fil (X)$
20		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
21	19 20	syl	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F \subseteq 𝒫 X$
22		elintg	$⊢ A \in ⋂ F \to (A \in ⋂ F \leftrightarrow \forall x \in F A \in x)$
23	22	ibi	$⊢ A \in ⋂ F \to \forall x \in F A \in x$
24	23	adantl	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \forall x \in F A \in x$
25		ssrab	$⊢ F \subseteq \{x \in 𝒫 X \| A \in x\} \leftrightarrow (F \subseteq 𝒫 X \land \forall x \in F A \in x)$
26	21 24 25	sylanbrc	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F \subseteq \{x \in 𝒫 X \| A \in x\}$
27		ufilmax	$⊢ (F \in UFil (X) \land \{x \in 𝒫 X \| A \in x\} \in Fil (X) \land F \subseteq \{x \in 𝒫 X \| A \in x\}) \to F = \{x \in 𝒫 X \| A \in x\}$
28	1 18 26 27	syl3anc	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F = \{x \in 𝒫 X \| A \in x\}$
29		eqimss	$⊢ F = \{x \in 𝒫 X \| A \in x\} \to F \subseteq \{x \in 𝒫 X \| A \in x\}$
30	29	adantl	$⊢ (F \in UFil (X) \land F = \{x \in 𝒫 X \| A \in x\}) \to F \subseteq \{x \in 𝒫 X \| A \in x\}$
31	25	simprbi	$⊢ F \subseteq \{x \in 𝒫 X \| A \in x\} \to \forall x \in F A \in x$
32	30 31	syl	$⊢ (F \in UFil (X) \land F = \{x \in 𝒫 X \| A \in x\}) \to \forall x \in F A \in x$
33		eleq2	$⊢ F = \{x \in 𝒫 X \| A \in x\} \to (X \in F \leftrightarrow X \in \{x \in 𝒫 X \| A \in x\})$
34	33	biimpac	$⊢ (X \in F \land F = \{x \in 𝒫 X \| A \in x\}) \to X \in \{x \in 𝒫 X \| A \in x\}$
35	4 34	sylan	$⊢ (F \in UFil (X) \land F = \{x \in 𝒫 X \| A \in x\}) \to X \in \{x \in 𝒫 X \| A \in x\}$
36		eleq2	$⊢ x = X \to (A \in x \leftrightarrow A \in X)$
37	36	elrab	$⊢ X \in \{x \in 𝒫 X \| A \in x\} \leftrightarrow (X \in 𝒫 X \land A \in X)$
38	37	simprbi	$⊢ X \in \{x \in 𝒫 X \| A \in x\} \to A \in X$
39		elintg	$⊢ A \in X \to (A \in ⋂ F \leftrightarrow \forall x \in F A \in x)$
40	35 38 39	3syl	$⊢ (F \in UFil (X) \land F = \{x \in 𝒫 X \| A \in x\}) \to (A \in ⋂ F \leftrightarrow \forall x \in F A \in x)$
41	32 40	mpbird	$⊢ (F \in UFil (X) \land F = \{x \in 𝒫 X \| A \in x\}) \to A \in ⋂ F$
42	28 41	impbida	$⊢ F \in UFil (X) \to (A \in ⋂ F \leftrightarrow F = \{x \in 𝒫 X \| A \in x\})$

Metamath Proof Explorer

Theorem uffixfr

Proof