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 A L UFil Y F : Y X X FilMap F L UFil X

Proof

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