Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  limccnp2cntop Unicode version

Theorem limccnp2cntop 12888
 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.) (Revised by Jim Kingdon, 14-Nov-2023.)
Hypotheses
Ref Expression
limccnp2.r
limccnp2.s
limccnp2.x
limccnp2.y
limccnp2cntop.k
limccnp2.j t
limccnp2.c lim
limccnp2.d lim
limccnp2.h
Assertion
Ref Expression
limccnp2cntop lim
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem limccnp2cntop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccnp2.j . . . . 5 t
2 limccnp2cntop.k . . . . . . . 8
32cntoptopon 12774 . . . . . . 7 TopOn
4 txtopon 12504 . . . . . . 7 TopOn TopOn TopOn
53, 3, 4mp2an 423 . . . . . 6 TopOn
6 limccnp2.x . . . . . . 7
7 limccnp2.y . . . . . . 7
8 xpss12 4657 . . . . . . 7
96, 7, 8syl2anc 409 . . . . . 6
10 resttopon 12413 . . . . . 6 TopOn t TopOn
115, 9, 10sylancr 411 . . . . 5 t TopOn
121, 11eqeltrid 2227 . . . 4 TopOn
133a1i 9 . . . 4 TopOn
14 limccnp2.h . . . 4
15 cnpf2 12449 . . . 4 TopOn TopOn
1612, 13, 14, 15syl3anc 1217 . . 3
172cntoptop 12775 . . . . . . . . . . 11
1817a1i 9 . . . . . . . . . . 11
19 txtop 12502 . . . . . . . . . . 11
2017, 18, 19sylancr 411 . . . . . . . . . 10
21 cnex 7795 . . . . . . . . . . . . 13
2221a1i 9 . . . . . . . . . . . 12
2322, 6ssexd 4077 . . . . . . . . . . 11
2422, 7ssexd 4077 . . . . . . . . . . 11
25 xpexg 4664 . . . . . . . . . . 11
2623, 24, 25syl2anc 409 . . . . . . . . . 10
27 resttop 12412 . . . . . . . . . 10 t
2820, 26, 27syl2anc 409 . . . . . . . . 9 t
291, 28eqeltrid 2227 . . . . . . . 8
30 toptopon2 12259 . . . . . . . 8 TopOn
3129, 30sylib 121 . . . . . . 7 TopOn
32 cnprcl2k 12448 . . . . . . 7 TopOn
3331, 18, 14, 32syl3anc 1217 . . . . . 6
34 toponuni 12255 . . . . . . 7 TopOn
3512, 34syl 14 . . . . . 6
3633, 35eleqtrrd 2220 . . . . 5
37 opelxp 4580 . . . . 5
3836, 37sylib 121 . . . 4
3938simpld 111 . . 3
4038simprd 113 . . 3
4116, 39, 40fovrnd 5926 . 2
42 txrest 12518 . . . . . . . . . . . . 13 t t t
4318, 18, 23, 24, 42syl22anc 1218 . . . . . . . . . . . 12 t t t
441, 43syl5eq 2185 . . . . . . . . . . 11 t t
45 cnxmet 12773 . . . . . . . . . . . . 13
46 eqid 2140 . . . . . . . . . . . . . 14
47 eqid 2140 . . . . . . . . . . . . . 14
4846, 2, 47metrest 12748 . . . . . . . . . . . . 13 t
4945, 6, 48sylancr 411 . . . . . . . . . . . 12 t
50 eqid 2140 . . . . . . . . . . . . . 14
51 eqid 2140 . . . . . . . . . . . . . 14
5250, 2, 51metrest 12748 . . . . . . . . . . . . 13 t
5345, 7, 52sylancr 411 . . . . . . . . . . . 12 t
5449, 53oveq12d 5803 . . . . . . . . . . 11 t t
5544, 54eqtrd 2173 . . . . . . . . . 10
5655oveq1d 5800 . . . . . . . . 9
5756fveq1d 5434 . . . . . . . 8
5814, 57eleqtrd 2219 . . . . . . 7
59 xmetres2 12621 . . . . . . . . 9
6045, 6, 59sylancr 411 . . . . . . . 8
61 xmetres2 12621 . . . . . . . . 9
6245, 7, 61sylancr 411 . . . . . . . 8
6345a1i 9 . . . . . . . 8
6447, 51, 2txmetcnp 12760 . . . . . . . 8
6560, 62, 63, 38, 64syl31anc 1220 . . . . . . 7
6658, 65mpbid 146 . . . . . 6
6766simprd 113 . . . . 5
6867r19.21bi 2524 . . . 4
69 simpll 519 . . . . . 6
70 simprl 521 . . . . . 6
71 limccnp2.c . . . . . . . . 9 lim
72 eqid 2140 . . . . . . . . . . . 12
73 limccnp2.r . . . . . . . . . . . 12
7472, 73dmmptd 5264 . . . . . . . . . . 11
75 limcrcl 12869 . . . . . . . . . . . . 13 lim
7671, 75syl 14 . . . . . . . . . . . 12
7776simp2d 995 . . . . . . . . . . 11
7874, 77eqsstrrd 3140 . . . . . . . . . 10
7976simp3d 996 . . . . . . . . . 10
806adantr 274 . . . . . . . . . . 11
8180, 73sseldd 3104 . . . . . . . . . 10
8278, 79, 81limcmpted 12874 . . . . . . . . 9 lim #
8371, 82mpbid 146 . . . . . . . 8 #
8483simprd 113 . . . . . . 7 #
8584r19.21bi 2524 . . . . . 6 #
8669, 70, 85syl2anc 409 . . . . 5 #
8769adantr 274 . . . . . . 7 #
88 simplrl 525 . . . . . . 7 #
89 limccnp2.d . . . . . . . . . 10 lim
907adantr 274 . . . . . . . . . . . 12
91 limccnp2.s . . . . . . . . . . . 12
9290, 91sseldd 3104 . . . . . . . . . . 11
9378, 79, 92limcmpted 12874 . . . . . . . . . 10 lim #
9489, 93mpbid 146 . . . . . . . . 9 #
9594simprd 113 . . . . . . . 8 #
9695r19.21bi 2524 . . . . . . 7 #
9787, 88, 96syl2anc 409 . . . . . 6 # #
98 simp-5l 533 . . . . . . . 8 # #
9998, 73sylancom 417 . . . . . . 7 # #
10098, 91sylancom 417 . . . . . . 7 # #
1016ad4antr 486 . . . . . . 7 # #
1027ad4antr 486 . . . . . . 7 # #
10371ad4antr 486 . . . . . . 7 # # lim
10489ad4antr 486 . . . . . . 7 # # lim
10514ad4antr 486 . . . . . . 7 # #
106 nfv 1509 . . . . . . . . 9
107 nfv 1509 . . . . . . . . . 10
108 nfra1 2470 . . . . . . . . . 10 #
109107, 108nfan 1545 . . . . . . . . 9 #
110106, 109nfan 1545 . . . . . . . 8 #
111 nfv 1509 . . . . . . . . 9
112 nfra1 2470 . . . . . . . . 9 #
113111, 112nfan 1545 . . . . . . . 8 #
114110, 113nfan 1545 . . . . . . 7 # #
115 simp-4r 532 . . . . . . 7 # #
11670ad2antrr 480 . . . . . . 7 # #
117 simprr 522 . . . . . . . 8
118117ad2antrr 480 . . . . . . 7 # #
119 simplrl 525 . . . . . . 7 # #
120 simplrr 526 . . . . . . 7 # # #
121 simprl 521 . . . . . . 7 # #
122 simprr 522 . . . . . . 7 # # #
12399, 100, 101, 102, 2, 1, 103, 104, 105, 114, 115, 116, 118, 119, 120, 121, 122limccnp2lem 12887 . . . . . 6 # # #
12497, 123rexlimddv 2558 . . . . 5 # #
12586, 124rexlimddv 2558 . . . 4 #
12668, 125rexlimddv 2558 . . 3 #
127126ralrimiva 2509 . 2 #
12816adantr 274 . . . 4
129128, 73, 91fovrnd 5926 . . 3
13078, 79, 129limcmpted 12874 . 2 lim #
13141, 127, 130mpbir2and 929 1 lim
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332   wcel 1481  wral 2417  wrex 2418  cvv 2690   wss 3077  cop 3536  cuni 3745   class class class wbr 3938   cmpt 3998   cxp 4548   cdm 4550   cres 4552   ccom 4554  wf 5130  cfv 5134  (class class class)co 5785  cc 7669   clt 7851   cmin 7984   # cap 8394  crp 9497  cabs 10828   ↾t crest 12193  cxmet 12222  cmopn 12227  ctop 12237  TopOnctopon 12250   ccnp 12428   ctx 12494   lim climc 12865 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-mulrcl 7770  ax-addcom 7771  ax-mulcom 7772  ax-addass 7773  ax-mulass 7774  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-1rid 7778  ax-0id 7779  ax-rnegex 7780  ax-precex 7781  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-apti 7786  ax-pre-ltadd 7787  ax-pre-mulgt0 7788  ax-pre-mulext 7789  ax-arch 7790  ax-caucvg 7791 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-po 4228  df-iso 4229  df-iord 4298  df-on 4300  df-ilim 4301  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-isom 5143  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-1st 6049  df-2nd 6050  df-recs 6213  df-frec 6299  df-map 6555  df-pm 6556  df-sup 6887  df-inf 6888  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-reap 8388  df-ap 8395  df-div 8484  df-inn 8772  df-2 8830  df-3 8831  df-4 8832  df-n0 9029  df-z 9106  df-uz 9378  df-q 9466  df-rp 9498  df-xneg 9616  df-xadd 9617  df-seqfrec 10277  df-exp 10351  df-cj 10673  df-re 10674  df-im 10675  df-rsqrt 10829  df-abs 10830  df-rest 12195  df-topgen 12214  df-psmet 12229  df-xmet 12230  df-met 12231  df-bl 12232  df-mopn 12233  df-top 12238  df-topon 12251  df-bases 12283  df-cnp 12431  df-tx 12495  df-limced 12867 This theorem is referenced by:  dvcnp2cntop  12905  dvaddxxbr  12907  dvmulxxbr  12908  dvcoapbr  12913
 Copyright terms: Public domain W3C validator