Theorem preimafvelsetpreimafv

Description: The preimage of a function value is an element of the class P of all preimages of function values. (Contributed by AV, 10-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		id	|- ( X e. A -> X e. A )
3		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
4	3	sneqd	|- ( x = X -> { ( F ` x ) } = { ( F ` X ) } )
5	4	imaeq2d	|- ( x = X -> ( `' F " { ( F ` x ) } ) = ( `' F " { ( F ` X ) } ) )
6	5	eqeq2d	|- ( x = X -> ( ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) <-> ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` X ) } ) ) )
7	6	adantl	|- ( ( X e. A /\ x = X ) -> ( ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) <-> ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` X ) } ) ) )
8		eqidd	|- ( X e. A -> ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` X ) } ) )
9	2 7 8	rspcedvd	|- ( X e. A -> E. x e. A ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) )
10	9	3ad2ant3	|- ( ( F Fn A /\ A e. V /\ X e. A ) -> E. x e. A ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) )
11		fnex	|- ( ( F Fn A /\ A e. V ) -> F e. _V )
12		cnvexg	|- ( F e. _V -> `' F e. _V )
13		imaexg	|- ( `' F e. _V -> ( `' F " { ( F ` X ) } ) e. _V )
14	11 12 13	3syl	|- ( ( F Fn A /\ A e. V ) -> ( `' F " { ( F ` X ) } ) e. _V )
15	14	3adant3	|- ( ( F Fn A /\ A e. V /\ X e. A ) -> ( `' F " { ( F ` X ) } ) e. _V )
16	1	elsetpreimafvb	|- ( ( `' F " { ( F ` X ) } ) e. _V -> ( ( `' F " { ( F ` X ) } ) e. P <-> E. x e. A ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) ) )
17	15 16	syl	|- ( ( F Fn A /\ A e. V /\ X e. A ) -> ( ( `' F " { ( F ` X ) } ) e. P <-> E. x e. A ( `' F " { ( F ` X ) } ) = ( `' F " { ( F ` x ) } ) ) )
18	10 17	mpbird	|- ( ( F Fn A /\ A e. V /\ X e. A ) -> ( `' F " { ( F ` X ) } ) e. P )