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	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h \exists p (g : A \underset{onto}{⟶} p \land h : p \underset{1-1}{⟶} B \land F = h \circ g)$

Proof

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

Metamath Proof Explorer

Theorem fundcmpsurinjALT

Proof