Theorem imasetpreimafvbijlemfv1

Description: Lemma for imasetpreimafvbij : for a preimage of a value of function F there is an element of the preimage so that the value of the mapping H at this preimage is the function value at this element. (Contributed by AV, 5-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	imasetpreimafvbijlemfv1	|- ( ( F Fn A /\ X e. P ) -> E. y e. X ( H ` X ) = ( F ` y ) )

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	0nelsetpreimafv	|- ( F Fn A -> (/) e/ P )
4		elnelne2	|- ( ( X e. P /\ (/) e/ P ) -> X =/= (/) )
5	4	expcom	|- ( (/) e/ P -> ( X e. P -> X =/= (/) ) )
6	3 5	syl	|- ( F Fn A -> ( X e. P -> X =/= (/) ) )
7	6	imp	|- ( ( F Fn A /\ X e. P ) -> X =/= (/) )
8		simpr	|- ( ( ( F Fn A /\ X e. P ) /\ y e. X ) -> y e. X )
9	1 2	imasetpreimafvbijlemfv	|- ( ( F Fn A /\ X e. P /\ y e. X ) -> ( H ` X ) = ( F ` y ) )
10	9	3expa	|- ( ( ( F Fn A /\ X e. P ) /\ y e. X ) -> ( H ` X ) = ( F ` y ) )
11	8 10	jca	|- ( ( ( F Fn A /\ X e. P ) /\ y e. X ) -> ( y e. X /\ ( H ` X ) = ( F ` y ) ) )
12	11	ex	|- ( ( F Fn A /\ X e. P ) -> ( y e. X -> ( y e. X /\ ( H ` X ) = ( F ` y ) ) ) )
13	12	eximdv	|- ( ( F Fn A /\ X e. P ) -> ( E. y y e. X -> E. y ( y e. X /\ ( H ` X ) = ( F ` y ) ) ) )
14		n0	|- ( X =/= (/) <-> E. y y e. X )
15		df-rex	|- ( E. y e. X ( H ` X ) = ( F ` y ) <-> E. y ( y e. X /\ ( H ` X ) = ( F ` y ) ) )
16	13 14 15	3imtr4g	|- ( ( F Fn A /\ X e. P ) -> ( X =/= (/) -> E. y e. X ( H ` X ) = ( F ` y ) ) )
17	7 16	mpd	|- ( ( F Fn A /\ X e. P ) -> E. y e. X ( H ` X ) = ( F ` y ) )