Metamath Proof Explorer

Theorem fmf

Description: Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fmf 
|- ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( X filGen ran ( y e. b |-> ( F " y ) ) ) e. _V
2 eqid 
 |-  ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) = ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) )
3 1 2 fnmpti 
 |-  ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) Fn ( fBas ` Y )
4 df-fm 
 |-  FilMap = ( x e. _V , f e. _V |-> ( b e. ( fBas ` dom f ) |-> ( x filGen ran ( y e. b |-> ( f " y ) ) ) ) )
5 4 a1i 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> FilMap = ( x e. _V , f e. _V |-> ( b e. ( fBas ` dom f ) |-> ( x filGen ran ( y e. b |-> ( f " y ) ) ) ) ) )
6 dmeq 
 |-  ( f = F -> dom f = dom F )
7 6 adantl 
 |-  ( ( x = X /\ f = F ) -> dom f = dom F )
8 fdm 
 |-  ( F : Y --> X -> dom F = Y )
9 8 3ad2ant3 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> dom F = Y )
10 7 9 sylan9eqr 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ ( x = X /\ f = F ) ) -> dom f = Y )
11 10 fveq2d 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ ( x = X /\ f = F ) ) -> ( fBas ` dom f ) = ( fBas ` Y ) )
12 id 
 |-  ( x = X -> x = X )
13 imaeq1 
 |-  ( f = F -> ( f " y ) = ( F " y ) )
14 13 mpteq2dv 
 |-  ( f = F -> ( y e. b |-> ( f " y ) ) = ( y e. b |-> ( F " y ) ) )
15 14 rneqd 
 |-  ( f = F -> ran ( y e. b |-> ( f " y ) ) = ran ( y e. b |-> ( F " y ) ) )
16 12 15 oveqan12d 
 |-  ( ( x = X /\ f = F ) -> ( x filGen ran ( y e. b |-> ( f " y ) ) ) = ( X filGen ran ( y e. b |-> ( F " y ) ) ) )
17 16 adantl 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ ( x = X /\ f = F ) ) -> ( x filGen ran ( y e. b |-> ( f " y ) ) ) = ( X filGen ran ( y e. b |-> ( F " y ) ) ) )
18 11 17 mpteq12dv 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ ( x = X /\ f = F ) ) -> ( b e. ( fBas ` dom f ) |-> ( x filGen ran ( y e. b |-> ( f " y ) ) ) ) = ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) )
19 elex 
 |-  ( X e. A -> X e. _V )
20 19 3ad2ant1 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> X e. _V )
21 fex2 
 |-  ( ( F : Y --> X /\ Y e. B /\ X e. A ) -> F e. _V )
22 21 3com13 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> F e. _V )
23 fvex 
 |-  ( fBas ` Y ) e. _V
24 23 mptex 
 |-  ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) e. _V
25 24 a1i 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) e. _V )
26 5 18 20 22 25 ovmpod 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( X FilMap F ) = ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) )
27 26 fneq1d 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( ( X FilMap F ) Fn ( fBas ` Y ) <-> ( b e. ( fBas ` Y ) |-> ( X filGen ran ( y e. b |-> ( F " y ) ) ) ) Fn ( fBas ` Y ) ) )
28 3 27 mpbiri 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( X FilMap F ) Fn ( fBas ` Y ) )
29 simpl1 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> X e. A )
30 simpr 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> b e. ( fBas ` Y ) )
31 simpl3 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> F : Y --> X )
32 fmfil 
 |-  ( ( X e. A /\ b e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` b ) e. ( Fil ` X ) )
33 29 30 31 32 syl3anc 
 |-  ( ( ( X e. A /\ Y e. B /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> ( ( X FilMap F ) ` b ) e. ( Fil ` X ) )
34 33 ralrimiva 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> A. b e. ( fBas ` Y ) ( ( X FilMap F ) ` b ) e. ( Fil ` X ) )
35 ffnfv 
 |-  ( ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) <-> ( ( X FilMap F ) Fn ( fBas ` Y ) /\ A. b e. ( fBas ` Y ) ( ( X FilMap F ) ` b ) e. ( Fil ` X ) ) )
36 28 34 35 sylanbrc 
 |-  ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) )