Metamath Proof Explorer

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 syl5ibr 
 |-  ( 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 ) ) ) )