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

Theorem cnmpt2nd 20688
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 6834 . . . . . 6  |-  2nd : _V -onto-> _V
2 fofn 5818 . . . . . 6  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
31, 2ax-mp 5 . . . . 5  |-  2nd  Fn  _V
4 ssv 3490 . . . . 5  |-  ( X  X.  Y )  C_  _V
5 fnssres 5713 . . . . 5  |-  ( ( 2nd  Fn  _V  /\  ( X  X.  Y
)  C_  _V )  ->  ( 2nd  |`  ( X  X.  Y ) )  Fn  ( X  X.  Y ) )
63, 4, 5mp2an 677 . . . 4  |-  ( 2nd  |`  ( X  X.  Y
) )  Fn  ( X  X.  Y )
7 dffn5 5932 . . . 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 212 . . 3  |-  ( 2nd  |`  ( X  X.  Y
) )  =  ( z  e.  ( X  X.  Y )  |->  ( ( 2nd  |`  ( X  X.  Y ) ) `
 z ) )
9 fvres 5901 . . . 4  |-  ( z  e.  ( X  X.  Y )  ->  (
( 2nd  |`  ( X  X.  Y ) ) `
 z )  =  ( 2nd `  z
) )
109mpteq2ia 4512 . . 3  |-  ( z  e.  ( X  X.  Y )  |->  ( ( 2nd  |`  ( X  X.  Y ) ) `  z ) )  =  ( z  e.  ( X  X.  Y ) 
|->  ( 2nd `  z
) )
11 vex 3088 . . . . 5  |-  x  e. 
_V
12 vex 3088 . . . . 5  |-  y  e. 
_V
1311, 12op2ndd 6824 . . . 4  |-  ( z  =  <. x ,  y
>.  ->  ( 2nd `  z
)  =  y )
1413mpt2mpt 6408 . . 3  |-  ( z  e.  ( X  X.  Y )  |->  ( 2nd `  z ) )  =  ( x  e.  X ,  y  e.  Y  |->  y )
158, 10, 143eqtri 2456 . 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 20629 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( 2nd  |`  ( X  X.  Y
) )  e.  ( ( J  tX  K
)  Cn  K ) )
1916, 17, 18syl2anc 666 . 2  |-  ( ph  ->  ( 2nd  |`  ( X  X.  Y ) )  e.  ( ( J 
tX  K )  Cn  K ) )
2015, 19syl5eqelr 2517 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 1438    e. wcel 1873   _Vcvv 3085    C_ wss 3442    |-> cmpt 4488    X. cxp 4857    |` cres 4861    Fn wfn 5602   -onto->wfo 5605   ` cfv 5607  (class class class)co 6311    |-> cmpt2 6313   2ndc2nd 6812  TopOnctopon 19922    Cn ccn 20244    tX ctx 20579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-iun 4307  df-br 4430  df-opab 4489  df-mpt 4490  df-id 4774  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-fo 5613  df-fv 5615  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-1st 6813  df-2nd 6814  df-map 7491  df-topgen 15347  df-top 19925  df-bases 19926  df-topon 19927  df-cn 20247  df-tx 20581
This theorem is referenced by:  cnmptcom  20697  xkofvcn  20703  cnmptk2  20705  txhmeo  20822  txswaphmeo  20824  ptunhmeo  20827  xkohmeo  20834  tgpsubcn  21109  istgp2  21110  oppgtmd  21116  prdstmdd  21142  dvrcn  21202  divcn  21904  cnrehmeo  21985  htpycom  22011  htpyco1  22013  htpycc  22015  reparphti  22032  pcohtpylem  22054  pcorevlem  22061  cxpcn  23689  vmcn  26339  dipcn  26363  mndpluscn  28746  cvxscon  29980  cvmlift2lem6  30045
  Copyright terms: Public domain W3C validator