This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 biimtrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
86 85 rexlimdva ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐹 ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
87 74 86 biimtrrid ⊢ ( 𝐹 ∈ ( 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 ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) )