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

Metamath Proof Explorer

Theorem filufint

Description: A filter is equal to the intersection of the ultrafilters containing it. (Contributed by Jeff Hankins, 1-Jan-2010) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filufint ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } = 𝐹 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 elintrab ⊢ ( 𝑥 ∈ ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓 ) )
3 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
4 3 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
5 difss ⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
6 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
7 6 difexd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ V )
8 7 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ V )
9 elpwg ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
10 8 9 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
11 5 10 mpbiri ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
12 11 snssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ 𝒫 𝑋 )
13 4 12 unssd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 )
14 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } )
15 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
16 ssn0 ⊢ ( ( 𝐹 ⊆ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∧ 𝐹 ≠ ∅ ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ )
17 14 15 16 sylancr ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ )
18 17 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ )
19 elsni ⊢ ( 𝑧 ∈ { ( 𝑋 ∖ 𝑥 ) } → 𝑧 = ( 𝑋 ∖ 𝑥 ) )
20 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
21 20 3adant3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝑦 ⊆ 𝑋 )
22 reldisj ⊢ ( 𝑦 ⊆ 𝑋 → ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ) )
23 21 22 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ) )
24 dfss4 ⊢ ( 𝑥 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
25 24 biimpi ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
26 25 sseq2d ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑦 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ↔ 𝑦 ⊆ 𝑥 ) )
27 26 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑦 ⊆ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ↔ 𝑦 ⊆ 𝑥 ) )
28 23 27 bitrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ ↔ 𝑦 ⊆ 𝑥 ) )
29 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐹 )
30 29 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )
31 30 3imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
32 28 31 sylbid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ → 𝑥 ∈ 𝐹 ) )
33 32 necon3bd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) )
34 33 3exp ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) ) ) )
35 34 com24 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( 𝑦 ∈ 𝐹 → ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) ) ) )
36 35 3imp1 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ )
37 ineq2 ⊢ ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑦 ∩ 𝑧 ) = ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) )
38 37 neeq1d ⊢ ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( ( 𝑦 ∩ 𝑧 ) ≠ ∅ ↔ ( 𝑦 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) )
39 36 38 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
40 39 expimpd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ∈ 𝐹 ∧ 𝑧 = ( 𝑋 ∖ 𝑥 ) ) → ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
41 19 40 sylan2i ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { ( 𝑋 ∖ 𝑥 ) } ) → ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
42 41 ralrimivv ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑦 ∩ 𝑧 ) ≠ ∅ )
43 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
44 43 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
45 5 a1i ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 )
46 25 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) = ∅ ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
47 difeq2 ⊢ ( ( 𝑋 ∖ 𝑥 ) = ∅ → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = ( 𝑋 ∖ ∅ ) )
48 dif0 ⊢ ( 𝑋 ∖ ∅ ) = 𝑋
49 47 48 eqtrdi ⊢ ( ( 𝑋 ∖ 𝑥 ) = ∅ → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑋 )
50 49 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) = ∅ ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑋 )
51 46 50 eqtr3d ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) = ∅ ) → 𝑥 = 𝑋 )
52 6 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) = ∅ ) → 𝑋 ∈ 𝐹 )
53 51 52 eqeltrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) = ∅ ) → 𝑥 ∈ 𝐹 )
54 53 3expia ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) = ∅ → 𝑥 ∈ 𝐹 ) )
55 54 necon3bd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ≠ ∅ ) )
56 55 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ≠ ∅ ) ) )
57 56 com23 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( 𝑋 ∖ 𝑥 ) ≠ ∅ ) ) )
58 57 3imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ≠ ∅ )
59 6 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝑋 ∈ 𝐹 )
60 snfbas ⊢ ( ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) ≠ ∅ ∧ 𝑋 ∈ 𝐹 ) → { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) )
61 45 58 59 60 syl3anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) )
62 fbunfip ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
63 44 61 62 syl2anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
64 42 63 mpbird ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
65 fsubbas ⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ) )
66 6 65 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ) )
67 66 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ) )
68 13 18 64 67 mpbir3and ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) )
69 fgcl ⊢ ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
70 68 69 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
71 filssufil ⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 )
72 snex ⊢ { ( 𝑋 ∖ 𝑥 ) } ∈ V
73 unexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ { ( 𝑋 ∖ 𝑥 ) } ∈ V ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V )
74 72 73 mpan2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V )
75 ssfii ⊢ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
76 74 75 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
77 76 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
78 77 unssad ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
79 ssfg ⊢ ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
80 68 79 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
81 78 80 sstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
82 81 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
83 simpr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 )
84 82 83 sstrd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → 𝐹 ⊆ 𝑓 )
85 ufilfil ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
86 0nelfil ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝑓 )
87 85 86 syl ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ¬ ∅ ∈ 𝑓 )
88 87 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ¬ ∅ ∈ 𝑓 )
89 disjdif ⊢ ( 𝑥 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅
90 85 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
91 simprr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → 𝑥 ∈ 𝑓 )
92 76 unssbd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
93 92 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
94 93 adantr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
95 68 adantr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) )
96 95 79 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
97 94 96 sstrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
98 97 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
99 simprl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 )
100 98 99 sstrd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ 𝑓 )
101 snidg ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
102 7 101 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
103 102 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
104 103 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
105 100 104 sseldd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 )
106 filin ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ∧ ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) → ( 𝑥 ∩ ( 𝑋 ∖ 𝑥 ) ) ∈ 𝑓 )
107 90 91 105 106 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → ( 𝑥 ∩ ( 𝑋 ∖ 𝑥 ) ) ∈ 𝑓 )
108 89 107 eqeltrrid ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓 ) ) → ∅ ∈ 𝑓 )
109 108 expr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝑥 ∈ 𝑓 → ∅ ∈ 𝑓 ) )
110 88 109 mtod ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ¬ 𝑥 ∈ 𝑓 )
111 84 110 jca ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) )
112 111 exp31 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) ) )
113 112 reximdvai ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
114 71 113 syl5 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
115 70 114 mpd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) )
116 115 3expia ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ) → ( 𝑥 ⊆ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
117 filssufil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
118 filelss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ⊆ 𝑋 )
119 118 ex ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
120 85 119 syl ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
121 120 con3d ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ( ¬ 𝑥 ⊆ 𝑋 → ¬ 𝑥 ∈ 𝑓 ) )
122 121 impcom ⊢ ( ( ¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ¬ 𝑥 ∈ 𝑓 )
123 122 a1d ⊢ ( ( ¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑓 → ¬ 𝑥 ∈ 𝑓 ) )
124 123 ancld ⊢ ( ( ¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑓 → ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
125 124 reximdva ⊢ ( ¬ 𝑥 ⊆ 𝑋 → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
126 117 125 syl5com ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ 𝑥 ⊆ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
127 126 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ) → ( ¬ 𝑥 ⊆ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
128 116 127 pm2.61d ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝐹 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) )
129 128 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ) )
130 rexanali ⊢ ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓 ) ↔ ¬ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓 ) )
131 129 130 imbitrdi ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓 ) ) )
132 131 con4d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓 ) → 𝑥 ∈ 𝐹 ) )
133 2 132 biimtrid ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } → 𝑥 ∈ 𝐹 ) )
134 133 ssrdv ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } ⊆ 𝐹 )
135 ssintub ⊢ 𝐹 ⊆ ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 }
136 135 a1i ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } )
137 134 136 eqssd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∩ { 𝑓 ∈ ( UFil ‘ 𝑋 ) ∣ 𝐹 ⊆ 𝑓 } = 𝐹 )