Metamath Proof Explorer

Theorem abscncfALT

Description: Absolute value is continuous. Alternate proof of abscncf . (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion abscncfALT 
|- abs e. ( CC -cn-> RR )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
3 1 2 abscn 
 |-  abs e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
4 ssid 
 |-  CC C_ CC
5 ax-resscn 
 |-  RR C_ CC
6 1 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
7 6 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
8 7 restid 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
9 6 8 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
10 9 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
11 1 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
12 1 10 11 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) )
13 4 5 12 mp2an 
 |-  ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
14 3 13 eleqtrri 
 |-  abs e. ( CC -cn-> RR )