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 ⊆ 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 ssun2 ⊢ dom ⁡ F ⊆ A ∪ dom ⁡ F
4 undif2 ⊢ A ∪ dom ⁡ F ∖ A = A ∪ dom ⁡ F
5 3 4 sseqtrri ⊢ dom ⁡ F ⊆ A ∪ dom ⁡ F ∖ A
6 ssres2 ⊢ dom ⁡ F ⊆ A ∪ dom ⁡ F ∖ A → F ↾ dom ⁡ F ⊆ F ↾ A ∪ dom ⁡ F ∖ A
7 5 6 ax-mp ⊢ F ↾ dom ⁡ F ⊆ F ↾ A ∪ dom ⁡ F ∖ A
8 resundi ⊢ F ↾ A ∪ dom ⁡ F ∖ A = F ↾ A ∪ F ↾ dom ⁡ F ∖ A
9 7 8 sseqtri ⊢ F ↾ dom ⁡ F ⊆ F ↾ A ∪ F ↾ dom ⁡ F ∖ A
10 9 rnssi ⊢ ran ⁡ F ↾ dom ⁡ F ⊆ ran ⁡ F ↾ A ∪ F ↾ dom ⁡ F ∖ A
11 rnun ⊢ ran ⁡ F ↾ A ∪ F ↾ dom ⁡ F ∖ A = ran ⁡ F ↾ A ∪ ran ⁡ F ↾ dom ⁡ F ∖ A
12 10 11 sseqtri ⊢ ran ⁡ F ↾ dom ⁡ F ⊆ ran ⁡ F ↾ A ∪ ran ⁡ F ↾ dom ⁡ F ∖ A
13 12 sseli ⊢ y ∈ ran ⁡ F ↾ dom ⁡ F → y ∈ ran ⁡ F ↾ A ∪ ran ⁡ F ↾ dom ⁡ F ∖ A
14 elun ⊢ y ∈ ran ⁡ F ↾ A ∪ ran ⁡ F ↾ dom ⁡ F ∖ A ↔ y ∈ ran ⁡ F ↾ A ∨ y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A
15 13 14 sylib ⊢ y ∈ ran ⁡ F ↾ dom ⁡ F → y ∈ ran ⁡ F ↾ A ∨ y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A
16 inv1 ⊢ dom ⁡ F ∩ V = dom ⁡ F
17 16 ineqcomi ⊢ V ∩ dom ⁡ F = dom ⁡ F
18 17 reseq2i ⊢ F ↾ V ∩ dom ⁡ F = F ↾ dom ⁡ F
19 resindm ⊢ F ↾ V ∩ 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 ∈ ran ⁡ F → y ∈ ran ⁡ F ↾ A ∨ y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A
25 ssel ⊢ ran ⁡ F ↾ dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A → y ∈ ran ⁡ F ↾ A
26 pm2.27 ⊢ y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A → y ∈ ran ⁡ F ↾ dom ⁡ F ∖ A → y ∈ ran ⁡ F ↾ A → y ∈ ran ⁡ F ↾ A
27 26 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
28 24 25 27 syl2imc ⊢ ran ⁡ F ↾ dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → y ∈ ran ⁡ F → y ∈ ran ⁡ F ↾ A
29 28 ssrdv ⊢ ran ⁡ F ↾ dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → ran ⁡ F ⊆ ran ⁡ F ↾ A
30 rnresss ⊢ ran ⁡ F ↾ A ⊆ ran ⁡ F
31 30 a1i ⊢ ran ⁡ F ↾ dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → ran ⁡ F ↾ A ⊆ ran ⁡ F
32 29 31 eqssd ⊢ ran ⁡ F ↾ dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → ran ⁡ F = ran ⁡ F ↾ A
33 2 32 sylbi ⊢ F dom ⁡ F ∖ A ⊆ ran ⁡ F ↾ A → ran ⁡ F = ran ⁡ F ↾ A