Metamath Proof Explorer

Theorem f1imadifssran

Description: Condition for the range of a one-to-one function to be the range of one its restrictions. Variant of imadifssran . (Contributed by AV, 4-Oct-2025)

Ref Expression
Assertion f1imadifssran 
|- ( Fun `' F -> ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) ) )

Proof

Step Hyp Ref Expression
1 imadmrn 
 |-  ( F " dom F ) = ran F
2 imadif 
 |-  ( Fun `' F -> ( F " ( dom F \ A ) ) = ( ( F " dom F ) \ ( F " A ) ) )
3 2 sseq1d 
 |-  ( Fun `' F -> ( ( F " ( dom F \ A ) ) C_ ( F " A ) <-> ( ( F " dom F ) \ ( F " A ) ) C_ ( F " A ) ) )
4 ssundif 
 |-  ( ( F " dom F ) C_ ( ( F " A ) u. ( F " A ) ) <-> ( ( F " dom F ) \ ( F " A ) ) C_ ( F " A ) )
5 unidm 
 |-  ( ( F " A ) u. ( F " A ) ) = ( F " A )
6 5 sseq2i 
 |-  ( ( F " dom F ) C_ ( ( F " A ) u. ( F " A ) ) <-> ( F " dom F ) C_ ( F " A ) )
7 id 
 |-  ( ( F " dom F ) C_ ( F " A ) -> ( F " dom F ) C_ ( F " A ) )
8 imassrn 
 |-  ( F " A ) C_ ran F
9 8 1 sseqtrri 
 |-  ( F " A ) C_ ( F " dom F )
10 9 a1i 
 |-  ( ( F " dom F ) C_ ( F " A ) -> ( F " A ) C_ ( F " dom F ) )
11 7 10 eqssd 
 |-  ( ( F " dom F ) C_ ( F " A ) -> ( F " dom F ) = ( F " A ) )
12 6 11 sylbi 
 |-  ( ( F " dom F ) C_ ( ( F " A ) u. ( F " A ) ) -> ( F " dom F ) = ( F " A ) )
13 4 12 sylbir 
 |-  ( ( ( F " dom F ) \ ( F " A ) ) C_ ( F " A ) -> ( F " dom F ) = ( F " A ) )
14 3 13 biimtrdi 
 |-  ( Fun `' F -> ( ( F " ( dom F \ A ) ) C_ ( F " A ) -> ( F " dom F ) = ( F " A ) ) )
15 14 imp 
 |-  ( ( Fun `' F /\ ( F " ( dom F \ A ) ) C_ ( F " A ) ) -> ( F " dom F ) = ( F " A ) )
16 1 15 eqtr3id 
 |-  ( ( Fun `' F /\ ( F " ( dom F \ A ) ) C_ ( F " A ) ) -> ran F = ( F " A ) )
17 16 ex 
 |-  ( Fun `' F -> ( ( F " ( dom F \ A ) ) C_ ( F " A ) -> ran F = ( F " A ) ) )
18 df-ima 
 |-  ( F " A ) = ran ( F |` A )
19 18 eqcomi 
 |-  ran ( F |` A ) = ( F " A )
20 19 sseq2i 
 |-  ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) <-> ( F " ( dom F \ A ) ) C_ ( F " A ) )
21 19 eqeq2i 
 |-  ( ran F = ran ( F |` A ) <-> ran F = ( F " A ) )
22 17 20 21 3imtr4g 
 |-  ( Fun `' F -> ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) ) )