Theorem fcoreslem1

Description: Lemma 1 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]$$
Assertion	fcoreslem1	$$⊢\phi \to P=F^{-1}\left[E\right]$$

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	1	ffund	$$⊢\phi \to \mathrm{Fun}F$$
5		cnvimainrn	$$⊢\mathrm{Fun}F\to F^{-1}\left[\mathrm{ran}F\cap C\right]=F^{-1}\left[C\right]$$
6	4 5	syl	$$⊢\phi \to F^{-1}\left[\mathrm{ran}F\cap C\right]=F^{-1}\left[C\right]$$
7	6	eqcomd	$$⊢\phi \to F^{-1}\left[C\right]=F^{-1}\left[\mathrm{ran}F\cap C\right]$$
8	2	imaeq2i	$$⊢F^{-1}\left[E\right]=F^{-1}\left[\mathrm{ran}F\cap C\right]$$
9	7 3 8	3eqtr4g	$$⊢\phi \to P=F^{-1}\left[E\right]$$