Metamath Proof Explorer


Theorem resopunitintvd

Description: Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis resopunitintvd.1
|- ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
Assertion resopunitintvd
|- ( ph -> ( x e. ( 0 (,) 1 ) |-> A ) e. ( ( 0 (,) 1 ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 resopunitintvd.1
 |-  ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
2 ioosscn
 |-  ( 0 (,) 1 ) C_ CC
3 resmpt
 |-  ( ( 0 (,) 1 ) C_ CC -> ( ( x e. CC |-> A ) |` ( 0 (,) 1 ) ) = ( x e. ( 0 (,) 1 ) |-> A ) )
4 2 3 ax-mp
 |-  ( ( x e. CC |-> A ) |` ( 0 (,) 1 ) ) = ( x e. ( 0 (,) 1 ) |-> A )
5 rescncf
 |-  ( ( 0 (,) 1 ) C_ CC -> ( ( x e. CC |-> A ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> A ) |` ( 0 (,) 1 ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) ) )
6 2 5 ax-mp
 |-  ( ( x e. CC |-> A ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> A ) |` ( 0 (,) 1 ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) )
7 1 6 syl
 |-  ( ph -> ( ( x e. CC |-> A ) |` ( 0 (,) 1 ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) )
8 4 7 eqeltrrid
 |-  ( ph -> ( x e. ( 0 (,) 1 ) |-> A ) e. ( ( 0 (,) 1 ) -cn-> CC ) )