Theorem fcoreslem3

Description: Lemma 3 for fcores . (Contributed by AV, 13-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	fcoreslem3	$$⊢\phi \to X:P\underset{onto}{⟶}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	1	ffnd	$$⊢\phi \to FFnA$$
6	2	a1i	$$⊢\phi \to E=\mathrm{ran}F\cap C$$
7	3	a1i	$$⊢\phi \to P=F^{-1}\left[C\right]$$
8	5 6 7	rescnvimafod	$$⊢\phi \to \left({F\upharpoonright }_P\right):P\underset{onto}{⟶}E$$
9		foeq1	$$⊢X={F\upharpoonright }_P\to \left(X:P\underset{onto}{⟶}E\leftrightarrow \left({F\upharpoonright }_P\right):P\underset{onto}{⟶}E\right)$$
10	4 9	mp1i	$$⊢\phi \to \left(X:P\underset{onto}{⟶}E\leftrightarrow \left({F\upharpoonright }_P\right):P\underset{onto}{⟶}E\right)$$
11	8 10	mpbird	$$⊢\phi \to X:P\underset{onto}{⟶}E$$