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 
|- ( F e. ( Fil ` X ) -> |^| { f e. ( UFil ` X ) | F C_ f } = F )

Proof

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