uffix2

Description: A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	uffix2	$⊢ F \in UFil (X) \to (⋂ F \neq \emptyset \leftrightarrow \exists x \in X F = \{y \in 𝒫 X \| x \in y\})$

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
2		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
3		intssuni	$⊢ F \neq \emptyset \to ⋂ F \subseteq ⋃ F$
4	1 2 3	3syl	$⊢ F \in UFil (X) \to ⋂ F \subseteq ⋃ F$
5		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
6	1 5	syl	$⊢ F \in UFil (X) \to ⋃ F = X$
7	4 6	sseqtrd	$⊢ F \in UFil (X) \to ⋂ F \subseteq X$
8	7	sseld	$⊢ F \in UFil (X) \to (x \in ⋂ F \to x \in X)$
9	8	pm4.71rd	$⊢ F \in UFil (X) \to (x \in ⋂ F \leftrightarrow (x \in X \land x \in ⋂ F))$
10		uffixfr	$⊢ F \in UFil (X) \to (x \in ⋂ F \leftrightarrow F = \{y \in 𝒫 X \| x \in y\})$
11	10	anbi2d	$⊢ F \in UFil (X) \to ((x \in X \land x \in ⋂ F) \leftrightarrow (x \in X \land F = \{y \in 𝒫 X \| x \in y\}))$
12	9 11	bitrd	$⊢ F \in UFil (X) \to (x \in ⋂ F \leftrightarrow (x \in X \land F = \{y \in 𝒫 X \| x \in y\}))$
13	12	exbidv	$⊢ F \in UFil (X) \to (\exists x x \in ⋂ F \leftrightarrow \exists x (x \in X \land F = \{y \in 𝒫 X \| x \in y\}))$
14		n0	$⊢ ⋂ F \neq \emptyset \leftrightarrow \exists x x \in ⋂ F$
15		df-rex	$⊢ \exists x \in X F = \{y \in 𝒫 X \| x \in y\} \leftrightarrow \exists x (x \in X \land F = \{y \in 𝒫 X \| x \in y\})$
16	13 14 15	3bitr4g	$⊢ F \in UFil (X) \to (⋂ F \neq \emptyset \leftrightarrow \exists x \in X F = \{y \in 𝒫 X \| x \in y\})$

Metamath Proof Explorer