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