Metamath Proof Explorer

Theorem ufileu

Description: If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion ufileu 
|- ( F e. ( Fil ` X ) -> ( F e. ( UFil ` X ) <-> E! f e. ( UFil ` X ) F C_ f ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( f e. ( UFil ` X ) -> f e. ( Fil ` X ) )
2 ufilmax 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) /\ F C_ f ) -> F = f )
3 2 3expa 
 |-  ( ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) ) /\ F C_ f ) -> F = f )
4 3 eqcomd 
 |-  ( ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) ) /\ F C_ f ) -> f = F )
5 4 ex 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) ) -> ( F C_ f -> f = F ) )
6 1 5 sylan2 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( UFil ` X ) ) -> ( F C_ f -> f = F ) )
7 6 ralrimiva 
 |-  ( F e. ( UFil ` X ) -> A. f e. ( UFil ` X ) ( F C_ f -> f = F ) )
8 ssid 
 |-  F C_ F
9 sseq2 
 |-  ( f = F -> ( F C_ f <-> F C_ F ) )
10 9 eqreu 
 |-  ( ( F e. ( UFil ` X ) /\ F C_ F /\ A. f e. ( UFil ` X ) ( F C_ f -> f = F ) ) -> E! f e. ( UFil ` X ) F C_ f )
11 8 10 mp3an2 
 |-  ( ( F e. ( UFil ` X ) /\ A. f e. ( UFil ` X ) ( F C_ f -> f = F ) ) -> E! f e. ( UFil ` X ) F C_ f )
12 7 11 mpdan 
 |-  ( F e. ( UFil ` X ) -> E! f e. ( UFil ` X ) F C_ f )
13 reu6 
 |-  ( E! f e. ( UFil ` X ) F C_ f <-> E. g e. ( UFil ` X ) A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) )
14 ibibr 
 |-  ( ( f = g -> F C_ f ) <-> ( f = g -> ( F C_ f <-> f = g ) ) )
15 14 pm5.74ri 
 |-  ( f = g -> ( F C_ f <-> ( F C_ f <-> f = g ) ) )
16 sseq2 
 |-  ( f = g -> ( F C_ f <-> F C_ g ) )
17 15 16 bitr3d 
 |-  ( f = g -> ( ( F C_ f <-> f = g ) <-> F C_ g ) )
18 17 rspcva 
 |-  ( ( g e. ( UFil ` X ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F C_ g )
19 18 adantll 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F C_ g )
20 ufilfil 
 |-  ( g e. ( UFil ` X ) -> g e. ( Fil ` X ) )
21 filelss 
 |-  ( ( g e. ( Fil ` X ) /\ x e. g ) -> x C_ X )
22 21 ex 
 |-  ( g e. ( Fil ` X ) -> ( x e. g -> x C_ X ) )
23 20 22 syl 
 |-  ( g e. ( UFil ` X ) -> ( x e. g -> x C_ X ) )
24 23 ad2antlr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> ( x e. g -> x C_ X ) )
25 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
26 25 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F C_ ~P X )
27 difss 
 |-  ( X \ x ) C_ X
28 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
29 28 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> X e. F )
30 difexg 
 |-  ( X e. F -> ( X \ x ) e. _V )
31 29 30 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. _V )
32 elpwg 
 |-  ( ( X \ x ) e. _V -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
33 31 32 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
34 27 33 mpbiri 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ~P X )
35 34 snssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> { ( X \ x ) } C_ ~P X )
36 26 35 unssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) C_ ~P X )
37 ssun1 
 |-  F C_ ( F u. { ( X \ x ) } )
38 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
39 38 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F =/= (/) )
40 ssn0 
 |-  ( ( F C_ ( F u. { ( X \ x ) } ) /\ F =/= (/) ) -> ( F u. { ( X \ x ) } ) =/= (/) )
41 37 39 40 sylancr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) =/= (/) )
42 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ f e. F ) -> f C_ X )
43 42 ad2ant2rl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> f C_ X )
44 df-ss 
 |-  ( f C_ X <-> ( f i^i X ) = f )
