Metamath Proof Explorer

Theorem ssufl

Description: If Y is a subset of X and filters extend to ultrafilters in X , then they still do in Y . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ssufl 
|- ( ( X e. UFL /\ Y C_ X ) -> Y e. UFL )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> X e. UFL )
2 filfbas 
 |-  ( f e. ( Fil ` Y ) -> f e. ( fBas ` Y ) )
3 2 adantl 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> f e. ( fBas ` Y ) )
4 filsspw 
 |-  ( f e. ( Fil ` Y ) -> f C_ ~P Y )
5 4 adantl 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> f C_ ~P Y )
6 simplr 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> Y C_ X )
7 6 sspwd 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> ~P Y C_ ~P X )
8 5 7 sstrd 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> f C_ ~P X )
9 fbasweak 
 |-  ( ( f e. ( fBas ` Y ) /\ f C_ ~P X /\ X e. UFL ) -> f e. ( fBas ` X ) )
10 3 8 1 9 syl3anc 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> f e. ( fBas ` X ) )
11 fgcl 
 |-  ( f e. ( fBas ` X ) -> ( X filGen f ) e. ( Fil ` X ) )
12 10 11 syl 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> ( X filGen f ) e. ( Fil ` X ) )
13 ufli 
 |-  ( ( X e. UFL /\ ( X filGen f ) e. ( Fil ` X ) ) -> E. u e. ( UFil ` X ) ( X filGen f ) C_ u )
14 1 12 13 syl2anc 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> E. u e. ( UFil ` X ) ( X filGen f ) C_ u )
15 ssfg 
 |-  ( f e. ( fBas ` X ) -> f C_ ( X filGen f ) )
16 10 15 syl 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> f C_ ( X filGen f ) )
17 16 adantr 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> f C_ ( X filGen f ) )
18 simprr 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> ( X filGen f ) C_ u )
19 17 18 sstrd 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> f C_ u )
20 filtop 
 |-  ( f e. ( Fil ` Y ) -> Y e. f )
21 20 ad2antlr 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> Y e. f )
22 19 21 sseldd 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> Y e. u )
23 simprl 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> u e. ( UFil ` X ) )
24 6 adantr 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> Y C_ X )
25 trufil 
 |-  ( ( u e. ( UFil ` X ) /\ Y C_ X ) -> ( ( u |`t Y ) e. ( UFil ` Y ) <-> Y e. u ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> ( ( u |`t Y ) e. ( UFil ` Y ) <-> Y e. u ) )
27 22 26 mpbird 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> ( u |`t Y ) e. ( UFil ` Y ) )
28 5 adantr 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> f C_ ~P Y )
29 restid2 
 |-  ( ( Y e. f /\ f C_ ~P Y ) -> ( f |`t Y ) = f )
30 21 28 29 syl2anc 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> ( f |`t Y ) = f )
31 ssrest 
 |-  ( ( u e. ( UFil ` X ) /\ f C_ u ) -> ( f |`t Y ) C_ ( u |`t Y ) )
32 23 19 31 syl2anc 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> ( f |`t Y ) C_ ( u |`t Y ) )
33 30 32 eqsstrrd 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> f C_ ( u |`t Y ) )
34 sseq2 
 |-  ( g = ( u |`t Y ) -> ( f C_ g <-> f C_ ( u |`t Y ) ) )
35 34 rspcev 
 |-  ( ( ( u |`t Y ) e. ( UFil ` Y ) /\ f C_ ( u |`t Y ) ) -> E. g e. ( UFil ` Y ) f C_ g )
36 27 33 35 syl2anc 
 |-  ( ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) /\ ( u e. ( UFil ` X ) /\ ( X filGen f ) C_ u ) ) -> E. g e. ( UFil ` Y ) f C_ g )
37 14 36 rexlimddv 
 |-  ( ( ( X e. UFL /\ Y C_ X ) /\ f e. ( Fil ` Y ) ) -> E. g e. ( UFil ` Y ) f C_ g )
38 37 ralrimiva 
 |-  ( ( X e. UFL /\ Y C_ X ) -> A. f e. ( Fil ` Y ) E. g e. ( UFil ` Y ) f C_ g )
39 ssexg 
 |-  ( ( Y C_ X /\ X e. UFL ) -> Y e. _V )
40 39 ancoms 
 |-  ( ( X e. UFL /\ Y C_ X ) -> Y e. _V )
41 isufl 
 |-  ( Y e. _V -> ( Y e. UFL <-> A. f e. ( Fil ` Y ) E. g e. ( UFil ` Y ) f C_ g ) )
42 40 41 syl 
 |-  ( ( X e. UFL /\ Y C_ X ) -> ( Y e. UFL <-> A. f e. ( Fil ` Y ) E. g e. ( UFil ` Y ) f C_ g ) )
43 38 42 mpbird 
 |-  ( ( X e. UFL /\ Y C_ X ) -> Y e. UFL )