Metamath Proof Explorer

Theorem fmucnd

Description: The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of BourbakiTop1 p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Hypotheses fmucnd.1 
|- ( ph -> U e. ( UnifOn ` X ) )
fmucnd.2 
|- ( ph -> V e. ( UnifOn ` Y ) )
fmucnd.3 
|- ( ph -> F e. ( U uCn V ) )
fmucnd.4 
|- ( ph -> C e. ( CauFilU ` U ) )
fmucnd.5 
|- D = ran ( a e. C |-> ( F " a ) )
Assertion fmucnd 
|- ( ph -> D e. ( CauFilU ` V ) )

Proof

Step Hyp Ref Expression
1 fmucnd.1 
 |-  ( ph -> U e. ( UnifOn ` X ) )
2 fmucnd.2 
 |-  ( ph -> V e. ( UnifOn ` Y ) )
3 fmucnd.3 
 |-  ( ph -> F e. ( U uCn V ) )
4 fmucnd.4 
 |-  ( ph -> C e. ( CauFilU ` U ) )
5 fmucnd.5 
 |-  D = ran ( a e. C |-> ( F " a ) )
6 cfilufbas 
 |-  ( ( U e. ( UnifOn ` X ) /\ C e. ( CauFilU ` U ) ) -> C e. ( fBas ` X ) )
7 1 4 6 syl2anc 
 |-  ( ph -> C e. ( fBas ` X ) )
8 isucn 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. v e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) v ( F ` y ) ) ) ) )
9 8 simprbda 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) /\ F e. ( U uCn V ) ) -> F : X --> Y )
10 1 2 3 9 syl21anc 
 |-  ( ph -> F : X --> Y )
11 2 elfvexd 
 |-  ( ph -> Y e. _V )
12 5 fbasrn 
 |-  ( ( C e. ( fBas ` X ) /\ F : X --> Y /\ Y e. _V ) -> D e. ( fBas ` Y ) )
13 7 10 11 12 syl3anc 
 |-  ( ph -> D e. ( fBas ` Y ) )
14 simplr 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> a e. C )
15 eqid 
 |-  ( F " a ) = ( F " a )
16 imaeq2 
 |-  ( c = a -> ( F " c ) = ( F " a ) )
17 16 rspceeqv 
 |-  ( ( a e. C /\ ( F " a ) = ( F " a ) ) -> E. c e. C ( F " a ) = ( F " c ) )
18 14 15 17 sylancl 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> E. c e. C ( F " a ) = ( F " c ) )
19 imaexg 
 |-  ( F e. ( U uCn V ) -> ( F " a ) e. _V )
20 eqid 
 |-  ( c e. C |-> ( F " c ) ) = ( c e. C |-> ( F " c ) )
21 20 elrnmpt 
 |-  ( ( F " a ) e. _V -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) )
22 3 19 21 3syl 
 |-  ( ph -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) )
23 22 ad3antrrr 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) )
24 18 23 mpbird 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( F " a ) e. ran ( c e. C |-> ( F " c ) ) )
25 imaeq2 
 |-  ( a = c -> ( F " a ) = ( F " c ) )
26 25 cbvmptv 
 |-  ( a e. C |-> ( F " a ) ) = ( c e. C |-> ( F " c ) )
27 26 rneqi 
 |-  ran ( a e. C |-> ( F " a ) ) = ran ( c e. C |-> ( F " c ) )
28 5 27 eqtri 
 |-  D = ran ( c e. C |-> ( F " c ) )
29 24 28 eleqtrrdi 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( F " a ) e. D )
30 10 ffnd 
 |-  ( ph -> F Fn X )
31 30 ad3antrrr 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> F Fn X )
32 fbelss 
 |-  ( ( C e. ( fBas ` X ) /\ a e. C ) -> a C_ X )
33 7 32 sylan 
 |-  ( ( ph /\ a e. C ) -> a C_ X )
34 33 ad4ant13 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> a C_ X )
35 fmucndlem 
 |-  ( ( F Fn X /\ a C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) = ( ( F " a ) X. ( F " a ) ) )
36 31 34 35 syl2anc 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) = ( ( F " a ) X. ( F " a ) ) )
37 eqid 
 |-  ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
38 37 mpofun 
 |-  Fun ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
39 funimass2 
 |-  ( ( Fun ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v )
40 38 39 mpan 
 |-  ( ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v )
41 40 adantl 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v )
42 36 41 eqsstrrd 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( F " a ) X. ( F " a ) ) C_ v )
43 id 
 |-  ( b = ( F " a ) -> b = ( F " a ) )
44 43 sqxpeqd 
 |-  ( b = ( F " a ) -> ( b X. b ) = ( ( F " a ) X. ( F " a ) ) )
45 44 sseq1d 
 |-  ( b = ( F " a ) -> ( ( b X. b ) C_ v <-> ( ( F " a ) X. ( F " a ) ) C_ v ) )
46 45 rspcev 
 |-  ( ( ( F " a ) e. D /\ ( ( F " a ) X. ( F " a ) ) C_ v ) -> E. b e. D ( b X. b ) C_ v )
47 29 42 46 syl2anc 
 |-  ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> E. b e. D ( b X. b ) C_ v )
48 1 adantr 
 |-  ( ( ph /\ v e. V ) -> U e. ( UnifOn ` X ) )
49 4 adantr 
 |-  ( ( ph /\ v e. V ) -> C e. ( CauFilU ` U ) )
50 2 adantr 
 |-  ( ( ph /\ v e. V ) -> V e. ( UnifOn ` Y ) )
51 3 adantr 
 |-  ( ( ph /\ v e. V ) -> F e. ( U uCn V ) )
52 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
53 nfcv 
 |-  F/_ s <. ( F ` x ) , ( F ` y ) >.
54 nfcv 
 |-  F/_ t <. ( F ` x ) , ( F ` y ) >.
55 nfcv 
 |-  F/_ x <. ( F ` s ) , ( F ` t ) >.
56 nfcv 
 |-  F/_ y <. ( F ` s ) , ( F ` t ) >.
57 simpl 
 |-  ( ( x = s /\ y = t ) -> x = s )
58 57 fveq2d 
 |-  ( ( x = s /\ y = t ) -> ( F ` x ) = ( F ` s ) )
59 simpr 
 |-  ( ( x = s /\ y = t ) -> y = t )
60 59 fveq2d 
 |-  ( ( x = s /\ y = t ) -> ( F ` y ) = ( F ` t ) )
61 58 60 opeq12d 
 |-  ( ( x = s /\ y = t ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` s ) , ( F ` t ) >. )
62 53 54 55 56 61 cbvmpo 
 |-  ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) = ( s e. X , t e. X |-> <. ( F ` s ) , ( F ` t ) >. )
63 48 50 51 52 62 ucnprima 
 |-  ( ( ph /\ v e. V ) -> ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) e. U )
64 cfiluexsm 
 |-  ( ( U e. ( UnifOn ` X ) /\ C e. ( CauFilU ` U ) /\ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) e. U ) -> E. a e. C ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) )
65 48 49 63 64 syl3anc 
 |-  ( ( ph /\ v e. V ) -> E. a e. C ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) )
66 47 65 r19.29a 
 |-  ( ( ph /\ v e. V ) -> E. b e. D ( b X. b ) C_ v )
67 66 ralrimiva 
 |-  ( ph -> A. v e. V E. b e. D ( b X. b ) C_ v )
68 iscfilu 
 |-  ( V e. ( UnifOn ` Y ) -> ( D e. ( CauFilU ` V ) <-> ( D e. ( fBas ` Y ) /\ A. v e. V E. b e. D ( b X. b ) C_ v ) ) )
69 2 68 syl 
 |-  ( ph -> ( D e. ( CauFilU ` V ) <-> ( D e. ( fBas ` Y ) /\ A. v e. V E. b e. D ( b X. b ) C_ v ) ) )
70 13 67 69 mpbir2and 
 |-  ( ph -> D e. ( CauFilU ` V ) )