Metamath Proof Explorer

Theorem limccnp2

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses limccnp2.r 
|- ( ( ph /\ x e. A ) -> R e. X )
limccnp2.s 
|- ( ( ph /\ x e. A ) -> S e. Y )
limccnp2.x 
|- ( ph -> X C_ CC )
limccnp2.y 
|- ( ph -> Y C_ CC )
limccnp2.k 
|- K = ( TopOpen ` CCfld )
limccnp2.j 
|- J = ( ( K tX K ) |`t ( X X. Y ) )
limccnp2.c 
|- ( ph -> C e. ( ( x e. A |-> R ) limCC B ) )
limccnp2.d 
|- ( ph -> D e. ( ( x e. A |-> S ) limCC B ) )
limccnp2.h 
|- ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )
Assertion limccnp2 
|- ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) limCC B ) )

Proof

Step Hyp Ref Expression
1 limccnp2.r 
 |-  ( ( ph /\ x e. A ) -> R e. X )
2 limccnp2.s 
 |-  ( ( ph /\ x e. A ) -> S e. Y )
3 limccnp2.x 
 |-  ( ph -> X C_ CC )
4 limccnp2.y 
 |-  ( ph -> Y C_ CC )
5 limccnp2.k 
 |-  K = ( TopOpen ` CCfld )
6 limccnp2.j 
 |-  J = ( ( K tX K ) |`t ( X X. Y ) )
7 limccnp2.c 
 |-  ( ph -> C e. ( ( x e. A |-> R ) limCC B ) )
8 limccnp2.d 
 |-  ( ph -> D e. ( ( x e. A |-> S ) limCC B ) )
9 limccnp2.h 
 |-  ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )
10 eqid 
 |-  U. J = U. J
11 10 cnprcl 
 |-  ( H e. ( ( J CnP K ) ` <. C , D >. ) -> <. C , D >. e. U. J )
12 9 11 syl 
 |-  ( ph -> <. C , D >. e. U. J )
13 5 cnfldtopon 
 |-  K e. ( TopOn ` CC )
14 txtopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ K e. ( TopOn ` CC ) ) -> ( K tX K ) e. ( TopOn ` ( CC X. CC ) ) )
15 13 13 14 mp2an 
 |-  ( K tX K ) e. ( TopOn ` ( CC X. CC ) )
16 xpss12 
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) )
17 3 4 16 syl2anc 
 |-  ( ph -> ( X X. Y ) C_ ( CC X. CC ) )
18 resttopon 
 |-  ( ( ( K tX K ) e. ( TopOn ` ( CC X. CC ) ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( ( K tX K ) |`t ( X X. Y ) ) e. ( TopOn ` ( X X. Y ) ) )
19 15 17 18 sylancr 
 |-  ( ph -> ( ( K tX K ) |`t ( X X. Y ) ) e. ( TopOn ` ( X X. Y ) ) )
20 6 19 eqeltrid 
 |-  ( ph -> J e. ( TopOn ` ( X X. Y ) ) )
21 toponuni 
 |-  ( J e. ( TopOn ` ( X X. Y ) ) -> ( X X. Y ) = U. J )
22 20 21 syl 
 |-  ( ph -> ( X X. Y ) = U. J )
23 12 22 eleqtrrd 
 |-  ( ph -> <. C , D >. e. ( X X. Y ) )
24 opelxp 
 |-  ( <. C , D >. e. ( X X. Y ) <-> ( C e. X /\ D e. Y ) )
25 23 24 sylib 
 |-  ( ph -> ( C e. X /\ D e. Y ) )
26 25 simpld 
 |-  ( ph -> C e. X )
27 26 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ x = B ) -> C e. X )
28 simpll 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> ph )
29 elun 
 |-  ( x e. ( A u. { B } ) <-> ( x e. A \/ x e. { B } ) )
