Metamath Proof Explorer

Theorem imaelsetpreimafv

Description: The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024)

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

Proof

Step Hyp Ref Expression
1 setpreimafvex.p 
 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2 1 fvelsetpreimafv 
 |-  ( ( F Fn A /\ S e. P ) -> E. x e. S S = ( `' F " { ( F ` x ) } ) )
3 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
4 3 sneqd 
 |-  ( y = x -> { ( F ` y ) } = { ( F ` x ) } )
5 4 imaeq2d 
 |-  ( y = x -> ( `' F " { ( F ` y ) } ) = ( `' F " { ( F ` x ) } ) )
6 5 eqeq2d 
 |-  ( y = x -> ( S = ( `' F " { ( F ` y ) } ) <-> S = ( `' F " { ( F ` x ) } ) ) )
7 6 cbvrexvw 
 |-  ( E. y e. S S = ( `' F " { ( F ` y ) } ) <-> E. x e. S S = ( `' F " { ( F ` x ) } ) )
8 2 7 sylibr 
 |-  ( ( F Fn A /\ S e. P ) -> E. y e. S S = ( `' F " { ( F ` y ) } ) )
9 8 3adant3 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> E. y e. S S = ( `' F " { ( F ` y ) } ) )
10 imaeq2 
 |-  ( S = ( `' F " { ( F ` y ) } ) -> ( F " S ) = ( F " ( `' F " { ( F ` y ) } ) ) )
11 10 3ad2ant3 
 |-  ( ( ( F Fn A /\ S e. P /\ X e. S ) /\ y e. S /\ S = ( `' F " { ( F ` y ) } ) ) -> ( F " S ) = ( F " ( `' F " { ( F ` y ) } ) ) )
12 fnfun 
 |-  ( F Fn A -> Fun F )
13 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " { ( F ` y ) } ) ) = ( { ( F ` y ) } i^i ran F ) )
14 12 13 syl 
 |-  ( F Fn A -> ( F " ( `' F " { ( F ` y ) } ) ) = ( { ( F ` y ) } i^i ran F ) )
15 14 3ad2ant1 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( F " ( `' F " { ( F ` y ) } ) ) = ( { ( F ` y ) } i^i ran F ) )
16 15 3ad2ant1 
 |-  ( ( ( F Fn A /\ S e. P /\ X e. S ) /\ y e. S /\ S = ( `' F " { ( F ` y ) } ) ) -> ( F " ( `' F " { ( F ` y ) } ) ) = ( { ( F ` y ) } i^i ran F ) )
17 1 elsetpreimafvbi 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( y e. S <-> ( y e. A /\ ( F ` y ) = ( F ` X ) ) ) )
18 fnfvelrn 
 |-  ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. ran F )
19 18 snssd 
 |-  ( ( F Fn A /\ y e. A ) -> { ( F ` y ) } C_ ran F )
20 df-ss 
 |-  ( { ( F ` y ) } C_ ran F <-> ( { ( F ` y ) } i^i ran F ) = { ( F ` y ) } )
21 19 20 sylib 
 |-  ( ( F Fn A /\ y e. A ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` y ) } )
22 21 3adant3 
 |-  ( ( F Fn A /\ y e. A /\ ( F ` y ) = ( F ` X ) ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` y ) } )
23 simp3 
 |-  ( ( F Fn A /\ y e. A /\ ( F ` y ) = ( F ` X ) ) -> ( F ` y ) = ( F ` X ) )
24 23 sneqd 
 |-  ( ( F Fn A /\ y e. A /\ ( F ` y ) = ( F ` X ) ) -> { ( F ` y ) } = { ( F ` X ) } )
25 22 24 eqtrd 
 |-  ( ( F Fn A /\ y e. A /\ ( F ` y ) = ( F ` X ) ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } )
26 25 3expib 
 |-  ( F Fn A -> ( ( y e. A /\ ( F ` y ) = ( F ` X ) ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } ) )
27 26 3ad2ant1 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( ( y e. A /\ ( F ` y ) = ( F ` X ) ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } ) )
28 17 27 sylbid 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( y e. S -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } ) )
29 28 imp 
 |-  ( ( ( F Fn A /\ S e. P /\ X e. S ) /\ y e. S ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } )
30 29 3adant3 
 |-  ( ( ( F Fn A /\ S e. P /\ X e. S ) /\ y e. S /\ S = ( `' F " { ( F ` y ) } ) ) -> ( { ( F ` y ) } i^i ran F ) = { ( F ` X ) } )
31 11 16 30 3eqtrd 
 |-  ( ( ( F Fn A /\ S e. P /\ X e. S ) /\ y e. S /\ S = ( `' F " { ( F ` y ) } ) ) -> ( F " S ) = { ( F ` X ) } )
32 31 rexlimdv3a 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( E. y e. S S = ( `' F " { ( F ` y ) } ) -> ( F " S ) = { ( F ` X ) } ) )
33 9 32 mpd 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( F " S ) = { ( F ` X ) } )