Theorem fcoreslem2

Description: Lemma 2 for fcores . (Contributed by AV, 17-Sep-2024)

	Ref	Expression
Hypotheses	fcores.f	$$⊢\phi \to F:A⟶B$$
	fcores.e	$$⊢E=\mathrm{ran}F\cap C$$
	fcores.p	$$⊢P=F^{-1}\left[C\right]$$
	fcores.x	$$⊢X={F\upharpoonright }_P$$
Assertion	fcoreslem2	$$⊢\phi \to \mathrm{ran}X=E$$

Proof

Step	Hyp	Ref	Expression
1		fcores.f	$$⊢\phi \to F:A⟶B$$
2		fcores.e	$$⊢E=\mathrm{ran}F\cap C$$
3		fcores.p	$$⊢P=F^{-1}\left[C\right]$$
4		fcores.x	$$⊢X={F\upharpoonright }_P$$
5		df-ima	$$⊢F\left[P\right]=\mathrm{ran}\left({F\upharpoonright }_P\right)$$
6	4	rneqi	$$⊢\mathrm{ran}X=\mathrm{ran}\left({F\upharpoonright }_P\right)$$
7	6	eqcomi	$$⊢\mathrm{ran}\left({F\upharpoonright }_P\right)=\mathrm{ran}X$$
8	7	a1i	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_P\right)=\mathrm{ran}X$$
9	5 8	eqtr2id	$$⊢\phi \to \mathrm{ran}X=F\left[P\right]$$
10	1 2 3	fcoreslem1	$$⊢\phi \to P=F^{-1}\left[E\right]$$
11	10	imaeq2d	$$⊢\phi \to F\left[P\right]=F\left[F^{-1}\left[E\right]\right]$$
12	1	ffund	$$⊢\phi \to \mathrm{Fun}F$$
13		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[E\right]\right]=E\cap \mathrm{ran}F$$
14	12 13	syl	$$⊢\phi \to F\left[F^{-1}\left[E\right]\right]=E\cap \mathrm{ran}F$$
15		inss1	$$⊢\mathrm{ran}F\cap C\subseteq \mathrm{ran}F$$
16	2 15	eqsstri	$$⊢E\subseteq \mathrm{ran}F$$
17	16	a1i	$$⊢\phi \to E\subseteq \mathrm{ran}F$$
18		dfss2	$$⊢E\subseteq \mathrm{ran}F\leftrightarrow E\cap \mathrm{ran}F=E$$
19	17 18	sylib	$$⊢\phi \to E\cap \mathrm{ran}F=E$$
20	14 19	eqtrd	$$⊢\phi \to F\left[F^{-1}\left[E\right]\right]=E$$
21	9 11 20	3eqtrd	$$⊢\phi \to \mathrm{ran}X=E$$