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