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		simpr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \forall y \in F y \cap x \neq \emptyset$
27		ineq2	$⊢ f = x \to y \cap f = y \cap x$
28	27	neeq1d	$⊢ f = x \to (y \cap f \neq \emptyset \leftrightarrow y \cap x \neq \emptyset)$
29	21 28	ralsn	$⊢ \forall f \in \{x\} y \cap f \neq \emptyset \leftrightarrow y \cap x \neq \emptyset$
30	29	ralbii	$⊢ \forall y \in F \forall f \in \{x\} y \cap f \neq \emptyset \leftrightarrow \forall y \in F y \cap x \neq \emptyset$
31	26 30	sylibr	$⊢ ((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$
32		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
33	32	ad2antrr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to F \in fBas (X)$
34		simplr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \subseteq X$
35		inss2	$⊢ X \cap x \subseteq x$
36		filtop	$⊢ F \in Fil (X) \to X \in F$
37	36	adantr	$⊢ (F \in Fil (X) \land x \subseteq X) \to X \in F$
38		ineq1	$⊢ y = X \to y \cap x = X \cap x$
39	38	neeq1d	$⊢ y = X \to (y \cap x \neq \emptyset \leftrightarrow X \cap x \neq \emptyset)$
40	39	rspcva	$⊢ (X \in F \land \forall y \in F y \cap x \neq \emptyset) \to X \cap x \neq \emptyset$
41	37 40	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$
42		ssn0	$⊢ (X \cap x \subseteq x \land X \cap x \neq \emptyset) \to x \neq \emptyset$
43	35 41 42	sylancr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to x \neq \emptyset$
44	36	ad2antrr	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to X \in F$
45		snfbas	$⊢ (x \subseteq X \land x \neq \emptyset \land X \in F) \to \{x\} \in fBas (X)$
46	34 43 44 45	syl3anc	$⊢ ((F \in Fil (X) \land x \subseteq X) \land \forall y \in F y \cap x \neq \emptyset) \to \{x\} \in fBas (X)$
47		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)$
48	33 46 47	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)$
49	31 48	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\})$
50		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\})))$
51	44 50	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\})))$
52	19 25 49 51	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)$
53		ssfg	$⊢ fi (F \cup \{x\}) \in fBas (X) \to fi (F \cup \{x\}) \subseteq X filGen fi (F \cup \{x\})$
54	52 53	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\})$
55	13 54	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\})$
56	55	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\})$
57		fgcl	$⊢ fi (F \cup \{x\}) \in fBas (X) \to X filGen fi (F \cup \{x\}) \in Fil (X)$
58		sseq2	$⊢ f = X filGen fi (F \cup \{x\}) \to (F \subseteq f \leftrightarrow F \subseteq X filGen fi (F \cup \{x\}))$
59		eqeq2	$⊢ f = X filGen fi (F \cup \{x\}) \to (F = f \leftrightarrow F = X filGen fi (F \cup \{x\}))$
60	58 59	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\})))$
61	60	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\})))$
62	52 57 61	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\})))$
63	56 62	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\}))$
64		vsnid	$⊢ x \in \{x\}$
65	20 64	sselii	$⊢ x \in (F \cup \{x\})$
66	65	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\})$
67	55 66	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\}))$
68		eleq2	$⊢ F = X filGen fi (F \cup \{x\}) \to (x \in F \leftrightarrow x \in (X filGen fi (F \cup \{x\})))$
69	67 68	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)$
70	63 69	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)$
71	70	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)$
72	71	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)$
73	72	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)$
74		rexnal	$⊢ \exists y \in F \neg y \cap x \neq \emptyset \leftrightarrow \neg \forall y \in F y \cap x \neq \emptyset$
75		nne	$⊢ \neg y \cap x \neq \emptyset \leftrightarrow y \cap x = \emptyset$
76		filelss	$⊢ (F \in Fil (X) \land y \in F) \to y \subseteq X$
77		reldisj	$⊢ y \subseteq X \to (y \cap x = \emptyset \leftrightarrow y \subseteq X ∖ x)$
78	76 77	syl	$⊢ (F \in Fil (X) \land y \in F) \to (y \cap x = \emptyset \leftrightarrow y \subseteq X ∖ x)$
79		difss	$⊢ X ∖ x \subseteq X$
80		filss	$⊢ (F \in Fil (X) \land (y \in F \land X ∖ x \subseteq X \land y \subseteq X ∖ x)) \to X ∖ x \in F$
81	80	3exp2	$⊢ F \in Fil (X) \to (y \in F \to (X ∖ x \subseteq X \to (y \subseteq X ∖ x \to X ∖ x \in F)))$
82	79 81	mpii	$⊢ F \in Fil (X) \to (y \in F \to (y \subseteq X ∖ x \to X ∖ x \in F))$
83	82	imp	$⊢ (F \in Fil (X) \land y \in F) \to (y \subseteq X ∖ x \to X ∖ x \in F)$
84	78 83	sylbid	$⊢ (F \in Fil (X) \land y \in F) \to (y \cap x = \emptyset \to X ∖ x \in F)$
85	75 84	biimtrid	$⊢ (F \in Fil (X) \land y \in F) \to (\neg y \cap x \neq \emptyset \to X ∖ x \in F)$
86	85	rexlimdva	$⊢ F \in Fil (X) \to (\exists y \in F \neg y \cap x \neq \emptyset \to X ∖ x \in F)$
87	74 86	biimtrrid	$⊢ F \in Fil (X) \to (\neg \forall y \in F y \cap x \neq \emptyset \to X ∖ x \in F)$
88	87	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)$
89	73 88	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)$
90	89	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)$
91	7 90	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)$
92	91	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)$
93		isufil	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F))$
94	6 92 93	sylanbrc	$⊢ (F \in Fil (X) \land \forall f \in Fil (X) (F \subseteq f \to F = f)) \to F \in UFil (X)$
95	5 94	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