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 vsnex ⊢ { 𝑥 } ∈ 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 ineq2 ⊢ ( 𝑓 = 𝑥 → ( 𝑦 ∩ 𝑓 ) = ( 𝑦 ∩ 𝑥 ) )
27 26 neeq1d ⊢ ( 𝑓 = 𝑥 → ( ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) )
28 21 27 ralsn ⊢ ( ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) ≠ ∅ )
29 28 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ )
30 29 bilanri ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ )
31 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
32 31 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
33 simplr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ⊆ 𝑋 )
34 inss2 ⊢ ( 𝑋 ∩ 𝑥 ) ⊆ 𝑥
35 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
36 35 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑋 ∈ 𝐹 )
37 ineq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∩ 𝑥 ) = ( 𝑋 ∩ 𝑥 ) )
38 37 neeq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) )
39 38 rspcva ⊢ ( ( 𝑋 ∈ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝑋 ∩ 𝑥 ) ≠ ∅ )
40 36 39 sylan ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝑋 ∩ 𝑥 ) ≠ ∅ )
41 ssn0 ⊢ ( ( ( 𝑋 ∩ 𝑥 ) ⊆ 𝑥 ∧ ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ≠ ∅ )
42 34 40 41 sylancr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ≠ ∅ )
43 35 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑋 ∈ 𝐹 )
44 snfbas ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ ∅ ∧ 𝑋 ∈ 𝐹 ) → { 𝑥 } ∈ ( fBas ‘ 𝑋 ) )
45 33 42 43 44 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → { 𝑥 } ∈ ( fBas ‘ 𝑋 ) )
46 fbunfip ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ) )
47 32 45 46 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ) )
48 30 47 mpbird ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) )
49 fsubbas ⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
50 43 49 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
51 19 25 48 50 mpbir3and ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) )
52 ssfg ⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) )
53 51 52 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) )
54 13 53 sstrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) )
55 54 unssad ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) )
56 fgcl ⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
57 sseq2 ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
58 eqeq2 ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝐹 = 𝑓 ↔ 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
59 57 58 imbi12d ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ↔ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) )
60 59 rspcv ⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) )
61 51 56 60 3syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) )
62 55 61 mpid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
63 vsnid ⊢ 𝑥 ∈ { 𝑥 }
64 20 63 sselii ⊢ 𝑥 ∈ ( 𝐹 ∪ { 𝑥 } )
65 64 a1i ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ∈ ( 𝐹 ∪ { 𝑥 } ) )
66 54 65 sseldd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) )
67 eleq2 ⊢ ( 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) )
68 66 67 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝑥 ∈ 𝐹 ) )
69 62 68 syld ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → 𝑥 ∈ 𝐹 ) )
70 69 impancom ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → ( ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) )
71 70 an32s ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) )
72 71 con3d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) )
73 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐹 ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ )
74 nne ⊢ ( ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) = ∅ )
75 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
76 reldisj ⊢ ( 𝑦 ⊆ 𝑋 → ( ( 𝑦 ∩ 𝑥 ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
77 75 76 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑦 ∩ 𝑥 ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
78 difss ⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
79 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ∧ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 )
80 79 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) )
81 78 80 mpii ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
82 81 imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
83 77 82 sylbid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑦 ∩ 𝑥 ) = ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
84 74 83 biimtrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
85 84 rexlimdva ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐹 ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
86 73 85 biimtrrid ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
87 86 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
88 72 87 syld ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
89 88 orrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
90 7 89 sylan2b ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
91 90 ralrimiva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
92 isufil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
93 6 91 92 sylanbrc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
94 5 93 impbii ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) )