fundcmpsurinjpreimafv

Description: Every function F : A --> B can be decomposed into a surjective function onto P and an injective function from P . (Contributed by AV, 12-Mar-2024) (Proof shortened by AV, 22-Mar-2024)

		Ref	Expression
	Hypothesis	fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
	Assertion	fundcmpsurinjpreimafv	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g)$

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2	1	fundcmpsurbijinjpreimafv	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists f \exists j ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)$
3		vex	$⊢ j \in V$
4		vex	$⊢ f \in V$
5	3 4	coex	$⊢ j \circ f \in V$
6		simprl1	$⊢ ((F : A ⟶ B \land A \in V) \land ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)) \to g : A \underset{onto}{⟶} P$
7		simp3	$⊢ (g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \to j : F [A] \underset{1-1}{⟶} B$
8		f1of1	$⊢ f : P \underset{1-1 onto}{⟶} F [A] \to f : P \underset{1-1}{⟶} F [A]$
9	8	3ad2ant2	$⊢ (g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \to f : P \underset{1-1}{⟶} F [A]$
10		f1co	$⊢ (j : F [A] \underset{1-1}{⟶} B \land f : P \underset{1-1}{⟶} F [A]) \to (j \circ f) : P \underset{1-1}{⟶} B$
11	7 9 10	syl2anc	$⊢ (g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \to (j \circ f) : P \underset{1-1}{⟶} B$
12	11	ad2antrl	$⊢ ((F : A ⟶ B \land A \in V) \land ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)) \to (j \circ f) : P \underset{1-1}{⟶} B$
13		simprr	$⊢ ((F : A ⟶ B \land A \in V) \land ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)) \to F = (j \circ f) \circ g$
14	6 12 13	3jca	$⊢ ((F : A ⟶ B \land A \in V) \land ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)) \to (g : A \underset{onto}{⟶} P \land (j \circ f) : P \underset{1-1}{⟶} B \land F = (j \circ f) \circ g)$
15		f1eq1	$⊢ h = j \circ f \to (h : P \underset{1-1}{⟶} B \leftrightarrow (j \circ f) : P \underset{1-1}{⟶} B)$
16		coeq1	$⊢ h = j \circ f \to h \circ g = (j \circ f) \circ g$
17	16	eqeq2d	$⊢ h = j \circ f \to (F = h \circ g \leftrightarrow F = (j \circ f) \circ g)$
18	15 17	3anbi23d	$⊢ h = j \circ f \to ((g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g) \leftrightarrow (g : A \underset{onto}{⟶} P \land (j \circ f) : P \underset{1-1}{⟶} B \land F = (j \circ f) \circ g))$
19	18	spcegv	$⊢ j \circ f \in V \to ((g : A \underset{onto}{⟶} P \land (j \circ f) : P \underset{1-1}{⟶} B \land F = (j \circ f) \circ g) \to \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g))$
20	5 14 19	mpsyl	$⊢ ((F : A ⟶ B \land A \in V) \land ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g)) \to \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g)$
21	20	ex	$⊢ (F : A ⟶ B \land A \in V) \to (((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g) \to \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g))$
22	21	exlimdvv	$⊢ (F : A ⟶ B \land A \in V) \to (\exists f \exists j ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g) \to \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g))$
23	22	eximdv	$⊢ (F : A ⟶ B \land A \in V) \to (\exists g \exists f \exists j ((g : A \underset{onto}{⟶} P \land f : P \underset{1-1 onto}{⟶} F [A] \land j : F [A] \underset{1-1}{⟶} B) \land F = (j \circ f) \circ g) \to \exists g \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g))$
24	2 23	mpd	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h (g : A \underset{onto}{⟶} P \land h : P \underset{1-1}{⟶} B \land F = h \circ g)$

Metamath Proof Explorer

Theorem fundcmpsurinjpreimafv

Proof