This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt2nd

Description: The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmpt21.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt21.k 
|- ( ph -> K e. ( TopOn ` Y ) )
Assertion cnmpt2nd 
|- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmpt21.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 fo2nd 
 |-  2nd : _V -onto-> _V
4 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
5 3 4 ax-mp 
 |-  2nd Fn _V
6 ssv 
 |-  ( X X. Y ) C_ _V
7 fnssres 
 |-  ( ( 2nd Fn _V /\ ( X X. Y ) C_ _V ) -> ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) )
8 5 6 7 mp2an 
 |-  ( 2nd |` ( X X. Y ) ) Fn ( X X. Y )
9 dffn5 
 |-  ( ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) <-> ( 2nd |` ( X X. Y ) ) = ( z e. ( X X. Y ) |-> ( ( 2nd |` ( X X. Y ) ) ` z ) ) )
10 8 9 mpbi 
 |-  ( 2nd |` ( X X. Y ) ) = ( z e. ( X X. Y ) |-> ( ( 2nd |` ( X X. Y ) ) ` z ) )
11 fvres 
 |-  ( z e. ( X X. Y ) -> ( ( 2nd |` ( X X. Y ) ) ` z ) = ( 2nd ` z ) )
12 11 mpteq2ia 
 |-  ( z e. ( X X. Y ) |-> ( ( 2nd |` ( X X. Y ) ) ` z ) ) = ( z e. ( X X. Y ) |-> ( 2nd ` z ) )
13 vex 
 |-  x e. _V
14 vex 
 |-  y e. _V
15 13 14 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
16 15 mpompt 
 |-  ( z e. ( X X. Y ) |-> ( 2nd ` z ) ) = ( x e. X , y e. Y |-> y )
17 10 12 16 3eqtri 
 |-  ( 2nd |` ( X X. Y ) ) = ( x e. X , y e. Y |-> y )
18 tx2cn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( J tX K ) Cn K ) )
19 1 2 18 syl2anc 
 |-  ( ph -> ( 2nd |` ( X X. Y ) ) e. ( ( J tX K ) Cn K ) )
20 17 19 eqeltrrid 
 |-  ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )