isufil2

Description: The maximal property of an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	isufil2	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f))$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
2		ufilmax	$⊢ (F \in UFil (X) \land f \in Fil (X) \land F \subseteq f) \to F = f$
3	2	3expia	$⊢ (F \in UFil (X) \land f \in Fil (X)) \to (F \subseteq f \to F = f)$
4	3	ralrimiva	$⊢ F \in UFil (X) \to \forall f \in Fil (X) (F \subseteq f \to F = f)$
5	1 4	jca	$⊢ F \in UFil (X) \to (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f))$
6		simpl	$⊢ (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \to F \in Fil (X)$
7		velpw	$⊢ x \in 𝒫 X \leftrightarrow x \subseteq X$
8		simpll	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \in Fil (X)$
9		vsnex	$⊢ \{x\} \in V$
10		unexg	$⊢ (F \in Fil (X) \land \{x\} \in V) \to F \cup \{x\} \in V$
11	8 9 10	sylancl	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \cup \{x\} \in V$
12		ssfii	$⊢ F \cup \{x\} \in V \to F \cup \{x\} \subseteq fi (F \cup \{x\})$
13	11 12	syl	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \cup \{x\} \subseteq fi (F \cup \{x\})$
14		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
15	14	ad2antrr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \subseteq 𝒫 X$
16	7	biimpri	$⊢ x \subseteq X \to x \in 𝒫 X$
17	16	ad2antlr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \in 𝒫 X$
18	17	snssd	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \{x\} \subseteq 𝒫 X$
19	15 18	unssd	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \cup \{x\} \subseteq 𝒫 X$
20		ssun2	$⊢ \{x\} \subseteq F \cup \{x\}$
21		vex	$⊢ x \in V$
22	21	snnz	$⊢ \{x\} \neq \emptyset$
23		ssn0	$⊢ (\{x\} \subseteq F \cup \{x\} \land \{x\} \neq \emptyset) \to F \cup \{x\} \neq \emptyset$
24	20 22 23	mp2an	$⊢ F \cup \{x\} \neq \emptyset$
25	24	a1i	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \cup \{x\} \neq \emptyset$
26		ineq2	$⊢ f = x \to y \cap f = y \cap x$
27	26	neeq1d	$⊢ f = x \to (y \cap f \neq \emptyset \leftrightarrow y \cap x \neq \emptyset)$
28	21 27	ralsn	$⊢ \forall f \in \{x\} y \cap f \neq \emptyset \leftrightarrow y \cap x \neq \emptyset$
29	28	ralbii	$⊢ \forall y \in F \forall f \in \{x\} y \cap f \neq \emptyset \leftrightarrow \forall y \in F y \cap x \neq \emptyset$
30	29	bilanri	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \forall y \in F \forall f \in \{x\} y \cap f \neq \emptyset$
31		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
32	31	ad2antrr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \in fBas (X)$
33		simplr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \subseteq X$
34		inss2	$⊢ X \cap x \subseteq x$
35		filtop	$⊢ F \in Fil (X) \to X \in F$
36	35	adantr	$⊢ (F \in Fil (X) \land x \subseteq X) \to X \in F$
37		ineq1	$⊢ y = X \to y \cap x = X \cap x$
38	37	neeq1d	$⊢ y = X \to (y \cap x \neq \emptyset \leftrightarrow X \cap x \neq \emptyset)$
39	38	rspcva	$⊢ (X \in F \land \forall y \in F y \cap x \neq \emptyset) \to X \cap x \neq \emptyset$
40	36 39	sylan	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to X \cap x \neq \emptyset$
41		ssn0	$⊢ (X \cap x \subseteq x \land X \cap x \neq \emptyset) \to x \neq \emptyset$
42	34 40 41	sylancr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \neq \emptyset$
43	35	ad2antrr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to X \in F$
44		snfbas	$⊢ (x \subseteq X \land x \neq \emptyset \land X \in F) \to \{x\} \in fBas (X)$
45	33 42 43 44	syl3anc	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \{x\} \in fBas (X)$
46		fbunfip	$⊢ (F \in fBas (X) \land \{x\} \in fBas (X)) \to (\neg \emptyset \in fi (F \cup \{x\}) \leftrightarrow \forall y \in F \forall f \in \{x\} y \cap f \neq \emptyset)$
47	32 45 46	syl2anc	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (\neg \emptyset \in fi (F \cup \{x\}) \leftrightarrow \forall y \in F \forall f \in \{x\} y \cap f \neq \emptyset)$
48	30 47	mpbird	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \neg \emptyset \in fi (F \cup \{x\})$
49		fsubbas	$⊢ X \in F \to (fi (F \cup \{x\}) \in fBas (X) \leftrightarrow (F \cup \{x\} \subseteq 𝒫 X \land F \cup \{x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{x\})))$
50	43 49	syl	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (fi (F \cup \{x\}) \in fBas (X) \leftrightarrow (F \cup \{x\} \subseteq 𝒫 X \land F \cup \{x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{x\})))$
51	19 25 48 50	mpbir3and	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to fi (F \cup \{x\}) \in fBas (X)$
52		ssfg	$⊢ fi (F \cup \{x\}) \in fBas (X) \to fi (F \cup \{x\}) \subseteq X filGen fi (F \cup \{x\})$
53	51 52	syl	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to fi (F \cup \{x\}) \subseteq X filGen fi (F \cup \{x\})$
54	13 53	sstrd	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \cup \{x\} \subseteq X filGen fi (F \cup \{x\})$
55	54	unssad	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \subseteq X filGen fi (F \cup \{x\})$
56		fgcl	$⊢ fi (F \cup \{x\}) \in fBas (X) \to X filGen fi (F \cup \{x\}) \in Fil (X)$
57		sseq2	$⊢ f = X filGen fi (F \cup \{x\}) \to (F \subseteq f \leftrightarrow F \subseteq X filGen fi (F \cup \{x\}))$
58		eqeq2	$⊢ f = X filGen fi (F \cup \{x\}) \to (F = f \leftrightarrow F = X filGen fi (F \cup \{x\}))$
59	57 58	imbi12d	$⊢ f = X filGen fi (F \cup \{x\}) \to ((F \subseteq f \to F = f) \leftrightarrow (F \subseteq X filGen fi (F \cup \{x\}) \to F = X filGen fi (F \cup \{x\})))$
60	59	rspcv	$⊢ X filGen fi (F \cup \{x\}) \in Fil (X) \to (\forall f \in Fil (X) (F \subseteq f \to F = f) \to (F \subseteq X filGen fi (F \cup \{x\}) \to F = X filGen fi (F \cup \{x\})))$
61	51 56 60	3syl	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (\forall f \in Fil (X) (F \subseteq f \to F = f) \to (F \subseteq X filGen fi (F \cup \{x\}) \to F = X filGen fi (F \cup \{x\})))$
62	55 61	mpid	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (\forall f \in Fil (X) (F \subseteq f \to F = f) \to F = X filGen fi (F \cup \{x\}))$
63		vsnid	$⊢ x \in \{x\}$
64	20 63	sselii	$⊢ x \in (F \cup \{x\})$
65	64	a1i	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \in (F \cup \{x\})$
66	54 65	sseldd	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \in (X filGen fi (F \cup \{x\}))$
67		eleq2	$⊢ F = X filGen fi (F \cup \{x\}) \to (x \in F \leftrightarrow x \in (X filGen fi (F \cup \{x\})))$
68	66 67	syl5ibrcom	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (F = X filGen fi (F \cup \{x\}) \to x \in F)$
69	62 68	syld	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to (\forall f \in Fil (X) (F \subseteq f \to F = f) \to x \in F)$
70	69	impancom	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \to (\forall y \in F y \cap x \neq \emptyset \to x \in F)$
71	70	an32s	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \subseteq X) \to (\forall y \in F y \cap x \neq \emptyset \to x \in F)$
72	71	con3d	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \subseteq X) \to (\neg x \in F \to \neg \forall y \in F y \cap x \neq \emptyset)$
73		rexnal	$⊢ \exists y \in F \neg y \cap x \neq \emptyset \leftrightarrow \neg \forall y \in F y \cap x \neq \emptyset$
74		nne	$⊢ \neg y \cap x \neq \emptyset \leftrightarrow y \cap x = \emptyset$
75		filelss	$⊢ (F \in Fil (X) \land y \in F) \to y \subseteq X$
76		reldisj	$⊢ y \subseteq X \to (y \cap x = \emptyset \leftrightarrow y \subseteq X ∖ x)$
77	75 76	syl	$⊢ (F \in Fil (X) \land y \in F) \to (y \cap x = \emptyset \leftrightarrow y \subseteq X ∖ x)$
78		difss	$⊢ X ∖ x \subseteq X$
79		filss	$⊢ (F \in Fil (X) \land (y \in F \land X ∖ x \subseteq X \land y \subseteq X ∖ x)) \to X ∖ x \in F$
80	79	3exp2	$⊢ F \in Fil (X) \to (y \in F \to (X ∖ x \subseteq X \to (y \subseteq X ∖ x \to X ∖ x \in F)))$
81	78 80	mpii	$⊢ F \in Fil (X) \to (y \in F \to (y \subseteq X ∖ x \to X ∖ x \in F))$
82	81	imp	$⊢ (F \in Fil (X) \land y \in F) \to (y \subseteq X ∖ x \to X ∖ x \in F)$
83	77 82	sylbid	$⊢ (F \in Fil (X) \land y \in F) \to (y \cap x = \emptyset \to X ∖ x \in F)$
84	74 83	biimtrid	$⊢ (F \in Fil (X) \land y \in F) \to (\neg y \cap x \neq \emptyset \to X ∖ x \in F)$
85	84	rexlimdva	$⊢ F \in Fil (X) \to (\exists y \in F \neg y \cap x \neq \emptyset \to X ∖ x \in F)$
86	73 85	biimtrrid	$⊢ F \in Fil (X) \to (\neg \forall y \in F y \cap x \neq \emptyset \to X ∖ x \in F)$
87	86	ad2antrr	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \subseteq X) \to (\neg \forall y \in F y \cap x \neq \emptyset \to X ∖ x \in F)$
88	72 87	syld	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \subseteq X) \to (\neg x \in F \to X ∖ x \in F)$
89	88	orrd	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \subseteq X) \to (x \in F \lor X ∖ x \in F)$
90	7 89	sylan2b	$⊢ ((F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \land x \in 𝒫 X) \to (x \in F \lor X ∖ x \in F)$
91	90	ralrimiva	$⊢ (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \to \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F)$
92		isufil	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F))$
93	6 91 92	sylanbrc	$⊢ (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \to F \in UFil (X)$
94	5 93	impbii	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f))$

Metamath Proof Explorer

Theorem isufil2

Proof