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 29 difexd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. _V )
31 elpwg 
 |-  ( ( X \ x ) e. _V -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
32 30 31 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
33 27 32 mpbiri 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ~P X )
34 33 snssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> { ( X \ x ) } C_ ~P X )
35 26 34 unssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) C_ ~P X )
36 ssun1 
 |-  F C_ ( F u. { ( X \ x ) } )
37 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
38 37 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F =/= (/) )
39 ssn0 
 |-  ( ( F C_ ( F u. { ( X \ x ) } ) /\ F =/= (/) ) -> ( F u. { ( X \ x ) } ) =/= (/) )
40 36 38 39 sylancr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) =/= (/) )
41 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ f e. F ) -> f C_ X )
42 41 ad2ant2rl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> f C_ X )
43 df-ss 
 |-  ( f C_ X <-> ( f i^i X ) = f )
44 42 43 sylib 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( f i^i X ) = f )
45 44 sseq1d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( ( f i^i X ) C_ x <-> f C_ x ) )
46 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( f e. F /\ x C_ X /\ f C_ x ) ) -> x e. F )
47 46 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( f e. F -> ( x C_ X -> ( f C_ x -> x e. F ) ) ) )
48 47 impcomd 
 |-  ( F e. ( Fil ` X ) -> ( ( x C_ X /\ f e. F ) -> ( f C_ x -> x e. F ) ) )
49 48 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) -> ( ( x C_ X /\ f e. F ) -> ( f C_ x -> x e. F ) ) )
50 49 imp 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( f C_ x -> x e. F ) )
51 45 50 sylbid 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( ( f i^i X ) C_ x -> x e. F ) )
52 51 con3d 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ f e. F ) ) -> ( -. x e. F -> -. ( f i^i X ) C_ x ) )
53 52 expr 
 |-  ( ( ( 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 com23 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ x C_ X ) -> ( -. x e. F -> ( f e. F -> -. ( f i^i X ) C_ x ) ) )
55 54 impr 
 |-  ( ( ( 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 imp 
 |-  ( ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) /\ f e. F ) -> -. ( f i^i X ) C_ x )
57 ineq2 
 |-  ( g = ( X \ x ) -> ( f i^i g ) = ( f i^i ( X \ x ) ) )
58 57 neeq1d 
 |-  ( g = ( X \ x ) -> ( ( f i^i g ) =/= (/) <-> ( f i^i ( X \ x ) ) =/= (/) ) )
59 58 ralsng 
 |-  ( ( X \ x ) e. _V -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> ( f i^i ( X \ x ) ) =/= (/) ) )
60 inssdif0 
 |-  ( ( f i^i X ) C_ x <-> ( f i^i ( X \ x ) ) = (/) )
61 60 necon3bbii 
 |-  ( -. ( f i^i X ) C_ x <-> ( f i^i ( X \ x ) ) =/= (/) )
62 59 61 bitr4di 
 |-  ( ( X \ x ) e. _V -> ( A. g e. { ( X \ x ) } ( f i^i g ) =/= (/) <-> -. ( f i^i X ) C_ x ) )
63 30 62 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 ) )
64 63 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 ) )
65 56 64 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 ) =/= (/) )
66 65 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 ) =/= (/) )
67 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
68 67 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F e. ( fBas ` X ) )
69 difssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) C_ X )
70 ssdif0 
 |-  ( X C_ x <-> ( X \ x ) = (/) )
71 eqss 
 |-  ( x = X <-> ( x C_ X /\ X C_ x ) )
72 71 simplbi2 
 |-  ( x C_ X -> ( X C_ x -> x = X ) )
73 eleq1 
 |-  ( x = X -> ( x e. F <-> X e. F ) )
74 73 notbid 
 |-  ( x = X -> ( -. x e. F <-> -. X e. F ) )
75 74 biimpcd 
 |-  ( -. x e. F -> ( x = X -> -. X e. F ) )
76 72 75 sylan9 
 |-  ( ( x C_ X /\ -. x e. F ) -> ( X C_ x -> -. X e. F ) )
