Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  metcnp3 Unicode version

Theorem metcnp3 18088
 Description: Two ways to express that is continuous at for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
Hypotheses
Ref Expression
metcn.2
metcn.4
Assertion
Ref Expression
metcnp3
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem metcnp3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 metcn.2 . . . . 5
21mopntopon 17987 . . . 4 TopOn
323ad2ant1 976 . . 3 TopOn
4 metcn.4 . . . . 5
54mopnval 17986 . . . 4
74mopntopon 17987 . . . 4 TopOn
873ad2ant2 977 . . 3 TopOn
9 simp3 957 . . 3
103, 6, 8, 9tgcnp 16985 . 2
11 simpll2 995 . . . . . . . 8
12 simplr 731 . . . . . . . . 9
13 simpll3 996 . . . . . . . . 9
14 ffvelrn 5665 . . . . . . . . 9
1512, 13, 14syl2anc 642 . . . . . . . 8
16 simpr 447 . . . . . . . 8
17 blcntr 17966 . . . . . . . 8
1811, 15, 16, 17syl3anc 1182 . . . . . . 7
19 rpxr 10363 . . . . . . . . . 10
2019adantl 452 . . . . . . . . 9
21 blelrn 17969 . . . . . . . . 9
2211, 15, 20, 21syl3anc 1182 . . . . . . . 8
23 eleq2 2346 . . . . . . . . . 10
24 sseq2 3202 . . . . . . . . . . . 12
2524anbi2d 684 . . . . . . . . . . 11
2625rexbidv 2566 . . . . . . . . . 10
2723, 26imbi12d 311 . . . . . . . . 9
2827rspcv 2882 . . . . . . . 8
2922, 28syl 15 . . . . . . 7
3018, 29mpid 37 . . . . . 6
31 simpl1 958 . . . . . . . . . . . 12
3231ad2antrr 706 . . . . . . . . . . 11
33 simplrr 737 . . . . . . . . . . 11
34 simpr 447 . . . . . . . . . . 11
351mopni2 18041 . . . . . . . . . . 11
3632, 33, 34, 35syl3anc 1182 . . . . . . . . . 10
37 imass2 5051 . . . . . . . . . . . . 13
38 sstr2 3188 . . . . . . . . . . . . 13
3937, 38syl 15 . . . . . . . . . . . 12
4039com12 27 . . . . . . . . . . 11
4140reximdv 2656 . . . . . . . . . 10
4236, 41syl5com 26 . . . . . . . . 9
4342expimpd 586 . . . . . . . 8
4443expr 598 . . . . . . 7
4544rexlimdv 2668 . . . . . 6
4630, 45syld 40 . . . . 5
4746ralrimdva 2635 . . . 4
48 simpl2 959 . . . . . . . . 9
49 blss 17974 . . . . . . . . . 10
50493expib 1154 . . . . . . . . 9
5148, 50syl 15 . . . . . . . 8
52 r19.29r 2686 . . . . . . . . . 10
5331ad3antrrr 710 . . . . . . . . . . . . . . . 16
5413ad2antrr 706 . . . . . . . . . . . . . . . 16
55 rpxr 10363 . . . . . . . . . . . . . . . . 17
5655ad2antrl 708 . . . . . . . . . . . . . . . 16
571blopn 18048 . . . . . . . . . . . . . . . 16
5853, 54, 56, 57syl3anc 1182 . . . . . . . . . . . . . . 15
59 simprl 732 . . . . . . . . . . . . . . . 16
60 blcntr 17966 . . . . . . . . . . . . . . . 16
6153, 54, 59, 60syl3anc 1182 . . . . . . . . . . . . . . 15
62 sstr 3189 . . . . . . . . . . . . . . . . 17
6362ad2ant2l 726 . . . . . . . . . . . . . . . 16
6463ancoms 439 . . . . . . . . . . . . . . 15
65 eleq2 2346 . . . . . . . . . . . . . . . . 17
66 imaeq2 5010 . . . . . . . . . . . . . . . . . 18
6766sseq1d 3207 . . . . . . . . . . . . . . . . 17
6865, 67anbi12d 691 . . . . . . . . . . . . . . . 16
6968rspcev 2886 . . . . . . . . . . . . . . 15
7058, 61, 64, 69syl12anc 1180 . . . . . . . . . . . . . 14
7170expr 598 . . . . . . . . . . . . 13
7271rexlimdva 2669 . . . . . . . . . . . 12
7372expimpd 586 . . . . . . . . . . 11
7473rexlimdva 2669 . . . . . . . . . 10
7552, 74syl5 28 . . . . . . . . 9
7675exp3a 425 . . . . . . . 8
7751, 76syld 40 . . . . . . 7
7877com23 72 . . . . . 6
7978exp4a 589 . . . . 5
8079ralrimdv 2634 . . . 4
8147, 80impbid 183 . . 3
8281pm5.32da 622 . 2
8310, 82bitrd 244 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1625   wcel 1686  wral 2545  wrex 2546   wss 3154   crn 4692  cima 4694  wf 5253  cfv 5257  (class class class)co 5860  cxr 8868  crp 10356  ctg 13344  cxmt 16371  cbl 16373  cmopn 16374  TopOnctopon 16634   ccnp 16957 This theorem is referenced by:  metcnp  18089 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816  ax-pre-sup 8817 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-er 6662  df-map 6776  df-en 6866  df-dom 6867  df-sdom 6868  df-sup 7196  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-div 9426  df-nn 9749  df-2 9806  df-n0 9968  df-z 10027  df-uz 10233  df-q 10319  df-rp 10357  df-xneg 10454  df-xadd 10455  df-xmul 10456  df-topgen 13346  df-xmet 16375  df-bl 16377  df-mopn 16378  df-top 16638  df-bases 16640  df-topon 16641  df-cnp 16960
 Copyright terms: Public domain W3C validator