Theorem f1oresf1orab

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022)

	Ref	Expression
Hypotheses	f1oresf1orab.1	|- F = ( x e. A |-> C )
	f1oresf1orab.2	|- ( ph -> F : A -1-1-onto-> B )
	f1oresf1orab.3	|- ( ph -> D C_ A )
	f1oresf1orab.4	|- ( ( ph /\ x e. A /\ y = C ) -> ( ch <-> x e. D ) )
Assertion	f1oresf1orab	|- ( ph -> ( F |` D ) : D -1-1-onto-> { y e. B | ch } )

Proof

Step	Hyp	Ref	Expression
1		f1oresf1orab.1	|- F = ( x e. A |-> C )
2		f1oresf1orab.2	|- ( ph -> F : A -1-1-onto-> B )
3		f1oresf1orab.3	|- ( ph -> D C_ A )
4		f1oresf1orab.4	|- ( ( ph /\ x e. A /\ y = C ) -> ( ch <-> x e. D ) )
5	1 2 4	f1oresrab	|- ( ph -> ( F |` { x e. A | x e. D } ) : { x e. A | x e. D } -1-1-onto-> { y e. B | ch } )
6		dfss7	|- ( D C_ A <-> { x e. A | x e. D } = D )
7	3 6	sylib	|- ( ph -> { x e. A | x e. D } = D )
8	7	eqcomd	|- ( ph -> D = { x e. A | x e. D } )
9	8	reseq2d	|- ( ph -> ( F |` D ) = ( F |` { x e. A | x e. D } ) )
10		eqidd	|- ( ph -> { y e. B | ch } = { y e. B | ch } )
11	9 8 10	f1oeq123d	|- ( ph -> ( ( F |` D ) : D -1-1-onto-> { y e. B | ch } <-> ( F |` { x e. A | x e. D } ) : { x e. A | x e. D } -1-1-onto-> { y e. B | ch } ) )
12	5 11	mpbird	|- ( ph -> ( F |` D ) : D -1-1-onto-> { y e. B | ch } )