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 ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹𝑓𝐹 = 𝑓 ) ) )

Proof

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