Metamath Proof Explorer

Theorem imadifssran

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

Ref Expression
Assertion imadifssran 
|- ( ( Rel F /\ A C_ dom F ) -> ( ( 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 ssel 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) )
4 resdm 
 |-  ( Rel F -> ( F |` dom F ) = F )
5 4 eqcomd 
 |-  ( Rel F -> F = ( F |` dom F ) )
6 5 adantr 
 |-  ( ( Rel F /\ A C_ dom F ) -> F = ( F |` dom F ) )
7 6 rneqd 
 |-  ( ( Rel F /\ A C_ dom F ) -> ran F = ran ( F |` dom F ) )
8 7 eleq2d 
 |-  ( ( Rel F /\ A C_ dom F ) -> ( y e. ran F <-> y e. ran ( F |` dom F ) ) )
9 undif 
 |-  ( A C_ dom F <-> ( A u. ( dom F \ A ) ) = dom F )
10 9 biimpi 
 |-  ( A C_ dom F -> ( A u. ( dom F \ A ) ) = dom F )
11 10 eqcomd 
 |-  ( A C_ dom F -> dom F = ( A u. ( dom F \ A ) ) )
12 11 reseq2d 
 |-  ( A C_ dom F -> ( F |` dom F ) = ( F |` ( A u. ( dom F \ A ) ) ) )
13 resundi 
 |-  ( F |` ( A u. ( dom F \ A ) ) ) = ( ( F |` A ) u. ( F |` ( dom F \ A ) ) )
14 12 13 eqtrdi 
 |-  ( A C_ dom F -> ( F |` dom F ) = ( ( F |` A ) u. ( F |` ( dom F \ A ) ) ) )
15 14 rneqd 
 |-  ( A C_ dom F -> ran ( F |` dom F ) = ran ( ( F |` A ) u. ( F |` ( dom F \ A ) ) ) )
16 rnun 
 |-  ran ( ( F |` A ) u. ( F |` ( dom F \ A ) ) ) = ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) )
17 15 16 eqtrdi 
 |-  ( A C_ dom F -> ran ( F |` dom F ) = ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) ) )
18 17 eleq2d 
 |-  ( A C_ dom F -> ( y e. ran ( F |` dom F ) <-> y e. ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) ) ) )
19 elun 
 |-  ( y e. ( ran ( F |` A ) u. ran ( F |` ( dom F \ A ) ) ) <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) )
20 18 19 bitrdi 
 |-  ( A C_ dom F -> ( y e. ran ( F |` dom F ) <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) ) )
21 20 adantl 
 |-  ( ( Rel F /\ A C_ dom F ) -> ( y e. ran ( F |` dom F ) <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) ) )
22 8 21 bitrd 
 |-  ( ( Rel F /\ A C_ dom F ) -> ( y e. ran F <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) ) )
23 22 adantl 
 |-  ( ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) /\ ( Rel F /\ A C_ dom F ) ) -> ( y e. ran F <-> ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) ) )
24 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 ) ) )
25 24 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 ) ) )
26 25 com12 
 |-  ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) -> ( ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) -> y e. ran ( F |` A ) ) )
27 26 adantr 
 |-  ( ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) /\ ( Rel F /\ A C_ dom F ) ) -> ( ( y e. ran ( F |` A ) \/ y e. ran ( F |` ( dom F \ A ) ) ) -> y e. ran ( F |` A ) ) )
28 23 27 sylbid 
 |-  ( ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) /\ ( Rel F /\ A C_ dom F ) ) -> ( y e. ran F -> y e. ran ( F |` A ) ) )
29 28 ex 
 |-  ( ( y e. ran ( F |` ( dom F \ A ) ) -> y e. ran ( F |` A ) ) -> ( ( Rel F /\ A C_ dom F ) -> ( y e. ran F -> y e. ran ( F |` A ) ) ) )
30 3 29 syl 
 |-  ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ( ( Rel F /\ A C_ dom F ) -> ( y e. ran F -> y e. ran ( F |` A ) ) ) )
31 30 impcom 
 |-  ( ( ( Rel F /\ A C_ dom F ) /\ ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) ) -> ( y e. ran F -> y e. ran ( F |` A ) ) )
32 31 ssrdv 
 |-  ( ( ( Rel F /\ A C_ dom F ) /\ ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) ) -> ran F C_ ran ( F |` A ) )
33 rnresss 
 |-  ran ( F |` A ) C_ ran F
34 33 a1i 
 |-  ( ( ( Rel F /\ A C_ dom F ) /\ ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) ) -> ran ( F |` A ) C_ ran F )
35 32 34 eqssd 
 |-  ( ( ( Rel F /\ A C_ dom F ) /\ ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) ) -> ran F = ran ( F |` A ) )
36 35 ex 
 |-  ( ( Rel F /\ A C_ dom F ) -> ( ran ( F |` ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) ) )
37 2 36 biimtrid 
 |-  ( ( Rel F /\ A C_ dom F ) -> ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) ) )