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 )