Theorem resopunitintvd

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

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

Proof

Step	Hyp	Ref	Expression
1		resopunitintvd.1	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
2		ioosscn	$$⊢\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}{⟶}ℂ$$