Metamath Proof Explorer

Theorem fmcfil

Description: The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion fmcfil 
|- ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( ( X FilMap F ) ` B ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
2 fmval 
 |-  ( ( X e. dom *Met /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( X filGen ran ( y e. B |-> ( F " y ) ) ) )
3 1 2 syl3an1 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( X filGen ran ( y e. B |-> ( F " y ) ) ) )
4 3 eleq1d 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( ( X FilMap F ) ` B ) e. ( CauFil ` D ) <-> ( X filGen ran ( y e. B |-> ( F " y ) ) ) e. ( CauFil ` D ) ) )
5 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> D e. ( *Met ` X ) )
6 simp2 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> B e. ( fBas ` Y ) )
7 simp3 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> F : Y --> X )
8 1 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> X e. dom *Met )
9 eqid 
 |-  ran ( y e. B |-> ( F " y ) ) = ran ( y e. B |-> ( F " y ) )
10 9 fbasrn 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y --> X /\ X e. dom *Met ) -> ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) )
11 6 7 8 10 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) )
12 fgcfil 
 |-  ( ( D e. ( *Met ` X ) /\ ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) ) -> ( ( X filGen ran ( y e. B |-> ( F " y ) ) ) e. ( CauFil ` D ) <-> A. x e. RR+ E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x ) )
13 5 11 12 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X filGen ran ( y e. B |-> ( F " y ) ) ) e. ( CauFil ` D ) <-> A. x e. RR+ E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x ) )
14 imassrn 
 |-  ( F " y ) C_ ran F
15 frn 
 |-  ( F : Y --> X -> ran F C_ X )
16 15 3ad2ant3 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ran F C_ X )
17 14 16 sstrid 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( F " y ) C_ X )
18 8 17 ssexd 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( F " y ) e. _V )
19 18 ralrimivw 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> A. y e. B ( F " y ) e. _V )
20 eqid 
 |-  ( y e. B |-> ( F " y ) ) = ( y e. B |-> ( F " y ) )
21 raleq 
 |-  ( s = ( F " y ) -> ( A. v e. s ( u D v ) < x <-> A. v e. ( F " y ) ( u D v ) < x ) )
22 21 raleqbi1dv 
 |-  ( s = ( F " y ) -> ( A. u e. s A. v e. s ( u D v ) < x <-> A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x ) )
23 20 22 rexrnmptw 
 |-  ( A. y e. B ( F " y ) e. _V -> ( E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x <-> E. y e. B A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x ) )
24 19 23 syl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x <-> E. y e. B A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x ) )
25 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> F : Y --> X )
26 25 ffnd 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> F Fn Y )
27 fbelss 
 |-  ( ( B e. ( fBas ` Y ) /\ y e. B ) -> y C_ Y )
28 6 27 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> y C_ Y )
29 oveq1 
 |-  ( u = ( F ` z ) -> ( u D v ) = ( ( F ` z ) D v ) )
30 29 breq1d 
 |-  ( u = ( F ` z ) -> ( ( u D v ) < x <-> ( ( F ` z ) D v ) < x ) )
31 30 ralbidv 
 |-  ( u = ( F ` z ) -> ( A. v e. ( F " y ) ( u D v ) < x <-> A. v e. ( F " y ) ( ( F ` z ) D v ) < x ) )
32 31 ralima 
 |-  ( ( F Fn Y /\ y C_ Y ) -> ( A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x <-> A. z e. y A. v e. ( F " y ) ( ( F ` z ) D v ) < x ) )
33 26 28 32 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> ( A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x <-> A. z e. y A. v e. ( F " y ) ( ( F ` z ) D v ) < x ) )
34 oveq2 
 |-  ( v = ( F ` w ) -> ( ( F ` z ) D v ) = ( ( F ` z ) D ( F ` w ) ) )
35 34 breq1d 
 |-  ( v = ( F ` w ) -> ( ( ( F ` z ) D v ) < x <-> ( ( F ` z ) D ( F ` w ) ) < x ) )
36 35 ralima 
 |-  ( ( F Fn Y /\ y C_ Y ) -> ( A. v e. ( F " y ) ( ( F ` z ) D v ) < x <-> A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
37 26 28 36 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> ( A. v e. ( F " y ) ( ( F ` z ) D v ) < x <-> A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
38 37 ralbidv 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> ( A. z e. y A. v e. ( F " y ) ( ( F ` z ) D v ) < x <-> A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
39 33 38 bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ y e. B ) -> ( A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x <-> A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
40 39 rexbidva 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. y e. B A. u e. ( F " y ) A. v e. ( F " y ) ( u D v ) < x <-> E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
41 24 40 bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x <-> E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
42 41 ralbidv 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A. x e. RR+ E. s e. ran ( y e. B |-> ( F " y ) ) A. u e. s A. v e. s ( u D v ) < x <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
43 4 13 42 3bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( ( X FilMap F ) ` B ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )