Metamath Proof Explorer

Theorem cnmpt1st

Description: The projection onto the first 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 cnmpt1st 
|- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )

Proof

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