Theorem fundcmpsurinj

Description: Every function F : A --> B can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024)

	Ref	Expression
Assertion	fundcmpsurinj	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \exists g\exists h\exists p\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)$$

Proof

Step	Hyp	Ref	Expression
1		abrexexg	$$⊢A\in V\to \left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\in \mathrm{V}$$
2	1	adantl	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\in \mathrm{V}$$
3		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
4	3	sneqd	$$⊢x=y\to \left\{F\left(x\right)\right\}=\left\{F\left(y\right)\right\}$$
5	4	imaeq2d	$$⊢x=y\to F^{-1}\left[\left\{F\left(x\right)\right\}\right]=F^{-1}\left[\left\{F\left(y\right)\right\}\right]$$
6	5	eqeq2d	$$⊢x=y\to \left(z=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow z=F^{-1}\left[\left\{F\left(y\right)\right\}\right]\right)$$
7	6	cbvrexvw	$$⊢\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow \exists y\in Az=F^{-1}\left[\left\{F\left(y\right)\right\}\right]$$
8	7	abbii	$$⊢\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}=\left\{z|\exists y\in Az=F^{-1}\left[\left\{F\left(y\right)\right\}\right]\right\}$$
9	8	fundcmpsurinjpreimafv	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \exists g\exists h\left(g:A\underset{onto}{⟶}\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\wedge h:\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\underset{1-1}{⟶}B\wedge F=h\circ g\right)$$
10		foeq3	$$⊢p=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\to \left(g:A\underset{onto}{⟶}p\leftrightarrow g:A\underset{onto}{⟶}\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\right)$$
11		f1eq2	$$⊢p=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\to \left(h:p\underset{1-1}{⟶}B\leftrightarrow h:\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\underset{1-1}{⟶}B\right)$$
12	10 11	3anbi12d	$$⊢p=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\to \left(\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)\leftrightarrow \left(g:A\underset{onto}{⟶}\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\wedge h:\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\underset{1-1}{⟶}B\wedge F=h\circ g\right)\right)$$
13	12	2exbidv	$$⊢p=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\to \left(\exists g\exists h\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)\leftrightarrow \exists g\exists h\left(g:A\underset{onto}{⟶}\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\wedge h:\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\underset{1-1}{⟶}B\wedge F=h\circ g\right)\right)$$
14	2 9 13	spcedv	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \exists p\exists g\exists h\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)$$
15		exrot3	$$⊢\exists p\exists g\exists h\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)\leftrightarrow \exists g\exists h\exists p\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)$$
16	14 15	sylib	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \exists g\exists h\exists p\left(g:A\underset{onto}{⟶}p\wedge h:p\underset{1-1}{⟶}B\wedge F=h\circ g\right)$$