ufilmax

Description: Any filter finer than an ultrafilter is actually equal to it. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

		Ref	Expression
	Assertion	ufilmax	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to F = G$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to F \subseteq G$
2		filelss	$⊢ (G \in Fil (X) \land x \in G) \to x \subseteq X$
3	2	ex	$⊢ G \in Fil (X) \to (x \in G \to x \subseteq X)$
4	3	3ad2ant2	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to (x \in G \to x \subseteq X)$
5		ufilb	$⊢ (F \in UFil (X) \land x \subseteq X) \to (\neg x \in F \leftrightarrow X ∖ x \in F)$
6	5	3ad2antl1	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (\neg x \in F \leftrightarrow X ∖ x \in F)$
7		simpl3	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to F \subseteq G$
8	7	sseld	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (X ∖ x \in F \to X ∖ x \in G)$
9		filfbas	$⊢ G \in Fil (X) \to G \in fBas (X)$
10		fbncp	$⊢ (G \in fBas (X) \land x \in G) \to \neg X ∖ x \in G$
11	10	ex	$⊢ G \in fBas (X) \to (x \in G \to \neg X ∖ x \in G)$
12	9 11	syl	$⊢ G \in Fil (X) \to (x \in G \to \neg X ∖ x \in G)$
13	12	con2d	$⊢ G \in Fil (X) \to (X ∖ x \in G \to \neg x \in G)$
14	13	3ad2ant2	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to (X ∖ x \in G \to \neg x \in G)$
15	14	adantr	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (X ∖ x \in G \to \neg x \in G)$
16	8 15	syld	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (X ∖ x \in F \to \neg x \in G)$
17	6 16	sylbid	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (\neg x \in F \to \neg x \in G)$
18	17	con4d	$⊢ ((F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \land x \subseteq X) \to (x \in G \to x \in F)$
19	18	ex	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to (x \subseteq X \to (x \in G \to x \in F))$
20	19	com23	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to (x \in G \to (x \subseteq X \to x \in F))$
21	4 20	mpdd	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to (x \in G \to x \in F)$
22	21	ssrdv	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to G \subseteq F$
23	1 22	eqssd	$⊢ (F \in UFil (X) \land G \in Fil (X) \land F \subseteq G) \to F = G$

Metamath Proof Explorer

Theorem ufilmax

Proof