45 43 44 sylib 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( f i^i X ) = f )
46 45 sseq1d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( ( f i^i X ) C_ x <-> f C_ x ) )
47 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( f e. F /\ x C_ X /\ f C_ x ) ) -> x e. F )
48 47 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( f e. F -> ( x C_ X -> ( f C_ x -> x e. F ) ) ) )
49 48 impcomd 
 |-  ( F e. ( Fil ` X ) -> ( ( x C_ X /\ f e. F ) -> ( f C_ x -> x e. F ) ) )
50 49 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) -> ( ( x C_ X /\ f e. F ) -> ( f C_ x -> x e. F ) ) )
51 50 imp 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( f C_ x -> x e. F ) )
52 46 51 sylbid 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( ( f i^i X ) C_ x -> x e. F ) )
53 52 con3d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( -. x e. F -> -. ( f i^i X ) C_ x ) )
54 53 expr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ x C_ X ) -> ( f e. F -> ( -. x e. F -> -. ( f i^i X ) C_ x ) ) )
55 54 com23 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ x C_ X ) -> ( -. x e. F -> ( f e. F -> -. ( f i^i X ) C_ x ) ) )
56 55 impr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( f e. F -> -. ( f i^i X ) C_ x ) )
57 56 imp 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) /\ f e. F ) -> -. ( f i^i X ) C_ x )
58 ineq2 
 |-  ( g = ( X \ x ) -> ( f i^i g ) = ( f i^i ( X \ x ) ) )
59 58 neeq1d 
 |-  ( g = ( X \ x ) -> ( ( f i^i g ) =/= (/) <-> ( f i^i ( X \ x ) ) =/= (/) ) )
60 59 ralsng 
 |-  ( ( X \ x ) e. _V -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> ( f i^i ( X \ x ) ) =/= (/) ) )
61 inssdif0 
 |-  ( ( f i^i X ) C_ x <-> ( f i^i ( X \ x ) ) = (/) )
62 61 necon3bbii 
 |-  ( -. ( f i^i X ) C_ x <-> ( f i^i ( X \ x ) ) =/= (/) )
63 60 62 bitr4di 
 |-  ( ( X \ x ) e. _V -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> -. ( f i^i X ) C_ x ) )
64 31 63 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> -. ( f i^i X ) C_ x ) )
65 64 adantr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) /\ f e. F ) -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> -. ( f i^i X ) C_ x ) )
66 57 65 mpbird 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) /\ f e. F ) -> A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) )
67 66 ralrimiva 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> A. f e. F A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) )
68 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
69 68 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F e. ( fBas ` X ) )
70 difssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) C_ X )
71 ssdif0 
 |-  ( X C_ x <-> ( X \ x ) = (/) )
72 eqss 
 |-  ( x = X <-> ( x C_ X /\ X C_ x ) )
73 72 simplbi2 
 |-  ( x C_ X -> ( X C_ x -> x = X ) )
74 eleq1 
 |-  ( x = X -> ( x e. F <-> X e. F ) )
75 74 notbid 
 |-  ( x = X -> ( -. x e. F <-> -. X e. F ) )
76 75 biimpcd 
 |-  ( -. x e. F -> ( x = X -> -. X e. F ) )
77 73 76 sylan9 
 |-  ( ( x C_ X /\ -. x e. F ) -> ( X C_ x -> -. X e. F ) )
78 77 adantl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X C_ x -> -. X e. F ) )
79 71 78 syl5bir 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( X \ x ) = (/) -> -. X e. F ) )
80 79 necon2ad 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X e. F -> ( X \ x ) =/= (/) ) )
81 29 80 mpd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) =/= (/) )
82 snfbas 
 |-  ( ( ( X \ x ) C_ X /\ ( X \ x ) =/= (/) /\ X e. F ) -> { ( X \ x ) } e. ( fBas ` X ) )
83 70 81 29 82 syl3anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> { ( X \ x ) } e. ( fBas ` X ) )
84 fbunfip 
 |-  ( ( F e. ( fBas ` X ) /\ { ( X \ x ) } e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. { ( X \ x ) } ) ) <-> A. f e. F A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) ) )
85 69 83 84 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( -. (/) e. ( fi ` ( F u. { ( X \ x ) } ) ) <-> A. f e. F A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) ) )
86 67 85 mpbird 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> -. (/) e. ( fi ` ( F u. { ( X \ x ) } ) ) )
87 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 ) } ) ) ) ) )
88 29 87 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. 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 ) } ) ) ) ) )
89 36 41 86 88 mpbir3and 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) )
90 fgcl 
 |-  ( ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) e. ( Fil ` X ) )