30 29 bilani 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( x e. A \/ x e. { B } ) )
31 30 ord 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x e. A -> x e. { B } ) )
32 elsni 
 |-  ( x e. { B } -> x = B )
33 31 32 syl6 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x e. A -> x = B ) )
34 33 con1d 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x = B -> x e. A ) )
35 34 imp 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> x e. A )
36 28 35 1 syl2anc 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> R e. X )
37 27 36 ifclda 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , C , R ) e. X )
38 25 simprd 
 |-  ( ph -> D e. Y )
39 38 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ x = B ) -> D e. Y )
40 28 35 2 syl2anc 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> S e. Y )
41 39 40 ifclda 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , D , S ) e. Y )
42 37 41 opelxpd 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. e. ( X X. Y ) )
43 eqidd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) = ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) )
44 13 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
45 cnpf2 
 |-  ( ( J e. ( TopOn ` ( X X. Y ) ) /\ K e. ( TopOn ` CC ) /\ H e. ( ( J CnP K ) ` <. C , D >. ) ) -> H : ( X X. Y ) --> CC )
46 20 44 9 45 syl3anc 
 |-  ( ph -> H : ( X X. Y ) --> CC )
47 46 feqmptd 
 |-  ( ph -> H = ( y e. ( X X. Y ) |-> ( H ` y ) ) )
48 fveq2 
 |-  ( y = <. if ( x = B , C , R ) , if ( x = B , D , S ) >. -> ( H ` y ) = ( H ` <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) )
49 df-ov 
 |-  ( if ( x = B , C , R ) H if ( x = B , D , S ) ) = ( H ` <. if ( x = B , C , R ) , if ( x = B , D , S ) >. )
50 ovif12 
 |-  ( if ( x = B , C , R ) H if ( x = B , D , S ) ) = if ( x = B , ( C H D ) , ( R H S ) )
51 49 50 eqtr3i 
 |-  ( H ` <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) = if ( x = B , ( C H D ) , ( R H S ) )
52 48 51 eqtrdi 
 |-  ( y = <. if ( x = B , C , R ) , if ( x = B , D , S ) >. -> ( H ` y ) = if ( x = B , ( C H D ) , ( R H S ) ) )
53 42 43 47 52 fmptco 
 |-  ( ph -> ( H o. ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ) = ( x e. ( A u. { B } ) |-> if ( x = B , ( C H D ) , ( R H S ) ) ) )
54 eqid 
 |-  ( x e. A |-> R ) = ( x e. A |-> R )
55 54 1 dmmptd 
 |-  ( ph -> dom ( x e. A |-> R ) = A )
56 limcrcl 
 |-  ( C e. ( ( x e. A |-> R ) limCC B ) -> ( ( x e. A |-> R ) : dom ( x e. A |-> R ) --> CC /\ dom ( x e. A |-> R ) C_ CC /\ B e. CC ) )
57 7 56 syl 
 |-  ( ph -> ( ( x e. A |-> R ) : dom ( x e. A |-> R ) --> CC /\ dom ( x e. A |-> R ) C_ CC /\ B e. CC ) )
58 57 simp2d 
 |-  ( ph -> dom ( x e. A |-> R ) C_ CC )
59 55 58 eqsstrrd 
 |-  ( ph -> A C_ CC )
60 57 simp3d 
 |-  ( ph -> B e. CC )
61 60 snssd 
 |-  ( ph -> { B } C_ CC )
62 59 61 unssd 
 |-  ( ph -> ( A u. { B } ) C_ CC )
63 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
64 13 62 63 sylancr 
 |-  ( ph -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
65 ssun2 
 |-  { B } C_ ( A u. { B } )
66 snssg 
 |-  ( B e. CC -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
67 60 66 syl 
 |-  ( ph -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
68 65 67 mpbiri 
 |-  ( ph -> B e. ( A u. { B } ) )
69 3 adantr 
 |-  ( ( ph /\ x e. A ) -> X C_ CC )
70 69 1 sseldd 
 |-  ( ( ph /\ x e. A ) -> R e. CC )
71 eqid 
 |-  ( K |`t ( A u. { B } ) ) = ( K |`t ( A u. { B } ) )
72 59 60 70 71 5 limcmpt 
 |-  ( ph -> ( C e. ( ( x e. A |-> R ) limCC B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , C , R ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
73 7 72 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , R ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
74 4 adantr 
 |-  ( ( ph /\ x e. A ) -> Y C_ CC )
75 74 2 sseldd 
 |-  ( ( ph /\ x e. A ) -> S e. CC )
76 59 60 75 71 5 limcmpt 
 |-  ( ph -> ( D e. ( ( x e. A |-> S ) limCC B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , D , S ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
77 8 76 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , D , S ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
78 64 44 44 68 73 77 txcnp 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K tX K ) ) ` B ) )
79 15 topontopi 
 |-  ( K tX K ) e. Top
