Theorem elsetpreimafvbi

Description: An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		fniniseg	|- ( F Fn A -> ( X e. ( `' F " { ( F ` x ) } ) <-> ( X e. A /\ ( F ` X ) = ( F ` x ) ) ) )
3		fniniseg	|- ( F Fn A -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` x ) ) ) )
4		eqeq2	|- ( ( F ` x ) = ( F ` X ) -> ( ( F ` Y ) = ( F ` x ) <-> ( F ` Y ) = ( F ` X ) ) )
5	4	anbi2d	|- ( ( F ` x ) = ( F ` X ) -> ( ( Y e. A /\ ( F ` Y ) = ( F ` x ) ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )
6	5	eqcoms	|- ( ( F ` X ) = ( F ` x ) -> ( ( Y e. A /\ ( F ` Y ) = ( F ` x ) ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )
7	3 6	sylan9bb	|- ( ( F Fn A /\ ( F ` X ) = ( F ` x ) ) -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )
8	7	ex	|- ( F Fn A -> ( ( F ` X ) = ( F ` x ) -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) )
9	8	adantld	|- ( F Fn A -> ( ( X e. A /\ ( F ` X ) = ( F ` x ) ) -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) )
10	2 9	sylbid	|- ( F Fn A -> ( X e. ( `' F " { ( F ` x ) } ) -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) )
11		eleq2	|- ( S = ( `' F " { ( F ` x ) } ) -> ( X e. S <-> X e. ( `' F " { ( F ` x ) } ) ) )
12		eleq2	|- ( S = ( `' F " { ( F ` x ) } ) -> ( Y e. S <-> Y e. ( `' F " { ( F ` x ) } ) ) )
13	12	bibi1d	|- ( S = ( `' F " { ( F ` x ) } ) -> ( ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) <-> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) )
14	11 13	imbi12d	|- ( S = ( `' F " { ( F ` x ) } ) -> ( ( X e. S -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) <-> ( X e. ( `' F " { ( F ` x ) } ) -> ( Y e. ( `' F " { ( F ` x ) } ) <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) ) )
15	10 14	imbitrrid	|- ( S = ( `' F " { ( F ` x ) } ) -> ( F Fn A -> ( X e. S -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) ) )
16	15	rexlimivw	|- ( E. x e. A S = ( `' F " { ( F ` x ) } ) -> ( F Fn A -> ( X e. S -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) ) )
17	1	elsetpreimafv	|- ( S e. P -> E. x e. A S = ( `' F " { ( F ` x ) } ) )
18	16 17	syl11	|- ( F Fn A -> ( S e. P -> ( X e. S -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) ) ) )
19	18	3imp	|- ( ( F Fn A /\ S e. P /\ X e. S ) -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )