Metamath Proof Explorer

Theorem fmcncfil

Description: The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017)

Ref Expression
Hypotheses fmcncfil.1 
|- J = ( MetOpen ` D )
fmcncfil.2 
|- K = ( MetOpen ` E )
Assertion fmcncfil 
|- ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( ( Y FilMap F ) ` B ) e. ( CauFil ` E ) )

Proof

Step Hyp Ref Expression
1 fmcncfil.1 
 |-  J = ( MetOpen ` D )
2 fmcncfil.2 
 |-  K = ( MetOpen ` E )
3 simpl2 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> E e. ( *Met ` Y ) )
4 simpl1 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> D e. ( CMet ` X ) )
5 1 cmetcvg 
 |-  ( ( D e. ( CMet ` X ) /\ B e. ( CauFil ` D ) ) -> ( J fLim B ) =/= (/) )
6 n0 
 |-  ( ( J fLim B ) =/= (/) <-> E. x x e. ( J fLim B ) )
7 5 6 sylib 
 |-  ( ( D e. ( CMet ` X ) /\ B e. ( CauFil ` D ) ) -> E. x x e. ( J fLim B ) )
8 4 7 sylancom 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> E. x x e. ( J fLim B ) )
9 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
10 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
11 4 9 10 3syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> D e. ( *Met ` X ) )
12 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( CauFil ` D ) ) -> B e. ( Fil ` X ) )
13 11 12 sylancom 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> B e. ( Fil ` X ) )
14 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
15 11 14 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> J e. ( TopOn ` X ) )
16 2 mopntopon 
 |-  ( E e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
17 3 16 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> K e. ( TopOn ` Y ) )
18 simpl3 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> F e. ( J Cn K ) )
19 cnflf 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. b e. ( Fil ` X ) A. x e. ( J fLim b ) ( F ` x ) e. ( ( K fLimf b ) ` F ) ) ) )
20 19 simplbda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> A. b e. ( Fil ` X ) A. x e. ( J fLim b ) ( F ` x ) e. ( ( K fLimf b ) ` F ) )
21 15 17 18 20 syl21anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> A. b e. ( Fil ` X ) A. x e. ( J fLim b ) ( F ` x ) e. ( ( K fLimf b ) ` F ) )
22 oveq2 
 |-  ( b = B -> ( J fLim b ) = ( J fLim B ) )
23 oveq2 
 |-  ( b = B -> ( K fLimf b ) = ( K fLimf B ) )
24 23 fveq1d 
 |-  ( b = B -> ( ( K fLimf b ) ` F ) = ( ( K fLimf B ) ` F ) )
25 24 eleq2d 
 |-  ( b = B -> ( ( F ` x ) e. ( ( K fLimf b ) ` F ) <-> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) )
26 22 25 raleqbidv 
 |-  ( b = B -> ( A. x e. ( J fLim b ) ( F ` x ) e. ( ( K fLimf b ) ` F ) <-> A. x e. ( J fLim B ) ( F ` x ) e. ( ( K fLimf B ) ` F ) ) )
27 26 rspcv 
 |-  ( B e. ( Fil ` X ) -> ( A. b e. ( Fil ` X ) A. x e. ( J fLim b ) ( F ` x ) e. ( ( K fLimf b ) ` F ) -> A. x e. ( J fLim B ) ( F ` x ) e. ( ( K fLimf B ) ` F ) ) )
28 13 21 27 sylc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> A. x e. ( J fLim B ) ( F ` x ) e. ( ( K fLimf B ) ` F ) )
29 df-ral 
 |-  ( A. x e. ( J fLim B ) ( F ` x ) e. ( ( K fLimf B ) ` F ) <-> A. x ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) )
30 28 29 sylib 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> A. x ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) )
31 19.29r 
 |-  ( ( E. x x e. ( J fLim B ) /\ A. x ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) ) -> E. x ( x e. ( J fLim B ) /\ ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) ) )
32 pm3.35 
 |-  ( ( x e. ( J fLim B ) /\ ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) )
33 32 eximi 
 |-  ( E. x ( x e. ( J fLim B ) /\ ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) ) -> E. x ( F ` x ) e. ( ( K fLimf B ) ` F ) )
34 31 33 syl 
 |-  ( ( E. x x e. ( J fLim B ) /\ A. x ( x e. ( J fLim B ) -> ( F ` x ) e. ( ( K fLimf B ) ` F ) ) ) -> E. x ( F ` x ) e. ( ( K fLimf B ) ` F ) )
35 8 30 34 syl2anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> E. x ( F ` x ) e. ( ( K fLimf B ) ` F ) )
36 1 2 metcn 
 |-  ( ( D e. ( *Met ` X ) /\ E e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. e e. RR+ E. d e. RR+ A. y e. X ( ( x D y ) < d -> ( ( F ` x ) E ( F ` y ) ) < e ) ) ) )
37 36 biimpa 
 |-  ( ( ( D e. ( *Met ` X ) /\ E e. ( *Met ` Y ) ) /\ F e. ( J Cn K ) ) -> ( F : X --> Y /\ A. x e. X A. e e. RR+ E. d e. RR+ A. y e. X ( ( x D y ) < d -> ( ( F ` x ) E ( F ` y ) ) < e ) ) )
38 11 3 18 37 syl21anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( F : X --> Y /\ A. x e. X A. e e. RR+ E. d e. RR+ A. y e. X ( ( x D y ) < d -> ( ( F ` x ) E ( F ` y ) ) < e ) ) )
39 38 simpld 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> F : X --> Y )
40 flfval 
 |-  ( ( K e. ( TopOn ` Y ) /\ B e. ( Fil ` X ) /\ F : X --> Y ) -> ( ( K fLimf B ) ` F ) = ( K fLim ( ( Y FilMap F ) ` B ) ) )
41 17 13 39 40 syl3anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( ( K fLimf B ) ` F ) = ( K fLim ( ( Y FilMap F ) ` B ) ) )
42 41 eleq2d 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( ( F ` x ) e. ( ( K fLimf B ) ` F ) <-> ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) ) )
43 42 exbidv 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( E. x ( F ` x ) e. ( ( K fLimf B ) ` F ) <-> E. x ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) ) )
44 35 43 mpbid 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> E. x ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) )
45 2 flimcfil 
 |-  ( ( E e. ( *Met ` Y ) /\ ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) ) -> ( ( Y FilMap F ) ` B ) e. ( CauFil ` E ) )
46 45 ex 
 |-  ( E e. ( *Met ` Y ) -> ( ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) -> ( ( Y FilMap F ) ` B ) e. ( CauFil ` E ) ) )
47 46 exlimdv 
 |-  ( E e. ( *Met ` Y ) -> ( E. x ( F ` x ) e. ( K fLim ( ( Y FilMap F ) ` B ) ) -> ( ( Y FilMap F ) ` B ) e. ( CauFil ` E ) ) )
48 3 44 47 sylc 
 |-  ( ( ( D e. ( CMet ` X ) /\ E e. ( *Met ` Y ) /\ F e. ( J Cn K ) ) /\ B e. ( CauFil ` D ) ) -> ( ( Y FilMap F ) ` B ) e. ( CauFil ` E ) )