This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ufildom1

Description: An ultrafilter is generated by at most one element (because free ultrafilters have no generators and fixed ultrafilters have exactly one). (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	ufildom1	$⊢ F \in UFil (X) \to ⋂ F ≼ 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ ⋂ F = \emptyset \to (⋂ F ≼ 1_{𝑜} \leftrightarrow \emptyset ≼ 1_{𝑜})$
2		uffixsn	$⊢ (F \in UFil (X) \land x \in ⋂ F) \to \{x\} \in F$
3		intss1	$⊢ \{x\} \in F \to ⋂ F \subseteq \{x\}$
4	2 3	syl	$⊢ (F \in UFil (X) \land x \in ⋂ F) \to ⋂ F \subseteq \{x\}$
5		simpr	$⊢ (F \in UFil (X) \land x \in ⋂ F) \to x \in ⋂ F$
6	5	snssd	$⊢ (F \in UFil (X) \land x \in ⋂ F) \to \{x\} \subseteq ⋂ F$
7	4 6	eqssd	$⊢ (F \in UFil (X) \land x \in ⋂ F) \to ⋂ F = \{x\}$
8	7	ex	$⊢ F \in UFil (X) \to (x \in ⋂ F \to ⋂ F = \{x\})$
9	8	eximdv	$⊢ F \in UFil (X) \to (\exists x x \in ⋂ F \to \exists x ⋂ F = \{x\})$
10		n0	$⊢ ⋂ F \neq \emptyset \leftrightarrow \exists x x \in ⋂ F$
11		en1	$⊢ ⋂ F \approx 1_{𝑜} \leftrightarrow \exists x ⋂ F = \{x\}$
12	9 10 11	3imtr4g	$⊢ F \in UFil (X) \to (⋂ F \neq \emptyset \to ⋂ F \approx 1_{𝑜})$
13	12	imp	$⊢ (F \in UFil (X) \land ⋂ F \neq \emptyset) \to ⋂ F \approx 1_{𝑜}$
14		endom	$⊢ ⋂ F \approx 1_{𝑜} \to ⋂ F ≼ 1_{𝑜}$
15	13 14	syl	$⊢ (F \in UFil (X) \land ⋂ F \neq \emptyset) \to ⋂ F ≼ 1_{𝑜}$
16		1on	$⊢ 1_{𝑜} \in On$
17		0domg	$⊢ 1_{𝑜} \in On \to \emptyset ≼ 1_{𝑜}$
18	16 17	mp1i	$⊢ F \in UFil (X) \to \emptyset ≼ 1_{𝑜}$
19	1 15 18	pm2.61ne	$⊢ F \in UFil (X) \to ⋂ F ≼ 1_{𝑜}$