91 89 90 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) e. ( Fil ` X ) )
92 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 )
93 91 92 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> E. f e. ( UFil ` X ) ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f )
94 r19.29 
 |-  ( ( A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) /\ E. f e. ( UFil ` X ) ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f ) -> E. f e. ( UFil ` X ) ( ( F C_ f <-> f = g ) /\ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f ) )
95 biimp 
 |-  ( ( F C_ f <-> f = g ) -> ( F C_ f -> f = g ) )
96 simpll 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F e. ( Fil ` X ) )
97 snex 
 |-  { ( X \ x ) } e. _V
98 unexg 
 |-  ( ( F e. ( Fil ` X ) /\ { ( X \ x ) } e. _V ) -> ( F u. { ( X \ x ) } ) e. _V )
99 96 97 98 sylancl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) e. _V )
100 ssfii 
 |-  ( ( F u. { ( X \ x ) } ) e. _V -> ( F u. { ( X \ x ) } ) C_ ( fi ` ( F u. { ( X \ x ) } ) ) )
101 99 100 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) C_ ( fi ` ( F u. { ( X \ x ) } ) ) )
102 ssfg 
 |-  ( ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) -> ( fi ` ( F u. { ( X \ x ) } ) ) C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
103 89 102 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( fi ` ( F u. { ( X \ x ) } ) ) C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
104 101 103 sstrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
105 104 unssad 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
106 sstr2 
 |-  ( F C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> F C_ f ) )
107 105 106 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> F C_ f ) )
108 107 imim1d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( F C_ f -> f = g ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> f = g ) ) )
109 sseq2 
 |-  ( f = g -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f <-> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
110 109 biimpcd 
 |-  ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> ( f = g -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
111 110 a2i 
 |-  ( ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> f = g ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
112 95 108 111 syl56 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( F C_ f <-> f = g ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) ) )
113 112 impd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( ( F C_ f <-> f = g ) /\ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
114 113 rexlimdvw 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( E. f e. ( UFil ` X ) ( ( F C_ f <-> f = g ) /\ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
115 94 114 syl5 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) /\ E. f e. ( UFil ` X ) ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
116 93 115 mpan2d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
117 116 imp 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g )
118 117 an32s 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g )
119 snidg 
 |-  ( ( X \ x ) e. _V -> ( X \ x ) e. { ( X \ x ) } )
120 31 119 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. { ( X \ x ) } )
121 elun2 
 |-  ( ( X \ x ) e. { ( X \ x ) } -> ( X \ x ) e. ( F u. { ( X \ x ) } ) )
122 120 121 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ( F u. { ( X \ x ) } ) )
123 104 122 sseldd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
124 123 adantlr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
125 118 124 sseldd 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. g )
126 simpllr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> g e. ( UFil ` X ) )
127 simprl 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> x C_ X )
128 ufilb 
 |-  ( ( g e. ( UFil ` X ) /\ x C_ X ) -> ( -. x e. g <-> ( X \ x ) e. g ) )
129 126 127 128 syl2anc 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( -. x e. g <-> ( X \ x ) e. g ) )
130 125 129 mpbird 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ ( x C_ X /\ -. x e. F ) ) -> -. x e. g )
131 130 expr 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ x C_ X ) -> ( -. x e. F -> -. x e. g ) )
132 131 con4d 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) /\ x C_ X ) -> ( x e. g -> x e. F ) )
133 132 ex 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> ( x C_ X -> ( x e. g -> x e. F ) ) )
134 133 com23 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> ( x e. g -> ( x C_ X -> x e. F ) ) )
135 24 134 mpdd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> ( x e. g -> x e. F ) )
136 135 ssrdv 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> g C_ F )
137 19 136 eqssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F = g )
138 simplr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> g e. ( UFil ` X ) )
139 137 138 eqeltrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F e. ( UFil ` X ) )
140 139 rexlimdva2 
 |-  ( F e. ( Fil ` X ) -> ( E. g e. ( UFil ` X ) A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) -> F e. ( UFil ` X ) ) )
141 13 140 syl5bi 
 |-  ( F e. ( Fil ` X ) -> ( E! f e. ( UFil ` X ) F C_ f -> F e. ( UFil ` X ) ) )
142 12 141 impbid2 
 |-  ( F e. ( Fil ` X ) -> ( F e. ( UFil ` X ) <-> E! f e. ( UFil ` X ) F C_ f ) )