Metamath Proof Explorer

Theorem imadifssran

Description: Condition for the range of a class to be the range of one of its restrictions. (Contributed by AV, 4-Oct-2025) Remove antecedent. (Revised by Eric Schmidt, 10-Jul-2026)

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

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " ( dom F \ A ) ) = ran ( F |` ( dom F \ A ) )
2 1 sseq1i 
 |-  ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) <-> ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) )
3 ssun2 
 |-  dom F C_ ( A u. dom F )
4 undif2 
 |-  ( A u. ( dom F \ A ) ) = ( A u. dom F )
5 3 4 sseqtrri 
 |-  dom F C_ ( A u. ( dom F \ A ) )
6 ssres2 
 |-  ( dom F C_ ( A u. ( dom F \ A ) ) -> ( F |` dom F ) C_ ( F |` ( A u. ( dom F \ A ) ) ) )
7 5 6 ax-mp 
 |-  ( F |` dom F ) C_ ( F |` ( A u. ( dom F \ A ) ) )
8 resundi 
 |-  ( F |` ( A u. ( dom F \ A ) ) ) = ( ( F |` A ) u. ( F |` ( dom F \ A ) ) )
9 7 8 sseqtri 
 |-  ( F |` dom F ) C_ ( ( F |` A ) u. ( F |` ( dom F \ A ) ) )
10 9 rnssi 
 |-  ran ( F |` dom F ) C_ ran ( ( F |` A ) u. ( F |` ( dom F \ A ) ) )
11 rnun 
 |-  ran ( ( F |` A ) u. ( F |` ( dom F \ A ) ) ) = ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) )
12 10 11 sseqtri 
 |-  ran ( F |` dom F ) C_ ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) )
13 12 sseli 
 |-  ( y e. ran ( F |` dom F ) -> y e. ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) ) )
14 elun 
 |-  ( y e. ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) ) <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) )
15 13 14 sylib 
 |-  ( y e. ran ( F |` dom F ) -> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) )
16 inv1 
 |-  ( dom F i^i _V ) = dom F
17 16 ineqcomi 
 |-  ( _V i^i dom F ) = dom F
18 17 reseq2i 
 |-  ( F |` ( _V i^i dom F ) ) = ( F |` dom F )
19 resindm 
 |-  ( F |` ( _V i^i dom F ) ) = ( F |` _V )
20 18 19 eqtr3i 
 |-  ( F |` dom F ) = ( F |` _V )
21 20 rneqi 
 |-  ran ( F |` dom F ) = ran ( F |` _V )
22 rnresv 
 |-  ran ( F |` _V ) = ran F
23 21 22 eqtr2i 
 |-  ran F = ran ( F |` dom F )
24 15 23 eleq2s 
 |-  ( y e. ran F -> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) )
25 ssel 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) )
26 pm2.27 
 |-  ( y e. ran ( F |` ( dom F \ A ) ) -> ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) -> y e. ran ( F |` A ) ) )
27 26 jao1i 
 |-  ( ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) -> ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) -> y e. ran ( F |` A ) ) )
28 24 25 27 syl2imc 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ( y e. ran F -> y e. ran ( F |` A ) ) )
29 28 ssrdv 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F C_ ran ( F |` A ) )
30 rnresss 
 |-  ran ( F |` A ) C_ ran F
31 30 a1i 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ran ( F |` A ) C_ ran F )
32 29 31 eqssd 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) )
33 2 32 sylbi 
 |-  ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) )