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 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) = ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) )
2 1 sseq1i ⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ↔ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) )
3 ssel ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
4 resdm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
5 4 eqcomd ⊢ ( Rel 𝐹 → 𝐹 = ( 𝐹 ↾ dom 𝐹 ) )
6 5 adantr ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → 𝐹 = ( 𝐹 ↾ dom 𝐹 ) )
7 6 rneqd ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ran 𝐹 = ran ( 𝐹 ↾ dom 𝐹 ) )
8 7 eleq2d ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) ) )
9 undif ⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) = dom 𝐹 )
10 9 biimpi ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) = dom 𝐹 )
11 10 eqcomd ⊢ ( 𝐴 ⊆ dom 𝐹 → dom 𝐹 = ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) )
12 11 reseq2d ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) )
13 resundi ⊢ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
14 12 13 eqtrdi ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
15 14 rneqd ⊢ ( 𝐴 ⊆ dom 𝐹 → ran ( 𝐹 ↾ dom 𝐹 ) = ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
16 rnun ⊢ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
17 15 16 eqtrdi ⊢ ( 𝐴 ⊆ dom 𝐹 → ran ( 𝐹 ↾ dom 𝐹 ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
18 17 eleq2d ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) ↔ 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ) )
19 elun ⊢ ( 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
20 18 19 bitrdi ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ) )
21 20 adantl ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ) )
22 8 21 bitrd ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑦 ∈ ran 𝐹 ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ) )
23 22 adantl ⊢ ( ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ) → ( 𝑦 ∈ ran 𝐹 ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ) )
24 pm2.27 ⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
25 24 jao1i ⊢ ( ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
26 25 com12 ⊢ ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
27 26 adantr ⊢ ( ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
28 23 27 sylbid ⊢ ( ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
29 28 ex ⊢ ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) ) )
30 3 29 syl ⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) ) )
31 30 impcom ⊢ ( ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
32 31 ssrdv ⊢ ( ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ) → ran 𝐹 ⊆ ran ( 𝐹 ↾ 𝐴 ) )
33 rnresss ⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹
34 33 a1i ⊢ ( ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹 )
35 32 34 eqssd ⊢ ( ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )
36 35 ex ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ) )
37 2 36 biimtrid ⊢ ( ( Rel 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) ) )