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 simpr 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> x e. ( A u. { B } ) )
30 elun 
 |-  ( x e. ( A u. { B } ) <-> ( x e. A \/ x e. { B } ) )
31 29 30 sylib 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( x e. A \/ x e. { B } ) )
32 31 ord 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x e. A -> x e. { B } ) )
33 elsni 
 |-  ( x e. { B } -> x = B )
34 32 33 syl6 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x e. A -> x = B ) )
35 34 con1d 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( -. x = B -> x e. A ) )
36 35 imp 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> x e. A )
37 28 36 1 syl2anc 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> R e. X )
38 27 37 ifclda 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , C , R ) e. X )
39 25 simprd 
 |-  ( ph -> D e. Y )
40 39 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ x = B ) -> D e. Y )
41 28 36 2 syl2anc 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> S e. Y )
42 40 41 ifclda 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , D , S ) e. Y )
43 38 42 opelxpd 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. e. ( X X. Y ) )
44 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 ) >. ) )
45 13 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
46 cnpf2 
 |-  ( ( J e. ( TopOn ` ( X X. Y ) ) /\ K e. ( TopOn ` CC ) /\ H e. ( ( J CnP K ) ` <. C , D >. ) ) -> H : ( X X. Y ) --> CC )
47 20 45 9 46 syl3anc 
 |-  ( ph -> H : ( X X. Y ) --> CC )
48 47 feqmptd 
 |-  ( ph -> H = ( y e. ( X X. Y ) |-> ( H ` y ) ) )
49 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 ) >. ) )
50 df-ov 
 |-  ( if ( x = B , C , R ) H if ( x = B , D , S ) ) = ( H ` <. if ( x = B , C , R ) , if ( x = B , D , S ) >. )
51 ovif12 
 |-  ( if ( x = B , C , R ) H if ( x = B , D , S ) ) = if ( x = B , ( C H D ) , ( R H S ) )
52 50 51 eqtr3i 
 |-  ( H ` <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) = if ( x = B , ( C H D ) , ( R H S ) )
53 49 52 eqtrdi 
 |-  ( y = <. if ( x = B , C , R ) , if ( x = B , D , S ) >. -> ( H ` y ) = if ( x = B , ( C H D ) , ( R H S ) ) )
54 43 44 48 53 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 ) ) ) )
55 eqid 
 |-  ( x e. A |-> R ) = ( x e. A |-> R )
56 55 1 dmmptd 
 |-  ( ph -> dom ( x e. A |-> R ) = A )
57 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 ) )
58 7 57 syl 
 |-  ( ph -> ( ( x e. A |-> R ) : dom ( x e. A |-> R ) --> CC /\ dom ( x e. A |-> R ) C_ CC /\ B e. CC ) )
59 58 simp2d 
 |-  ( ph -> dom ( x e. A |-> R ) C_ CC )
60 56 59 eqsstrrd 
 |-  ( ph -> A C_ CC )
61 58 simp3d 
 |-  ( ph -> B e. CC )
62 61 snssd 
 |-  ( ph -> { B } C_ CC )
63 60 62 unssd 
 |-  ( ph -> ( A u. { B } ) C_ CC )
64 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
65 13 63 64 sylancr 
 |-  ( ph -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
66 ssun2 
 |-  { B } C_ ( A u. { B } )
67 snssg 
 |-  ( B e. CC -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
68 61 67 syl 
 |-  ( ph -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
69 66 68 mpbiri 
 |-  ( ph -> B e. ( A u. { B } ) )
70 3 adantr 
 |-  ( ( ph /\ x e. A ) -> X C_ CC )
71 70 1 sseldd 
 |-  ( ( ph /\ x e. A ) -> R e. CC )
72 eqid 
 |-  ( K |`t ( A u. { B } ) ) = ( K |`t ( A u. { B } ) )
73 60 61 71 72 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 ) ) )
74 7 73 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , R ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
75 4 adantr 
 |-  ( ( ph /\ x e. A ) -> Y C_ CC )
76 75 2 sseldd 
 |-  ( ( ph /\ x e. A ) -> S e. CC )
77 60 61 76 72 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 ) ) )
78 8 77 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , D , S ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
79 65 45 45 69 74 78 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 ) )
80 15 topontopi 
 |-  ( K tX K ) e. Top
81 80 a1i 
 |-  ( ph -> ( K tX K ) e. Top )
82 43 fmpttd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) : ( A u. { B } ) --> ( X X. Y ) )
83 toponuni 
 |-  ( ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
84 65 83 syl 
 |-  ( ph -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
85 84 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 ) ) )
86 82 85 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 ) )
87 eqid 
 |-  U. ( K |`t ( A u. { B } ) ) = U. ( K |`t ( A u. { B } ) )
88 15 toponunii 
 |-  ( CC X. CC ) = U. ( K tX K )
89 87 88 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 ) ) )
90 81 86 17 89 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 ) ) )
91 79 90 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 ) )
92 6 oveq2i 
 |-  ( ( K |`t ( A u. { B } ) ) CnP J ) = ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) )
93 92 fveq1i 
 |-  ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) = ( ( ( K |`t ( A u. { B } ) ) CnP ( ( K tX K ) |`t ( X X. Y ) ) ) ` B )
94 91 93 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 ) )
95 iftrue 
 |-  ( x = B -> if ( x = B , C , R ) = C )
96 iftrue 
 |-  ( x = B -> if ( x = B , D , S ) = D )
97 95 96 opeq12d 
 |-  ( x = B -> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. = <. C , D >. )
98 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 ) >. )
99 opex 
 |-  <. C , D >. e. _V
100 97 98 99 fvmpt 
 |-  ( B e. ( A u. { B } ) -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) = <. C , D >. )
101 69 100 syl 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) = <. C , D >. )
102 101 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 >. ) )
103 9 102 eleqtrrd 
 |-  ( ph -> H e. ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> <. if ( x = B , C , R ) , if ( x = B , D , S ) >. ) ` B ) ) )
104 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 ) )
105 94 103 104 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 ) )
106 54 105 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 ) )
107 47 adantr 
 |-  ( ( ph /\ x e. A ) -> H : ( X X. Y ) --> CC )
108 107 1 2 fovrnd 
 |-  ( ( ph /\ x e. A ) -> ( R H S ) e. CC )
109 60 61 108 72 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 ) ) )
110 106 109 mpbird 
 |-  ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) limCC B ) )