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 ) )