Metamath Proof Explorer

Theorem tx1cn

Description: Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion tx1cn 
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )

Proof

Step Hyp Ref Expression
1 f1stres 
 |-  ( 1st |` ( X X. Y ) ) : ( X X. Y ) --> X
2 1 a1i 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) : ( X X. Y ) --> X )
3 ffn 
 |-  ( ( 1st |` ( X X. Y ) ) : ( X X. Y ) --> X -> ( 1st |` ( X X. Y ) ) Fn ( X X. Y ) )
4 elpreima 
 |-  ( ( 1st |` ( X X. Y ) ) Fn ( X X. Y ) -> ( z e. ( `' ( 1st |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ ( ( 1st |` ( X X. Y ) ) ` z ) e. w ) ) )
5 1 3 4 mp2b 
 |-  ( z e. ( `' ( 1st |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ ( ( 1st |` ( X X. Y ) ) ` z ) e. w ) )
6 fvres 
 |-  ( z e. ( X X. Y ) -> ( ( 1st |` ( X X. Y ) ) ` z ) = ( 1st ` z ) )
7 6 eleq1d 
 |-  ( z e. ( X X. Y ) -> ( ( ( 1st |` ( X X. Y ) ) ` z ) e. w <-> ( 1st ` z ) e. w ) )
8 1st2nd2 
 |-  ( z e. ( X X. Y ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
9 xp2nd 
 |-  ( z e. ( X X. Y ) -> ( 2nd ` z ) e. Y )
10 elxp6 
 |-  ( z e. ( w X. Y ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. w /\ ( 2nd ` z ) e. Y ) ) )
11 anass 
 |-  ( ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. w ) /\ ( 2nd ` z ) e. Y ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. w /\ ( 2nd ` z ) e. Y ) ) )
12 an32 
 |-  ( ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. w ) /\ ( 2nd ` z ) e. Y ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 2nd ` z ) e. Y ) /\ ( 1st ` z ) e. w ) )
13 10 11 12 3bitr2i 
 |-  ( z e. ( w X. Y ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 2nd ` z ) e. Y ) /\ ( 1st ` z ) e. w ) )
14 13 baib 
 |-  ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 2nd ` z ) e. Y ) -> ( z e. ( w X. Y ) <-> ( 1st ` z ) e. w ) )
15 8 9 14 syl2anc 
 |-  ( z e. ( X X. Y ) -> ( z e. ( w X. Y ) <-> ( 1st ` z ) e. w ) )
16 7 15 bitr4d 
 |-  ( z e. ( X X. Y ) -> ( ( ( 1st |` ( X X. Y ) ) ` z ) e. w <-> z e. ( w X. Y ) ) )
17 16 pm5.32i 
 |-  ( ( z e. ( X X. Y ) /\ ( ( 1st |` ( X X. Y ) ) ` z ) e. w ) <-> ( z e. ( X X. Y ) /\ z e. ( w X. Y ) ) )
18 5 17 bitri 
 |-  ( z e. ( `' ( 1st |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ z e. ( w X. Y ) ) )
19 toponss 
 |-  ( ( R e. ( TopOn ` X ) /\ w e. R ) -> w C_ X )
20 19 adantlr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> w C_ X )
21 xpss1 
 |-  ( w C_ X -> ( w X. Y ) C_ ( X X. Y ) )
22 20 21 syl 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( w X. Y ) C_ ( X X. Y ) )
23 22 sseld 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( z e. ( w X. Y ) -> z e. ( X X. Y ) ) )
24 23 pm4.71rd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( z e. ( w X. Y ) <-> ( z e. ( X X. Y ) /\ z e. ( w X. Y ) ) ) )
25 18 24 bitr4id 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( z e. ( `' ( 1st |` ( X X. Y ) ) " w ) <-> z e. ( w X. Y ) ) )
26 25 eqrdv 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( `' ( 1st |` ( X X. Y ) ) " w ) = ( w X. Y ) )
27 toponmax 
 |-  ( S e. ( TopOn ` Y ) -> Y e. S )
28 27 ad2antlr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> Y e. S )
29 txopn 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( w e. R /\ Y e. S ) ) -> ( w X. Y ) e. ( R tX S ) )
30 29 anassrs 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) /\ Y e. S ) -> ( w X. Y ) e. ( R tX S ) )
31 28 30 mpdan 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( w X. Y ) e. ( R tX S ) )
32 26 31 eqeltrd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. R ) -> ( `' ( 1st |` ( X X. Y ) ) " w ) e. ( R tX S ) )
33 32 ralrimiva 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> A. w e. R ( `' ( 1st |` ( X X. Y ) ) " w ) e. ( R tX S ) )
34 txtopon 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) )
35 simpl 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> R e. ( TopOn ` X ) )
36 iscn 
 |-  ( ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) /\ R e. ( TopOn ` X ) ) -> ( ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) <-> ( ( 1st |` ( X X. Y ) ) : ( X X. Y ) --> X /\ A. w e. R ( `' ( 1st |` ( X X. Y ) ) " w ) e. ( R tX S ) ) ) )
37 34 35 36 syl2anc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) <-> ( ( 1st |` ( X X. Y ) ) : ( X X. Y ) --> X /\ A. w e. R ( `' ( 1st |` ( X X. Y ) ) " w ) e. ( R tX S ) ) ) )
38 2 33 37 mpbir2and 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )