# Metamath Proof Explorer

## Theorem 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 \mathrm{UFil}\left({X}\right)↔\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \forall {f}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {f}\to {F}={f}\right)\right)$

### Proof

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