80 79 a1i 
 |-  ( ph -> ( K tX K ) e. Top )
81 42 fmpttd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : ( A u. { B } ) --> ( X X. Y ) )
82 toponuni 
 |-  ( ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
83 64 82 syl 
 |-  ( ph -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
84 83 feq2d 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : ( A u. { B } ) --> ( X X. Y ) <-> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : U. ( K |`t ( A u. { B } ) ) --> ( X X. Y ) ) )
85 81 84 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : U. ( K |`t ( A u. { B } ) ) --> ( X X. Y ) )
86 eqid 
 |-  U. ( K |`t ( A u. { B } ) ) = U. ( K |`t ( A u. { B } ) )
87 15 toponunii 
 |-  ( CC X. CC ) = U. ( K tX K )
88 86 87 cnprest2 
 |-  ( ( ( K tX K ) e. Top /\ ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : U. ( K |`t ( A u. { B } ) ) --> ( X X. Y ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K tX K ) ) ` B ) <-> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) ) ` B ) ) )
89 80 85 17 88 syl3anc 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K tX K ) ) ` B ) <-> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) ) ` B ) ) )
90 78 89 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) ) ` B ) )
91 6 oveq2i 
 |-  ( ( K |`t ( A u. { B } ) ) CnP J ) = ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) )
92 91 fveq1i 
 |-  ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) = ( ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) ) ` B )
93 90 92 eleqtrrdi 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) )
94 iftrue 
 |-  ( x = B -> if ( x = B , C , R ) = C )
95 iftrue 
 |-  ( x = B -> if ( x = B , D , S ) = D )
96 94 95 opeq12d 
 |-  ( x = B -> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. = <. C , D >. )
97 eqid 
 |-  ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) = ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. )
98 opex 
 |-  <. C , D >. e. _V
99 96 97 98 fvmpt 
 |-  ( B e. ( A u. { B } ) -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) = <. C , D >. )
100 68 99 syl 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) = <. C , D >. )
101 100 fveq2d 
 |-  ( ph -> ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) ) = ( ( J CnP K ) ` <. C , D >. ) )
102 9 101 eleqtrrd 
 |-  ( ph -> H e. ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) ) )
103 cnpco 
 |-  ( ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) e. ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) /\ H e. ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) ) ) -> ( H o. ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
104 93 102 103 syl2anc 
 |-  ( ph -> ( H o. ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
105 53 104 eqeltrrd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , ( C H D ) , ( R H S ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
106 46 adantr 
 |-  ( ( ph /\ x e. A ) -> H : ( X X. Y ) --> CC )
107 106 1 2 fovcdmd 
 |-  ( ( ph /\ x e. A ) -> ( R H S ) e. CC )
108 59 60 107 71 5 limcmpt 
 |-  ( ph -> ( ( C H D ) e. ( ( x e. A |-> ( R H S ) ) limCC B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , ( C H D ) , ( R H S ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
109 105 108 mpbird 
 |-  ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) limCC B ) )