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