Theorem resopunitintvd

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

	Ref	Expression
Hypothesis	resopunitintvd.1	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
Assertion	resopunitintvd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐴 ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		resopunitintvd.1	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
2		ioosscn	⊢ ( 0 (,) 1 ) ⊆ ℂ
3		resmpt	⊢ ( ( 0 (,) 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 0 (,) 1 ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐴 ) )
4	2 3	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 0 (,) 1 ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐴 )
5		rescncf	⊢ ( ( 0 (,) 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 0 (,) 1 ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) ) )
6	2 5	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 0 (,) 1 ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
7	1 6	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ 𝐴 ) ↾ ( 0 (,) 1 ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
8	4 7	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝐴 ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )