This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rescnvimafod

Description: The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024) (Revised by AV, 29-Sep-2024)

Ref Expression
Hypotheses rescnvimafod.f 
|- ( ph -> F Fn A )
rescnvimafod.e 
|- ( ph -> E = ( ran F i^i B ) )
rescnvimafod.d 
|- ( ph -> D = ( `' F " B ) )
Assertion rescnvimafod 
|- ( ph -> ( F |` D ) : D -onto-> E )

Proof

Step Hyp Ref Expression
1 rescnvimafod.f 
 |-  ( ph -> F Fn A )
2 rescnvimafod.e 
 |-  ( ph -> E = ( ran F i^i B ) )
3 rescnvimafod.d 
 |-  ( ph -> D = ( `' F " B ) )
4 cnvimass 
 |-  ( `' F " B ) C_ dom F
5 4 a1i 
 |-  ( ph -> ( `' F " B ) C_ dom F )
6 1 fndmd 
 |-  ( ph -> dom F = A )
7 6 eqcomd 
 |-  ( ph -> A = dom F )
8 5 3 7 3sstr4d 
 |-  ( ph -> D C_ A )
9 1 8 fnssresd 
 |-  ( ph -> ( F |` D ) Fn D )
10 df-ima 
 |-  ( F " D ) = ran ( F |` D )
11 3 imaeq2d 
 |-  ( ph -> ( F " D ) = ( F " ( `' F " B ) ) )
12 fnfun 
 |-  ( F Fn A -> Fun F )
13 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " B ) ) = ( B i^i ran F ) )
14 1 12 13 3syl 
 |-  ( ph -> ( F " ( `' F " B ) ) = ( B i^i ran F ) )
15 incom 
 |-  ( B i^i ran F ) = ( ran F i^i B )
16 15 a1i 
 |-  ( ph -> ( B i^i ran F ) = ( ran F i^i B ) )
17 11 14 16 3eqtrd 
 |-  ( ph -> ( F " D ) = ( ran F i^i B ) )
18 10 17 eqtr3id 
 |-  ( ph -> ran ( F |` D ) = ( ran F i^i B ) )
19 18 2 eqtr4d 
 |-  ( ph -> ran ( F |` D ) = E )
20 df-fo 
 |-  ( ( F |` D ) : D -onto-> E <-> ( ( F |` D ) Fn D /\ ran ( F |` D ) = E ) )
21 9 19 20 sylanbrc 
 |-  ( ph -> ( F |` D ) : D -onto-> E )