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

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) = ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) )
2	1	sseq1i	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) ↔ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) )
3		ssun2	⊢ dom 𝐹 ⊆ ( 𝐴 ∪ dom 𝐹 )
4		undif2	⊢ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) = ( 𝐴 ∪ dom 𝐹 )
5	3 4	sseqtrri	⊢ dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) )
6		ssres2	⊢ ( dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) → ( 𝐹 ↾ dom 𝐹 ) ⊆ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) )
7	5 6	ax-mp	⊢ ( 𝐹 ↾ dom 𝐹 ) ⊆ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) )
8		resundi	⊢ ( 𝐹 ↾ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
9	7 8	sseqtri	⊢ ( 𝐹 ↾ dom 𝐹 ) ⊆ ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
10	9	rnssi	⊢ ran ( 𝐹 ↾ dom 𝐹 ) ⊆ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
11		rnun	⊢ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
12	10 11	sseqtri	⊢ ran ( 𝐹 ↾ dom 𝐹 ) ⊆ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) )
13	12	sseli	⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) → 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
14		elun	⊢ ( 𝑦 ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) ↔ ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
15	13 14	sylib	⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ dom 𝐹 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
16		inv1	⊢ ( dom 𝐹 ∩ V ) = dom 𝐹
17	16	ineqcomi	⊢ ( V ∩ dom 𝐹 ) = dom 𝐹
18	17	reseq2i	⊢ ( 𝐹 ↾ ( V ∩ dom 𝐹 ) ) = ( 𝐹 ↾ dom 𝐹 )
19		resindm	⊢ ( 𝐹 ↾ ( V ∩ dom 𝐹 ) ) = ( 𝐹 ↾ V )
20	18 19	eqtr3i	⊢ ( 𝐹 ↾ dom 𝐹 ) = ( 𝐹 ↾ V )
21	20	rneqi	⊢ ran ( 𝐹 ↾ dom 𝐹 ) = ran ( 𝐹 ↾ V )
22		rnresv	⊢ ran ( 𝐹 ↾ V ) = ran 𝐹
23	21 22	eqtr2i	⊢ ran 𝐹 = ran ( 𝐹 ↾ dom 𝐹 )
24	15 23	eleq2s	⊢ ( 𝑦 ∈ ran 𝐹 → ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) )
25		ssel	⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
26		pm2.27	⊢ ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
27	26	jao1i	⊢ ( ( 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ) → ( ( 𝑦 ∈ ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
28	24 25 27	syl2imc	⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 𝐹 ↾ 𝐴 ) ) )
29	28	ssrdv	⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 ⊆ ran ( 𝐹 ↾ 𝐴 ) )
30		rnresss	⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹
31	30	a1i	⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹 )
32	29 31	eqssd	⊢ ( ran ( 𝐹 ↾ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )
33	2 32	sylbi	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )