Theorem fundcmpsurinjALT

Description: Alternate proof of fundcmpsurinj , based on fundcmpsurinjimaid : Every function F : A --> B can be decomposed into a surjective and an injective function. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by AV, 13-Mar-2024)

	Ref	Expression
Assertion	fundcmpsurinjALT	$$⊢\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		mptexg	$$⊢A\in V\to \left(y\in A⟼F\left(y\right)\right)\in \mathrm{V}$$
2	1	adantl	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \left(y\in A⟼F\left(y\right)\right)\in \mathrm{V}$$
3		ffun	$$⊢F:A⟶B\to \mathrm{Fun}F$$
4		funimaexg	$$⊢\left(\mathrm{Fun}F\wedge A\in V\right)\to F\left[A\right]\in \mathrm{V}$$
5	3 4	sylan	$$⊢\left(F:A⟶B\wedge A\in V\right)\to F\left[A\right]\in \mathrm{V}$$
6	5	resiexd	$$⊢\left(F:A⟶B\wedge A\in V\right)\to {\mathrm{I}\upharpoonright }_{F\left[A\right]}\in \mathrm{V}$$
7	2 6 5	3jca	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \left(\left(y\in A⟼F\left(y\right)\right)\in \mathrm{V}\wedge {\mathrm{I}\upharpoonright }_{F\left[A\right]}\in \mathrm{V}\wedge F\left[A\right]\in \mathrm{V}\right)$$
8		eqid	$$⊢F\left[A\right]=F\left[A\right]$$
9		eqid	$$⊢\left(y\in A⟼F\left(y\right)\right)=\left(y\in A⟼F\left(y\right)\right)$$
10		eqid	$$⊢{\mathrm{I}\upharpoonright }_{F\left[A\right]}={\mathrm{I}\upharpoonright }_{F\left[A\right]}$$
11	8 9 10	fundcmpsurinjimaid	$$⊢F:A⟶B\to \left(\left(y\in A⟼F\left(y\right)\right):A\underset{onto}{⟶}F\left[A\right]\wedge \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\wedge F=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)\right)$$
12	11	adantr	$$⊢\left(F:A⟶B\wedge A\in V\right)\to \left(\left(y\in A⟼F\left(y\right)\right):A\underset{onto}{⟶}F\left[A\right]\wedge \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\wedge F=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)\right)$$
13		simp1	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to g=\left(y\in A⟼F\left(y\right)\right)$$
14		eqidd	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to A=A$$
15		simp3	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to p=F\left[A\right]$$
16	13 14 15	foeq123d	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to \left(g:A\underset{onto}{⟶}p\leftrightarrow \left(y\in A⟼F\left(y\right)\right):A\underset{onto}{⟶}F\left[A\right]\right)$$
17		simpl	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to h={\mathrm{I}\upharpoonright }_{F\left[A\right]}$$
18		simpr	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to p=F\left[A\right]$$
19		eqidd	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to B=B$$
20	17 18 19	f1eq123d	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to \left(h:p\underset{1-1}{⟶}B\leftrightarrow \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\right)$$
21	20	3adant1	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to \left(h:p\underset{1-1}{⟶}B\leftrightarrow \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\right)$$
22		simpl	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge g=\left(y\in A⟼F\left(y\right)\right)\right)\to h={\mathrm{I}\upharpoonright }_{F\left[A\right]}$$
23		simpr	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge g=\left(y\in A⟼F\left(y\right)\right)\right)\to g=\left(y\in A⟼F\left(y\right)\right)$$
24	22 23	coeq12d	$$⊢\left(h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge g=\left(y\in A⟼F\left(y\right)\right)\right)\to h\circ g=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)$$
25	24	ancoms	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\to h\circ g=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)$$
26	25	3adant3	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to h\circ g=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)$$
27	26	eqeq2d	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\right]\right)\to \left(F=h\circ g\leftrightarrow F=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)\right)$$
28	16 21 27	3anbi123d	$$⊢\left(g=\left(y\in A⟼F\left(y\right)\right)\wedge h={\mathrm{I}\upharpoonright }_{F\left[A\right]}\wedge p=F\left[A\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(\left(y\in A⟼F\left(y\right)\right):A\underset{onto}{⟶}F\left[A\right]\wedge \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\wedge F=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)\right)\right)$$
29	28	spc3egv	$$⊢\left(\left(y\in A⟼F\left(y\right)\right)\in \mathrm{V}\wedge {\mathrm{I}\upharpoonright }_{F\left[A\right]}\in \mathrm{V}\wedge F\left[A\right]\in \mathrm{V}\right)\to \left(\left(\left(y\in A⟼F\left(y\right)\right):A\underset{onto}{⟶}F\left[A\right]\wedge \left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right):F\left[A\right]\underset{1-1}{⟶}B\wedge F=\left({\mathrm{I}\upharpoonright }_{F\left[A\right]}\right)\circ \left(y\in A⟼F\left(y\right)\right)\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)\right)$$
30	7 12 29	sylc	$$⊢\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)$$