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

Theorem cnmpt2nd 19142
Description: The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
cnmpt21.j  |-  ( ph  ->  J  e.  (TopOn `  X ) )
cnmpt21.k  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
Assertion
Ref Expression
cnmpt2nd  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  y )  e.  ( ( J  tX  K
)  Cn  K ) )
Distinct variable groups:    x, y, ph    x, X, y    x, Y, y
Allowed substitution hints:    J( x, y)    K( x, y)

Proof of Theorem cnmpt2nd
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 fo2nd 6596 . . . . . 6  |-  2nd : _V -onto-> _V
2 fofn 5619 . . . . . 6  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
31, 2ax-mp 5 . . . . 5  |-  2nd  Fn  _V
4 ssv 3373 . . . . 5  |-  ( X  X.  Y )  C_  _V
5 fnssres 5521 . . . . 5  |-  ( ( 2nd  Fn  _V  /\  ( X  X.  Y
)  C_  _V )  ->  ( 2nd  |`  ( X  X.  Y ) )  Fn  ( X  X.  Y ) )
63, 4, 5mp2an 667 . . . 4  |-  ( 2nd  |`  ( X  X.  Y
) )  Fn  ( X  X.  Y )
7 dffn5 5734 . . . 4  |-  ( ( 2nd  |`  ( X  X.  Y ) )  Fn  ( X  X.  Y
)  <->  ( 2nd  |`  ( X  X.  Y ) )  =  ( z  e.  ( X  X.  Y
)  |->  ( ( 2nd  |`  ( X  X.  Y
) ) `  z
) ) )
86, 7mpbi 208 . . 3  |-  ( 2nd  |`  ( X  X.  Y
) )  =  ( z  e.  ( X  X.  Y )  |->  ( ( 2nd  |`  ( X  X.  Y ) ) `
 z ) )
9 fvres 5701 . . . 4  |-  ( z  e.  ( X  X.  Y )  ->  (
( 2nd  |`  ( X  X.  Y ) ) `
 z )  =  ( 2nd `  z
) )
109mpteq2ia 4371 . . 3  |-  ( z  e.  ( X  X.  Y )  |->  ( ( 2nd  |`  ( X  X.  Y ) ) `  z ) )  =  ( z  e.  ( X  X.  Y ) 
|->  ( 2nd `  z
) )
11 vex 2973 . . . . 5  |-  x  e. 
_V
12 vex 2973 . . . . 5  |-  y  e. 
_V
1311, 12op2ndd 6587 . . . 4  |-  ( z  =  <. x ,  y
>.  ->  ( 2nd `  z
)  =  y )
1413mpt2mpt 6181 . . 3  |-  ( z  e.  ( X  X.  Y )  |->  ( 2nd `  z ) )  =  ( x  e.  X ,  y  e.  Y  |->  y )
158, 10, 143eqtri 2465 . 2  |-  ( 2nd  |`  ( X  X.  Y
) )  =  ( x  e.  X , 
y  e.  Y  |->  y )
16 cnmpt21.j . . 3  |-  ( ph  ->  J  e.  (TopOn `  X ) )
17 cnmpt21.k . . 3  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
18 tx2cn 19083 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( 2nd  |`  ( X  X.  Y
) )  e.  ( ( J  tX  K
)  Cn  K ) )
1916, 17, 18syl2anc 656 . 2  |-  ( ph  ->  ( 2nd  |`  ( X  X.  Y ) )  e.  ( ( J 
tX  K )  Cn  K ) )
2015, 19syl5eqelr 2526 1  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  y )  e.  ( ( J  tX  K
)  Cn  K ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761   _Vcvv 2970    C_ wss 3325    e. cmpt 4347    X. cxp 4834    |` cres 4838    Fn wfn 5410   -onto->wfo 5413   ` cfv 5415  (class class class)co 6090    e. cmpt2 6092   2ndc2nd 6575  TopOnctopon 18399    Cn ccn 18728    tX ctx 19033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fo 5421  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-1st 6576  df-2nd 6577  df-map 7212  df-topgen 14378  df-top 18403  df-bases 18405  df-topon 18406  df-cn 18731  df-tx 19035
This theorem is referenced by:  cnmptcom  19151  xkofvcn  19157  cnmptk2  19159  txhmeo  19276  txswaphmeo  19278  ptunhmeo  19281  xkohmeo  19288  tgpsubcn  19561  istgp2  19562  oppgtmd  19568  prdstmdd  19594  dvrcn  19658  divcn  20344  cnrehmeo  20425  htpycom  20448  htpyco1  20450  htpycc  20452  reparphti  20469  pcohtpylem  20491  pcorevlem  20498  cxpcn  22126  vmcn  24013  dipcn  24037  mndpluscn  26276  cvxscon  27046  cvmlift2lem6  27111
  Copyright terms: Public domain W3C validator