fundcmpsurbijinj

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

		Ref	Expression
	Assertion	fundcmpsurbijinj	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h \exists i \exists p \exists q ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$

Proof

Step	Hyp	Ref	Expression
1		ffun	$⊢ F : A ⟶ B \to Fun F$
2		funimaexg	$⊢ (Fun F \land A \in V) \to F [A] \in V$
3	1 2	sylan	$⊢ (F : A ⟶ B \land A \in V) \to F [A] \in V$
4		abrexexg	$⊢ A \in V \to \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \in V$
5	4	adantl	$⊢ (F : A ⟶ B \land A \in V) \to \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \in V$
6		fveq2	$⊢ y = x \to F (y) = F (x)$
7	6	sneqd	$⊢ y = x \to \{F (y)\} = \{F (x)\}$
8	7	imaeq2d	$⊢ y = x \to F^{-1} [\{F (y)\}] = F^{-1} [\{F (x)\}]$
9	8	eqeq2d	$⊢ y = x \to (z = F^{-1} [\{F (y)\}] \leftrightarrow z = F^{-1} [\{F (x)\}])$
10	9	cbvrexvw	$⊢ \exists y \in A z = F^{-1} [\{F (y)\}] \leftrightarrow \exists x \in A z = F^{-1} [\{F (x)\}]$
11	10	abbii	$⊢ \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
12	11	fundcmpsurbijinjpreimafv	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h \exists i ((g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
13		foeq3	$⊢ p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \to (g : A \underset{onto}{⟶} p \leftrightarrow g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\})$
14	13	adantl	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to (g : A \underset{onto}{⟶} p \leftrightarrow g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\})$
15		f1oeq23	$⊢ (p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land q = F [A]) \to (h : p \underset{1-1 onto}{⟶} q \leftrightarrow h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A])$
16	15	ancoms	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to (h : p \underset{1-1 onto}{⟶} q \leftrightarrow h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A])$
17		f1eq2	$⊢ q = F [A] \to (i : q \underset{1-1}{⟶} B \leftrightarrow i : F [A] \underset{1-1}{⟶} B)$
18	17	adantr	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to (i : q \underset{1-1}{⟶} B \leftrightarrow i : F [A] \underset{1-1}{⟶} B)$
19	14 16 18	3anbi123d	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \leftrightarrow (g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B))$
20	19	anbi1d	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to (((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow ((g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g))$
21	20	3exbidv	$⊢ (q = F [A] \land p = \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\}) \to (\exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow \exists g \exists h \exists i ((g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g))$
22	21	spc2egv	$⊢ (F [A] \in V \land \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \in V) \to (\exists g \exists h \exists i ((g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \to \exists q \exists p \exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g))$
23	22	imp	$⊢ ((F [A] \in V \land \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \in V) \land \exists g \exists h \exists i ((g : A \underset{onto}{⟶} \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \land h : \{z \| \exists y \in A z = F^{-1} [\{F (y)\}]\} \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)) \to \exists q \exists p \exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
24	3 5 12 23	syl21anc	$⊢ (F : A ⟶ B \land A \in V) \to \exists q \exists p \exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
25		exrot4	$⊢ \exists q \exists p \exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow \exists g \exists h \exists q \exists p \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
26		excom13	$⊢ \exists q \exists p \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow \exists i \exists p \exists q ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
27	26	2exbii	$⊢ \exists g \exists h \exists q \exists p \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow \exists g \exists h \exists i \exists p \exists q ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
28	25 27	bitri	$⊢ \exists q \exists p \exists g \exists h \exists i ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow \exists g \exists h \exists i \exists p \exists q ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$
29	24 28	sylib	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h \exists i \exists p \exists q ((g : A \underset{onto}{⟶} p \land h : p \underset{1-1 onto}{⟶} q \land i : q \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$

Metamath Proof Explorer

Theorem fundcmpsurbijinj

Proof