77 76 adantl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X C_ x -> -. X e. F ) )
78 70 77 syl5bir 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( ( X \ x ) = (/) -> -. X e. F ) )
79 78 necon2ad 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X e. F -> ( X \ x ) =/= (/) ) )
80 29 79 mpd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) =/= (/) )
81 snfbas 
 |-  ( ( ( X \ x ) C_ X /\ ( X \ x ) =/= (/) /\ X e. F ) -> { ( X \ x ) } e. ( fBas ` X ) )
82 69 80 29 81 syl3anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> { ( X \ x ) } e. ( fBas ` X ) )
83 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 ) =/= (/) ) )
84 68 82 83 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 ) =/= (/) ) )
85 66 84 mpbird 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> -. (/) e. ( fi ` ( F u. { ( X \ x ) } ) ) )
86 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 ) } ) ) ) ) )
87 29 86 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 ) } ) ) ) ) )
88 35 40 85 87 mpbir3and 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) )
89 fgcl 
 |-  ( ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) e. ( Fil ` X ) )
90 88 89 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 ) )
91 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 )
92 90 91 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 )
93 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 ) )
94 biimp 
 |-  ( ( F C_ f <-> f = g ) -> ( F C_ f -> f = g ) )
95 simpll 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F e. ( Fil ` X ) )
96 snex 
 |-  { ( X \ x ) } e. _V
97 unexg 
 |-  ( ( F e. ( Fil ` X ) /\ { ( X \ x ) } e. _V ) -> ( F u. { ( X \ x ) } ) e. _V )
98 95 96 97 sylancl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( F u. { ( X \ x ) } ) e. _V )
99 ssfii 
 |-  ( ( F u. { ( X \ x ) } ) e. _V -> ( F u. { ( X \ x ) } ) C_ ( fi ` ( F u. { ( X \ x ) } ) ) )
100 98 99 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 ) } ) ) )
101 ssfg 
 |-  ( ( fi ` ( F u. { ( X \ x ) } ) ) e. ( fBas ` X ) -> ( fi ` ( F u. { ( X \ x ) } ) ) C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
102 88 101 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 ) } ) ) ) )
103 100 102 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 ) } ) ) ) )
104 103 unssad 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> F C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) )
105 sstr2 
 |-  ( F C_ ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> F C_ f ) )
106 104 105 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 ) )
107 106 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 ) ) )
108 sseq2 
 |-  ( f = g -> ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f <-> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
109 108 biimpcd 
 |-  ( ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ f -> ( f = g -> ( X filGen ( fi ` ( F u. { ( X \ x ) } ) ) ) C_ g ) )
110 109 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 ) )
111 94 107 110 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 ) ) )
112 111 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 ) )
113 112 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 ) )
114 93 113 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 ) )
115 92 114 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 ) )
116 115 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 )
117 116 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 )
118 snidg 
 |-  ( ( X \ x ) e. _V -> ( X \ x ) e. { ( X \ x ) } )
119 30 118 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. { ( X \ x ) } )
120 elun2 
 |-  ( ( X \ x ) e. { ( X \ x ) } -> ( X \ x ) e. ( F u. { ( X \ x ) } ) )
121 119 120 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ ( x C_ X /\ -. x e. F ) ) -> ( X \ x ) e. ( F u. { ( X \ x ) } ) )
122 103 121 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 ) } ) ) ) )
123 122 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 ) } ) ) ) )
124 117 123 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 )
125 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 ) )
126 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 )
127 ufilb 
 |-  ( ( g e. ( UFil ` X ) /\ x C_ X ) -> ( -. x e. g <-> ( X \ x ) e. g ) )
128 125 126 127 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 ) )
129 124 128 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 )
130 129 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 ) )
131 130 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 ) )
132 131 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 ) ) )
133 132 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 ) ) )
134 24 133 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 ) )
135 134 ssrdv 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> g C_ F )
136 19 135 eqssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F = g )
137 simplr 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> g e. ( UFil ` X ) )
138 136 137 eqeltrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ g e. ( UFil ` X ) ) /\ A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) ) -> F e. ( UFil ` X ) )
139 138 rexlimdva2 
 |-  ( F e. ( Fil ` X ) -> ( E. g e. ( UFil ` X ) A. f e. ( UFil ` X ) ( F C_ f <-> f = g ) -> F e. ( UFil ` X ) ) )
140 13 139 syl5bi 
 |-  ( F e. ( Fil ` X ) -> ( E! f e. ( UFil ` X ) F C_ f -> F e. ( UFil ` X ) ) )
141 12 140 impbid2 
 |-  ( F e. ( Fil ` X ) -> ( F e. ( UFil ` X ) <-> E! f e. ( UFil ` X ) F C_ f ) )