Metamath Proof Explorer

Theorem ressupprn

Description: The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion ressupprn 
|- ( ( Fun F /\ F e. V /\ .0. e. W ) -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 1 biimpi 
 |-  ( Fun F -> F Fn dom F )
3 2 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> F Fn dom F )
4 dmexg 
 |-  ( F e. V -> dom F e. _V )
5 4 3ad2ant2 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> dom F e. _V )
6 simp3 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> .0. e. W )
7 elsuppfn 
 |-  ( ( F Fn dom F /\ dom F e. _V /\ .0. e. W ) -> ( x e. ( F supp .0. ) <-> ( x e. dom F /\ ( F ` x ) =/= .0. ) ) )
8 3 5 6 7 syl3anc 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( x e. ( F supp .0. ) <-> ( x e. dom F /\ ( F ` x ) =/= .0. ) ) )
9 8 anbi1d 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( ( x e. ( F supp .0. ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( ( x e. dom F /\ ( F ` x ) =/= .0. ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) ) )
10 anass 
 |-  ( ( ( x e. dom F /\ ( F ` x ) =/= .0. ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( x e. dom F /\ ( ( F ` x ) =/= .0. /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) ) )
11 10 a1i 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( ( ( x e. dom F /\ ( F ` x ) =/= .0. ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( x e. dom F /\ ( ( F ` x ) =/= .0. /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) ) ) )
12 8 biimprd 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( ( x e. dom F /\ ( F ` x ) =/= .0. ) -> x e. ( F supp .0. ) ) )
13 12 impl 
 |-  ( ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) /\ ( F ` x ) =/= .0. ) -> x e. ( F supp .0. ) )
14 13 fvresd 
 |-  ( ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) /\ ( F ` x ) =/= .0. ) -> ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) )
15 14 eqeq1d 
 |-  ( ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) /\ ( F ` x ) =/= .0. ) -> ( ( ( F |` ( F supp .0. ) ) ` x ) = y <-> ( F ` x ) = y ) )
16 15 pm5.32da 
 |-  ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) -> ( ( ( F ` x ) =/= .0. /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( ( F ` x ) =/= .0. /\ ( F ` x ) = y ) ) )
17 ancom 
 |-  ( ( ( F ` x ) =/= .0. /\ ( F ` x ) = y ) <-> ( ( F ` x ) = y /\ ( F ` x ) =/= .0. ) )
18 simpr 
 |-  ( ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) /\ ( F ` x ) = y ) -> ( F ` x ) = y )
19 18 neeq1d 
 |-  ( ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) /\ ( F ` x ) = y ) -> ( ( F ` x ) =/= .0. <-> y =/= .0. ) )
20 19 pm5.32da 
 |-  ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) -> ( ( ( F ` x ) = y /\ ( F ` x ) =/= .0. ) <-> ( ( F ` x ) = y /\ y =/= .0. ) ) )
21 17 20 bitrid 
 |-  ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) -> ( ( ( F ` x ) =/= .0. /\ ( F ` x ) = y ) <-> ( ( F ` x ) = y /\ y =/= .0. ) ) )
22 16 21 bitrd 
 |-  ( ( ( Fun F /\ F e. V /\ .0. e. W ) /\ x e. dom F ) -> ( ( ( F ` x ) =/= .0. /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( ( F ` x ) = y /\ y =/= .0. ) ) )
23 22 pm5.32da 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( ( x e. dom F /\ ( ( F ` x ) =/= .0. /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) ) <-> ( x e. dom F /\ ( ( F ` x ) = y /\ y =/= .0. ) ) ) )
24 9 11 23 3bitrd 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( ( x e. ( F supp .0. ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = y ) <-> ( x e. dom F /\ ( ( F ` x ) = y /\ y =/= .0. ) ) ) )
25 24 rexbidv2 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( E. x e. ( F supp .0. ) ( ( F |` ( F supp .0. ) ) ` x ) = y <-> E. x e. dom F ( ( F ` x ) = y /\ y =/= .0. ) ) )
26 suppssdm 
 |-  ( F supp .0. ) C_ dom F
27 fnssres 
 |-  ( ( F Fn dom F /\ ( F supp .0. ) C_ dom F ) -> ( F |` ( F supp .0. ) ) Fn ( F supp .0. ) )
28 3 26 27 sylancl 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( F |` ( F supp .0. ) ) Fn ( F supp .0. ) )
29 fvelrnb 
 |-  ( ( F |` ( F supp .0. ) ) Fn ( F supp .0. ) -> ( y e. ran ( F |` ( F supp .0. ) ) <-> E. x e. ( F supp .0. ) ( ( F |` ( F supp .0. ) ) ` x ) = y ) )
30 28 29 syl 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( y e. ran ( F |` ( F supp .0. ) ) <-> E. x e. ( F supp .0. ) ( ( F |` ( F supp .0. ) ) ` x ) = y ) )
31 fvelrnb 
 |-  ( F Fn dom F -> ( y e. ran F <-> E. x e. dom F ( F ` x ) = y ) )
32 31 anbi1d 
 |-  ( F Fn dom F -> ( ( y e. ran F /\ y =/= .0. ) <-> ( E. x e. dom F ( F ` x ) = y /\ y =/= .0. ) ) )
33 eldifsn 
 |-  ( y e. ( ran F \ { .0. } ) <-> ( y e. ran F /\ y =/= .0. ) )
34 r19.41v 
 |-  ( E. x e. dom F ( ( F ` x ) = y /\ y =/= .0. ) <-> ( E. x e. dom F ( F ` x ) = y /\ y =/= .0. ) )
35 32 33 34 3bitr4g 
 |-  ( F Fn dom F -> ( y e. ( ran F \ { .0. } ) <-> E. x e. dom F ( ( F ` x ) = y /\ y =/= .0. ) ) )
36 3 35 syl 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( y e. ( ran F \ { .0. } ) <-> E. x e. dom F ( ( F ` x ) = y /\ y =/= .0. ) ) )
37 25 30 36 3bitr4d 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ( y e. ran ( F |` ( F supp .0. ) ) <-> y e. ( ran F \ { .0. } ) ) )
38 37 eqrdv 
 |-  ( ( Fun F /\ F e. V /\ .0. e. W ) -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )