Theorem resclunitintvd

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

	Ref	Expression
Hypothesis	resclunitintvd.1	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
Assertion	resclunitintvd	$$⊢\phi \to \left(x\in \left[0,1\right]⟼A\right):\left[0,1\right]\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		resclunitintvd.1	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
2		unitsscn	$$⊢\left[0,1\right]\subseteq ℂ$$
3		resmpt	$$⊢\left[0,1\right]\subseteq ℂ\to {\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[0,1\right]}=\left(x\in \left[0,1\right]⟼A\right)$$
4	2 3	ax-mp	$$⊢{\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[0,1\right]}=\left(x\in \left[0,1\right]⟼A\right)$$
5		rescncf	$$⊢\left[0,1\right]\subseteq ℂ\to \left(\left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ\to \left({\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[0,1\right]}\right):\left[0,1\right]\underset{cn}{⟶}ℂ\right)$$
6	2 5	ax-mp	$$⊢\left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ\to \left({\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[0,1\right]}\right):\left[0,1\right]\underset{cn}{⟶}ℂ$$
7	1 6	syl	$$⊢\phi \to \left({\left(x\in ℂ⟼A\right)\upharpoonright }_{\left[0,1\right]}\right):\left[0,1\right]\underset{cn}{⟶}ℂ$$
8	4 7	eqeltrrid	$$⊢\phi \to \left(x\in \left[0,1\right]⟼A\right):\left[0,1\right]\underset{cn}{⟶}ℂ$$