Theorem f1oresf1o

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

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

Proof

Step	Hyp	Ref	Expression
1		f1oresf1o.1	|- ( ph -> F : A -1-1-onto-> B )
2		f1oresf1o.2	|- ( ph -> D C_ A )
3		f1oresf1o.3	|- ( ph -> ( E. x e. D ( F ` x ) = y <-> ( y e. B /\ ch ) ) )
4		f1of1	|- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
5	1 4	syl	|- ( ph -> F : A -1-1-> B )
6		f1ores	|- ( ( F : A -1-1-> B /\ D C_ A ) -> ( F |` D ) : D -1-1-onto-> ( F " D ) )
7	5 2 6	syl2anc	|- ( ph -> ( F |` D ) : D -1-1-onto-> ( F " D ) )
8		f1ofun	|- ( F : A -1-1-onto-> B -> Fun F )
9	1 8	syl	|- ( ph -> Fun F )
10		f1odm	|- ( F : A -1-1-onto-> B -> dom F = A )
11	1 10	syl	|- ( ph -> dom F = A )
12	2 11	sseqtrrd	|- ( ph -> D C_ dom F )
13		dfimafn	|- ( ( Fun F /\ D C_ dom F ) -> ( F " D ) = { y | E. x e. D ( F ` x ) = y } )
14	9 12 13	syl2anc	|- ( ph -> ( F " D ) = { y | E. x e. D ( F ` x ) = y } )
15	3	abbidv	|- ( ph -> { y | E. x e. D ( F ` x ) = y } = { y | ( y e. B /\ ch ) } )
16		df-rab	|- { y e. B | ch } = { y | ( y e. B /\ ch ) }
17	15 16	eqtr4di	|- ( ph -> { y | E. x e. D ( F ` x ) = y } = { y e. B | ch } )
18	14 17	eqtr2d	|- ( ph -> { y e. B | ch } = ( F " D ) )
19	18	f1oeq3d	|- ( ph -> ( ( F |` D ) : D -1-1-onto-> { y e. B | ch } <-> ( F |` D ) : D -1-1-onto-> ( F " D ) ) )
20	7 19	mpbird	|- ( ph -> ( F |` D ) : D -1-1-onto-> { y e. B | ch } )