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

Theorem cnmptid 20328
Description: The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypothesis
Ref Expression
cnmptid.j  |-  ( ph  ->  J  e.  (TopOn `  X ) )
Assertion
Ref Expression
cnmptid  |-  ( ph  ->  ( x  e.  X  |->  x )  e.  ( J  Cn  J ) )
Distinct variable groups:    ph, x    x, J    x, X

Proof of Theorem cnmptid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 equcom 1799 . . . . . 6  |-  ( x  =  y  <->  y  =  x )
21opabbii 4503 . . . . 5  |-  { <. x ,  y >.  |  x  =  y }  =  { <. x ,  y
>.  |  y  =  x }
3 dfid3 4785 . . . . 5  |-  _I  =  { <. x ,  y
>.  |  x  =  y }
4 mptv 4531 . . . . 5  |-  ( x  e.  _V  |->  x )  =  { <. x ,  y >.  |  y  =  x }
52, 3, 43eqtr4i 2493 . . . 4  |-  _I  =  ( x  e.  _V  |->  x )
65reseq1i 5258 . . 3  |-  (  _I  |`  X )  =  ( ( x  e.  _V  |->  x )  |`  X )
7 ssv 3509 . . . 4  |-  X  C_  _V
8 resmpt 5311 . . . 4  |-  ( X 
C_  _V  ->  ( ( x  e.  _V  |->  x )  |`  X )  =  ( x  e.  X  |->  x ) )
97, 8ax-mp 5 . . 3  |-  ( ( x  e.  _V  |->  x )  |`  X )  =  ( x  e.  X  |->  x )
106, 9eqtri 2483 . 2  |-  (  _I  |`  X )  =  ( x  e.  X  |->  x )
11 cnmptid.j . . 3  |-  ( ph  ->  J  e.  (TopOn `  X ) )
12 idcn 19925 . . 3  |-  ( J  e.  (TopOn `  X
)  ->  (  _I  |`  X )  e.  ( J  Cn  J ) )
1311, 12syl 16 . 2  |-  ( ph  ->  (  _I  |`  X )  e.  ( J  Cn  J ) )
1410, 13syl5eqelr 2547 1  |-  ( ph  ->  ( x  e.  X  |->  x )  e.  ( J  Cn  J ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823   _Vcvv 3106    C_ wss 3461   {copab 4496    |-> cmpt 4497    _I cid 4779    |` cres 4990   ` cfv 5570  (class class class)co 6270  TopOnctopon 19562    Cn ccn 19892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-map 7414  df-top 19566  df-topon 19569  df-cn 19895
This theorem is referenced by:  xkoinjcn  20354  txcon  20356  imasnopn  20357  imasncld  20358  imasncls  20359  pt1hmeo  20473  istgp2  20756  tmdmulg  20757  tmdlactcn  20767  clsnsg  20774  tgpt0  20783  tlmtgp  20864  nmcn  21515  expcn  21542  divccn  21543  cncfmptid  21582  cdivcncf  21587  iirevcn  21596  iihalf1cn  21598  iihalf2cn  21600  icchmeo  21607  evth2  21626  pcocn  21683  pcopt  21688  pcopt2  21689  pcoass  21690  csscld  21855  clsocv  21856  dvcnvlem  22543  resqrtcn  23291  sqrtcn  23292  efrlim  23497  ipasslem7  25949  occllem  26419  hmopidmchi  27268  rmulccn  28145  cvxpcon  28951  cvmlift2lem2  29013  cvmlift2lem3  29014  cvmliftphtlem  29026  cxpcncf2  31942
  Copyright terms: Public domain W3C validator