Theorem f1imadifssran

Description: Condition for the range of a one-to-one function to be the range of one its restrictions. Variant of imadifssran . (Contributed by AV, 4-Oct-2025)

	Ref	Expression
Assertion	f1imadifssran	$$⊢\mathrm{Fun}{F}^{-1}\to \left(F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to \mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imadmrn	$$⊢F\left[\mathrm{dom}F\right]=\mathrm{ran}F$$
2		imadif	$$⊢\mathrm{Fun}{F}^{-1}\to F\left[\mathrm{dom}F\setminus A\right]=F\left[\mathrm{dom}F\right]\setminus F\left[A\right]$$
3	2	sseq1d	$$⊢\mathrm{Fun}{F}^{-1}\to \left(F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\leftrightarrow F\left[\mathrm{dom}F\right]\setminus F\left[A\right]\subseteq F\left[A\right]\right)$$
4		ssundif	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\cup F\left[A\right]\leftrightarrow F\left[\mathrm{dom}F\right]\setminus F\left[A\right]\subseteq F\left[A\right]$$
5		unidm	$$⊢F\left[A\right]\cup F\left[A\right]=F\left[A\right]$$
6	5	sseq2i	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\cup F\left[A\right]\leftrightarrow F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]$$
7		id	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\to F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]$$
8		imassrn	$$⊢F\left[A\right]\subseteq \mathrm{ran}F$$
9	8 1	sseqtrri	$$⊢F\left[A\right]\subseteq F\left[\mathrm{dom}F\right]$$
10	9	a1i	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\to F\left[A\right]\subseteq F\left[\mathrm{dom}F\right]$$
11	7 10	eqssd	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\to F\left[\mathrm{dom}F\right]=F\left[A\right]$$
12	6 11	sylbi	$$⊢F\left[\mathrm{dom}F\right]\subseteq F\left[A\right]\cup F\left[A\right]\to F\left[\mathrm{dom}F\right]=F\left[A\right]$$
13	4 12	sylbir	$$⊢F\left[\mathrm{dom}F\right]\setminus F\left[A\right]\subseteq F\left[A\right]\to F\left[\mathrm{dom}F\right]=F\left[A\right]$$
14	3 13	biimtrdi	$$⊢\mathrm{Fun}{F}^{-1}\to \left(F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\to F\left[\mathrm{dom}F\right]=F\left[A\right]\right)$$
15	14	imp	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\right)\to F\left[\mathrm{dom}F\right]=F\left[A\right]$$
16	1 15	eqtr3id	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\right)\to \mathrm{ran}F=F\left[A\right]$$
17	16	ex	$$⊢\mathrm{Fun}{F}^{-1}\to \left(F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\to \mathrm{ran}F=F\left[A\right]\right)$$
18		df-ima	$$⊢F\left[A\right]=\mathrm{ran}\left({F\upharpoonright }_A\right)$$
19	18	eqcomi	$$⊢\mathrm{ran}\left({F\upharpoonright }_A\right)=F\left[A\right]$$
20	19	sseq2i	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\leftrightarrow F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]$$
21	19	eqeq2i	$$⊢\mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_A\right)\leftrightarrow \mathrm{ran}F=F\left[A\right]$$
22	17 20 21	3imtr4g	$$⊢\mathrm{Fun}{F}^{-1}\to \left(F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to \mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_A\right)\right)$$