Theorem fssrescdmd

Description: Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025)

	Ref	Expression
Hypotheses	fssrescdmd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fssrescdmd.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	fssrescdmd.d	⊢ ( 𝜑 → ( 𝐹 “ 𝐶 ) ⊆ 𝐷 )
Assertion	fssrescdmd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fssrescdmd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fssrescdmd.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3		fssrescdmd.d	⊢ ( 𝜑 → ( 𝐹 “ 𝐶 ) ⊆ 𝐷 )
4	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
5	4 2	fnssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
6		resima	⊢ ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) = ( 𝐹 “ 𝐶 )
7	6 3	eqsstrid	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 )
8	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
9	8	funresd	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝐶 ) )
10	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
11	2 10	sseqtrrd	⊢ ( 𝜑 → 𝐶 ⊆ dom 𝐹 )
12		ssdmres	⊢ ( 𝐶 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 )
13	12	a1i	⊢ ( 𝜑 → ( 𝐶 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ) )
14		eqcom	⊢ ( dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ↔ 𝐶 = dom ( 𝐹 ↾ 𝐶 ) )
15	13 14	bitrdi	⊢ ( 𝜑 → ( 𝐶 ⊆ dom 𝐹 ↔ 𝐶 = dom ( 𝐹 ↾ 𝐶 ) ) )
16	11 15	mpbid	⊢ ( 𝜑 → 𝐶 = dom ( 𝐹 ↾ 𝐶 ) )
17	16	eqimssd	⊢ ( 𝜑 → 𝐶 ⊆ dom ( 𝐹 ↾ 𝐶 ) )
18		funimass4	⊢ ( ( Fun ( 𝐹 ↾ 𝐶 ) ∧ 𝐶 ⊆ dom ( 𝐹 ↾ 𝐶 ) ) → ( ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
19	9 17 18	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐶 ) “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
20	7 19	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 )
21		ffnfv	⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 ↔ ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ∈ 𝐷 ) )
22	5 20 21	sylanbrc	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐷 )