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

Theorem cnrest2 17114
 Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnrest2 TopOn t

Proof of Theorem cnrest2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cntop1 17070 . . . 4
21a1i 10 . . 3 TopOn
3 eqid 2358 . . . . . . . 8
4 eqid 2358 . . . . . . . 8
53, 4cnf 17076 . . . . . . 7
6 ffn 5469 . . . . . . 7
75, 6syl 15 . . . . . 6
87a1i 10 . . . . 5 TopOn
9 simp2 956 . . . . 5 TopOn
108, 9jctird 528 . . . 4 TopOn
11 df-f 5338 . . . 4
1210, 11syl6ibr 218 . . 3 TopOn
132, 12jcad 519 . 2 TopOn
14 cntop1 17070 . . . . 5 t
1514adantl 452 . . . 4 TopOn t
163toptopon 16771 . . . . . 6 TopOn
1715, 16sylib 188 . . . . 5 TopOn t TopOn
18 resttopon 16992 . . . . . . 7 TopOn t TopOn
19183adant2 974 . . . . . 6 TopOn t TopOn
2019adantr 451 . . . . 5 TopOn t t TopOn
21 simpr 447 . . . . 5 TopOn t t
22 cnf2 17079 . . . . 5 TopOn t TopOn t
2317, 20, 21, 22syl3anc 1182 . . . 4 TopOn t
2415, 23jca 518 . . 3 TopOn t
2524ex 423 . 2 TopOn t
26 vex 2867 . . . . . . . . 9
2726inex1 4234 . . . . . . . 8
2827a1i 10 . . . . . . 7 TopOn
29 simpl1 958 . . . . . . . 8 TopOn TopOn
30 simpl3 960 . . . . . . . . 9 TopOn
31 toponmax 16766 . . . . . . . . . 10 TopOn
3229, 31syl 15 . . . . . . . . 9 TopOn
33 ssexg 4239 . . . . . . . . 9
3430, 32, 33syl2anc 642 . . . . . . . 8 TopOn
35 elrest 13425 . . . . . . . 8 TopOn t
3629, 34, 35syl2anc 642 . . . . . . 7 TopOn t
37 imaeq2 5087 . . . . . . . . 9
3837eleq1d 2424 . . . . . . . 8
3938adantl 452 . . . . . . 7 TopOn
4028, 36, 39ralxfr2d 4629 . . . . . 6 TopOn t
41 simplrr 737 . . . . . . . . . 10 TopOn
42 ffun 5471 . . . . . . . . . 10
43 inpreima 5732 . . . . . . . . . 10
4441, 42, 433syl 18 . . . . . . . . 9 TopOn
45 cnvimass 5112 . . . . . . . . . . . 12
46 cnvimarndm 5113 . . . . . . . . . . . 12
4745, 46sseqtr4i 3287 . . . . . . . . . . 11
48 simpll2 995 . . . . . . . . . . . 12 TopOn
49 imass2 5128 . . . . . . . . . . . 12
5048, 49syl 15 . . . . . . . . . . 11 TopOn
5147, 50syl5ss 3266 . . . . . . . . . 10 TopOn
52 df-ss 3242 . . . . . . . . . 10
5351, 52sylib 188 . . . . . . . . 9 TopOn
5444, 53eqtrd 2390 . . . . . . . 8 TopOn
5554eleq1d 2424 . . . . . . 7 TopOn
5655ralbidva 2635 . . . . . 6 TopOn
57 simprr 733 . . . . . . . 8 TopOn
58 fss 5477 . . . . . . . 8
5957, 30, 58syl2anc 642 . . . . . . 7 TopOn
6059biantrurd 494 . . . . . 6 TopOn
6140, 56, 603bitrrd 271 . . . . 5 TopOn t
6257biantrurd 494 . . . . 5 TopOn t t
6361, 62bitrd 244 . . . 4 TopOn t
64 simprl 732 . . . . . 6 TopOn
6564, 16sylib 188 . . . . 5 TopOn TopOn
66 iscn 17065 . . . . 5 TopOn TopOn
6765, 29, 66syl2anc 642 . . . 4 TopOn
6819adantr 451 . . . . 5 TopOn t TopOn
69 iscn 17065 . . . . 5 TopOn t TopOn t t
7065, 68, 69syl2anc 642 . . . 4 TopOn t t
7163, 67, 703bitr4d 276 . . 3 TopOn t
7271ex 423 . 2 TopOn t
7313, 25, 72pm5.21ndd 343 1 TopOn t
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1642   wcel 1710  wral 2619  wrex 2620  cvv 2864   cin 3227   wss 3228  cuni 3906  ccnv 4767   cdm 4768   crn 4769  cima 4771   wfun 5328   wfn 5329  wf 5330  cfv 5334  (class class class)co 5942   ↾t crest 13418  ctop 16731  TopOnctopon 16732   ccn 17054 This theorem is referenced by:  cnrest2r  17115  rncmp  17223  conima  17251  concn  17252  kgencn2  17352  kgencn3  17353  qtoprest  17508  hmeores  17562  symgtgp  17880  submtmd  17883  subgtgp  17884  metdcn2  18441  metdscn2  18458  cnmptre  18523  iimulcn  18534  icchmeo  18537  evth  18555  evth2  18556  lebnumlem2  18558  reparphti  18593  efrlim  20369  rmulccn  23470  raddcn  23471  xrge0mulc1cn  23483  cvxpcon  24177  cvxscon  24178  cvmliftmolem1  24216  cvmliftlem8  24227  cvmlift2lem9  24246  cvmlift3lem6  24259  areacirclem4  25519  ivthALT  25582  cnres2  25806  cnresima  25807  refsumcn  27024 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-recs 6472  df-rdg 6507  df-oadd 6567  df-er 6744  df-map 6859  df-en 6949  df-fin 6952  df-fi 7252  df-rest 13420  df-topgen 13437  df-top 16736  df-bases 16738  df-topon 16739  df-cn 17057
 Copyright terms: Public domain W3C validator