Theorem fvelsetpreimafv

Description: There is an element in a preimage S of function values so that S is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	fvelsetpreimafv	|- ( ( F Fn A /\ S e. P ) -> E. x e. S S = ( `' F " { ( F ` x ) } ) )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		preimafvsnel	|- ( ( F Fn A /\ x e. A ) -> x e. ( `' F " { ( F ` x ) } ) )
3	2	adantrr	|- ( ( F Fn A /\ ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) ) -> x e. ( `' F " { ( F ` x ) } ) )
4		eleq2	|- ( S = ( `' F " { ( F ` x ) } ) -> ( x e. S <-> x e. ( `' F " { ( F ` x ) } ) ) )
5	4	ad2antll	|- ( ( F Fn A /\ ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) ) -> ( x e. S <-> x e. ( `' F " { ( F ` x ) } ) ) )
6	3 5	mpbird	|- ( ( F Fn A /\ ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) ) -> x e. S )
7		simprr	|- ( ( F Fn A /\ ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) ) -> S = ( `' F " { ( F ` x ) } ) )
8	6 7	jca	|- ( ( F Fn A /\ ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) ) -> ( x e. S /\ S = ( `' F " { ( F ` x ) } ) ) )
9	8	ex	|- ( F Fn A -> ( ( x e. A /\ S = ( `' F " { ( F ` x ) } ) ) -> ( x e. S /\ S = ( `' F " { ( F ` x ) } ) ) ) )
10	9	reximdv2	|- ( F Fn A -> ( E. x e. A S = ( `' F " { ( F ` x ) } ) -> E. x e. S S = ( `' F " { ( F ` x ) } ) ) )
11	1	elsetpreimafv	|- ( S e. P -> E. x e. A S = ( `' F " { ( F ` x ) } ) )
12	10 11	impel	|- ( ( F Fn A /\ S e. P ) -> E. x e. S S = ( `' F " { ( F ` x ) } ) )