Metamath Proof Explorer

Theorem uffixsn

Description: The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	uffixsn	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{A\} \in F$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ x = \{A\} \to (A \in x \leftrightarrow A \in \{A\})$
2		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
3		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
4		intssuni	$⊢ F \neq \emptyset \to ⋂ F \subseteq ⋃ F$
5	2 3 4	3syl	$⊢ F \in UFil (X) \to ⋂ F \subseteq ⋃ F$
6		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
7	2 6	syl	$⊢ F \in UFil (X) \to ⋃ F = X$
8	5 7	sseqtrd	$⊢ F \in UFil (X) \to ⋂ F \subseteq X$
9	8	sselda	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to A \in X$
10	9	snssd	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{A\} \subseteq X$
11		snex	$⊢ \{A\} \in V$
12	11	elpw	$⊢ \{A\} \in 𝒫 X \leftrightarrow \{A\} \subseteq X$
13	10 12	sylibr	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{A\} \in 𝒫 X$
14		snidg	$⊢ A \in ⋂ F \to A \in \{A\}$
15	14	adantl	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to A \in \{A\}$
16	1 13 15	elrabd	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{A\} \in \{x \in 𝒫 X \| A \in x\}$
17		uffixfr	$⊢ F \in UFil (X) \to (A \in ⋂ F \leftrightarrow F = \{x \in 𝒫 X \| A \in x\})$
18	17	biimpa	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to F = \{x \in 𝒫 X \| A \in x\}$
19	16 18	eleqtrrd	$⊢ (F \in UFil (X) \land A \in ⋂ F) \to \{A\} \in F$