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	|- ( ph -> F : A --> B )
	fssrescdmd.c	|- ( ph -> C C_ A )
	fssrescdmd.d	|- ( ph -> ( F " C ) C_ D )
Assertion	fssrescdmd	|- ( ph -> ( F |` C ) : C --> D )

Proof

Step	Hyp	Ref	Expression
1		fssrescdmd.f	|- ( ph -> F : A --> B )
2		fssrescdmd.c	|- ( ph -> C C_ A )
3		fssrescdmd.d	|- ( ph -> ( F " C ) C_ D )
4	1	ffnd	|- ( ph -> F Fn A )
5	4 2	fnssresd	|- ( ph -> ( F |` C ) Fn C )
6		resima	|- ( ( F |` C ) " C ) = ( F " C )
7	6 3	eqsstrid	|- ( ph -> ( ( F |` C ) " C ) C_ D )
8	1	ffund	|- ( ph -> Fun F )
9	8	funresd	|- ( ph -> Fun ( F |` C ) )
10	1	fdmd	|- ( ph -> dom F = A )
11	2 10	sseqtrrd	|- ( ph -> C C_ dom F )
12		ssdmres	|- ( C C_ dom F <-> dom ( F |` C ) = C )
13	12	a1i	|- ( ph -> ( C C_ dom F <-> dom ( F |` C ) = C ) )
14		eqcom	|- ( dom ( F |` C ) = C <-> C = dom ( F |` C ) )
15	13 14	bitrdi	|- ( ph -> ( C C_ dom F <-> C = dom ( F |` C ) ) )
16	11 15	mpbid	|- ( ph -> C = dom ( F |` C ) )
17	16	eqimssd	|- ( ph -> C C_ dom ( F |` C ) )
18		funimass4	|- ( ( Fun ( F |` C ) /\ C C_ dom ( F |` C ) ) -> ( ( ( F |` C ) " C ) C_ D <-> A. x e. C ( ( F |` C ) ` x ) e. D ) )
19	9 17 18	syl2anc	|- ( ph -> ( ( ( F |` C ) " C ) C_ D <-> A. x e. C ( ( F |` C ) ` x ) e. D ) )
20	7 19	mpbid	|- ( ph -> A. x e. C ( ( F |` C ) ` x ) e. D )
21		ffnfv	|- ( ( F |` C ) : C --> D <-> ( ( F |` C ) Fn C /\ A. x e. C ( ( F |` C ) ` x ) e. D ) )
22	5 20 21	sylanbrc	|- ( ph -> ( F |` C ) : C --> D )