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 ) )