Theorem imasetpreimafvbij

Description: The mapping H is a bijective function between the set P of all preimages of values of function F and the range of F . (Contributed by AV, 22-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
	fundcmpsurinj.h	|- H = ( p e. P |-> U. ( F " p ) )
Assertion	imasetpreimafvbij	|- ( ( F Fn A /\ A e. V ) -> H : P -1-1-onto-> ( F " A ) )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		fundcmpsurinj.h	|- H = ( p e. P |-> U. ( F " p ) )
3	1 2	imasetpreimafvbijlemf1	|- ( F Fn A -> H : P -1-1-> ( F " A ) )
4	3	adantr	|- ( ( F Fn A /\ A e. V ) -> H : P -1-1-> ( F " A ) )
5	1 2	imasetpreimafvbijlemfo	|- ( ( F Fn A /\ A e. V ) -> H : P -onto-> ( F " A ) )
6		df-f1o	|- ( H : P -1-1-onto-> ( F " A ) <-> ( H : P -1-1-> ( F " A ) /\ H : P -onto-> ( F " A ) ) )
7	4 5 6	sylanbrc	|- ( ( F Fn A /\ A e. V ) -> H : P -1-1-onto-> ( F " A ) )