Theorem fundcmpsurinjimaid

Description: Every function F : A --> B can be decomposed into a surjective function onto the image ( F " A ) of the domain of F and an injective function from the image ( F " A ) . (Contributed by AV, 17-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinjimaid.i	$$⊢I=F\left[A\right]$$
	fundcmpsurinjimaid.g	$$⊢G=\left(x\in A⟼F\left(x\right)\right)$$
	fundcmpsurinjimaid.h	$$⊢H={\mathrm{I}\upharpoonright }_I$$
Assertion	fundcmpsurinjimaid	$$⊢F:A⟶B\to \left(G:A\underset{onto}{⟶}I\wedge H:I\underset{1-1}{⟶}B\wedge F=H\circ G\right)$$

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinjimaid.i	$$⊢I=F\left[A\right]$$
2		fundcmpsurinjimaid.g	$$⊢G=\left(x\in A⟼F\left(x\right)\right)$$
3		fundcmpsurinjimaid.h	$$⊢H={\mathrm{I}\upharpoonright }_I$$
4		fimadmfo	$$⊢F:A⟶B\to F:A\underset{onto}{⟶}F\left[A\right]$$
5		ffn	$$⊢F:A⟶B\to FFnA$$
6		dffn5	$$⊢FFnA\leftrightarrow F=\left(x\in A⟼F\left(x\right)\right)$$
7	5 6	sylib	$$⊢F:A⟶B\to F=\left(x\in A⟼F\left(x\right)\right)$$
8	7	eqcomd	$$⊢F:A⟶B\to \left(x\in A⟼F\left(x\right)\right)=F$$
9	2 8	syl5eq	$$⊢F:A⟶B\to G=F$$
10		eqidd	$$⊢F:A⟶B\to A=A$$
11	1	a1i	$$⊢F:A⟶B\to I=F\left[A\right]$$
12	9 10 11	foeq123d	$$⊢F:A⟶B\to \left(G:A\underset{onto}{⟶}I\leftrightarrow F:A\underset{onto}{⟶}F\left[A\right]\right)$$
13	4 12	mpbird	$$⊢F:A⟶B\to G:A\underset{onto}{⟶}I$$
14		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1\; onto}{⟶}I$$
15		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1\; onto}{⟶}I\to \left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I$$
16		f1eq1	$$⊢H={\mathrm{I}\upharpoonright }_I\to \left(H:I\underset{1-1}{⟶}I\leftrightarrow \left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I\right)$$
17	3 16	ax-mp	$$⊢H:I\underset{1-1}{⟶}I\leftrightarrow \left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I$$
18	17	biimpri	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I\to H:I\underset{1-1}{⟶}I$$
19		fimass	$$⊢F:A⟶B\to F\left[A\right]\subseteq B$$
20	1 19	eqsstrid	$$⊢F:A⟶B\to I\subseteq B$$
21		f1ss	$$⊢\left(H:I\underset{1-1}{⟶}I\wedge I\subseteq B\right)\to H:I\underset{1-1}{⟶}B$$
22	18 20 21	syl2an	$$⊢\left(\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I\wedge F:A⟶B\right)\to H:I\underset{1-1}{⟶}B$$
23	22	ex	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1}{⟶}I\to \left(F:A⟶B\to H:I\underset{1-1}{⟶}B\right)$$
24	14 15 23	mp2b	$$⊢F:A⟶B\to H:I\underset{1-1}{⟶}B$$
25	3	fveq1i	$$⊢H\left(F\left(x\right)\right)=\left({\mathrm{I}\upharpoonright }_I\right)\left(F\left(x\right)\right)$$
26	5	adantr	$$⊢\left(F:A⟶B\wedge x\in A\right)\to FFnA$$
27		simpr	$$⊢\left(F:A⟶B\wedge x\in A\right)\to x\in A$$
28	26 27 27	fnfvimad	$$⊢\left(F:A⟶B\wedge x\in A\right)\to F\left(x\right)\in F\left[A\right]$$
29	28 1	eleqtrrdi	$$⊢\left(F:A⟶B\wedge x\in A\right)\to F\left(x\right)\in I$$
30		fvresi	$$⊢F\left(x\right)\in I\to \left({\mathrm{I}\upharpoonright }_I\right)\left(F\left(x\right)\right)=F\left(x\right)$$
31	29 30	syl	$$⊢\left(F:A⟶B\wedge x\in A\right)\to \left({\mathrm{I}\upharpoonright }_I\right)\left(F\left(x\right)\right)=F\left(x\right)$$
32	25 31	syl5eq	$$⊢\left(F:A⟶B\wedge x\in A\right)\to H\left(F\left(x\right)\right)=F\left(x\right)$$
33	32	mpteq2dva	$$⊢F:A⟶B\to \left(x\in A⟼H\left(F\left(x\right)\right)\right)=\left(x\in A⟼F\left(x\right)\right)$$
34	2	coeq2i	$$⊢H\circ G=H\circ \left(x\in A⟼F\left(x\right)\right)$$
35		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I\underset{1-1\; onto}{⟶}I\to \left({\mathrm{I}\upharpoonright }_I\right):I⟶I$$
36	14 35	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_I\right):I⟶I$$
37	3	feq1i	$$⊢H:I⟶I\leftrightarrow \left({\mathrm{I}\upharpoonright }_I\right):I⟶I$$
38	36 37	mpbir	$$⊢H:I⟶I$$
39	38	a1i	$$⊢F:A⟶B\to H:I⟶I$$
40	39 29	cofmpt	$$⊢F:A⟶B\to H\circ \left(x\in A⟼F\left(x\right)\right)=\left(x\in A⟼H\left(F\left(x\right)\right)\right)$$
41	34 40	syl5eq	$$⊢F:A⟶B\to H\circ G=\left(x\in A⟼H\left(F\left(x\right)\right)\right)$$
42	33 41 7	3eqtr4rd	$$⊢F:A⟶B\to F=H\circ G$$
43	13 24 42	3jca	$$⊢F:A⟶B\to \left(G:A\underset{onto}{⟶}I\wedge H:I\underset{1-1}{⟶}B\wedge F=H\circ G\right)$$