Metamath Proof Explorer

Theorem fmufil

Description: An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fmufil 
|- ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( UFil ` X ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( L e. ( UFil ` Y ) -> L e. ( Fil ` Y ) )
2 filfbas 
 |-  ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) )
3 1 2 syl 
 |-  ( L e. ( UFil ` Y ) -> L e. ( fBas ` Y ) )
4 fmfil 
 |-  ( ( X e. A /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
5 3 4 syl3an2 
 |-  ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
6 simpl2 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> L e. ( UFil ` Y ) )
7 6 1 2 3syl 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> L e. ( fBas ` Y ) )
8 simprl 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> f e. ( Fil ` X ) )
9 simpl3 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> F : Y --> X )
10 simprr 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> ( ( X FilMap F ) ` L ) C_ f )
11 7 8 9 10 fmfnfm 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> E. g e. ( Fil ` Y ) ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) )
12 6 adantr 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> L e. ( UFil ` Y ) )
13 simprl 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> g e. ( Fil ` Y ) )
14 simprrl 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> L C_ g )
15 ufilmax 
 |-  ( ( L e. ( UFil ` Y ) /\ g e. ( Fil ` Y ) /\ L C_ g ) -> L = g )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> L = g )
17 16 fveq2d 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> ( ( X FilMap F ) ` L ) = ( ( X FilMap F ) ` g ) )
18 simprrr 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> f = ( ( X FilMap F ) ` g ) )
19 17 18 eqtr4d 
 |-  ( ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) /\ ( g e. ( Fil ` Y ) /\ ( L C_ g /\ f = ( ( X FilMap F ) ` g ) ) ) ) -> ( ( X FilMap F ) ` L ) = f )
20 11 19 rexlimddv 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ ( f e. ( Fil ` X ) /\ ( ( X FilMap F ) ` L ) C_ f ) ) -> ( ( X FilMap F ) ` L ) = f )
21 20 expr 
 |-  ( ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) /\ f e. ( Fil ` X ) ) -> ( ( ( X FilMap F ) ` L ) C_ f -> ( ( X FilMap F ) ` L ) = f ) )
22 21 ralrimiva 
 |-  ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> A. f e. ( Fil ` X ) ( ( ( X FilMap F ) ` L ) C_ f -> ( ( X FilMap F ) ` L ) = f ) )
23 isufil2 
 |-  ( ( ( X FilMap F ) ` L ) e. ( UFil ` X ) <-> ( ( ( X FilMap F ) ` L ) e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( ( ( X FilMap F ) ` L ) C_ f -> ( ( X FilMap F ) ` L ) = f ) ) )
24 5 22 23 sylanbrc 
 |-  ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( UFil ` X ) )