fundcmpsurbijinjpreimafv

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

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

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		simpr	$⊢ (F : A ⟶ B \land A \in V) \to A \in V$
3	2	mptexd	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ F^{-1} [\{F (a)\}]) \in V$
4	1	setpreimafvex	$⊢ A \in V \to P \in V$
5	4	adantl	$⊢ (F : A ⟶ B \land A \in V) \to P \in V$
6	5	mptexd	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ⋃ F [y]) \in V$
7		ffun	$⊢ F : A ⟶ B \to Fun F$
8		funimaexg	$⊢ (Fun F \land A \in V) \to F [A] \in V$
9	7 8	sylan	$⊢ (F : A ⟶ B \land A \in V) \to F [A] \in V$
10	9	resiexd	$⊢ (F : A ⟶ B \land A \in V) \to {I ↾}_{F [A]} \in V$
11	3 6 10	3jca	$⊢ (F : A ⟶ B \land A \in V) \to ((a \in A ⟼ F^{-1} [\{F (a)\}]) \in V \land (y \in P ⟼ ⋃ F [y]) \in V \land {I ↾}_{F [A]} \in V)$
12		ffn	$⊢ F : A ⟶ B \to F Fn A$
13		fveq2	$⊢ a = x \to F (a) = F (x)$
14	13	sneqd	$⊢ a = x \to \{F (a)\} = \{F (x)\}$
15	14	imaeq2d	$⊢ a = x \to F^{-1} [\{F (a)\}] = F^{-1} [\{F (x)\}]$
16	15	cbvmptv	$⊢ (a \in A ⟼ F^{-1} [\{F (a)\}]) = (x \in A ⟼ F^{-1} [\{F (x)\}])$
17	1 16	fundcmpsurinjlem2	$⊢ (F Fn A \land A \in V) \to (a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P$
18	12 17	sylan	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P$
19		eqid	$⊢ (y \in P ⟼ ⋃ F [y]) = (y \in P ⟼ ⋃ F [y])$
20	1 19	imasetpreimafvbij	$⊢ (F Fn A \land A \in V) \to (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A]$
21	12 20	sylan	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A]$
22		f1oi	$⊢ ({I ↾}_{F [A]}) : F [A] \underset{1-1 onto}{⟶} F [A]$
23		f1of1	$⊢ ({I ↾}_{F [A]}) : F [A] \underset{1-1 onto}{⟶} F [A] \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} F [A]$
24		fimass	$⊢ F : A ⟶ B \to F [A] \subseteq B$
25		f1ss	$⊢ (({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} F [A] \land F [A] \subseteq B) \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B$
26	24 25	sylan2	$⊢ (({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} F [A] \land F : A ⟶ B) \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B$
27	26	ex	$⊢ ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} F [A] \to (F : A ⟶ B \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B)$
28	22 23 27	mp2b	$⊢ F : A ⟶ B \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B$
29	28	adantr	$⊢ (F : A ⟶ B \land A \in V) \to ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B$
30	18 21 29	3jca	$⊢ (F : A ⟶ B \land A \in V) \to ((a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P \land (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A] \land ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B)$
31	12	adantr	$⊢ (F : A ⟶ B \land A \in V) \to F Fn A$
32		uniimaprimaeqfv	$⊢ (F Fn A \land a \in A) \to ⋃ F [F^{-1} [\{F (a)\}]] = F (a)$
33	31 32	sylan	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to ⋃ F [F^{-1} [\{F (a)\}]] = F (a)$
34	33	fveq2d	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to ({I ↾}_{F [A]}) (⋃ F [F^{-1} [\{F (a)\}]]) = ({I ↾}_{F [A]}) (F (a))$
35	34	mpteq2dva	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ ({I ↾}_{F [A]}) (⋃ F [F^{-1} [\{F (a)\}]])) = (a \in A ⟼ ({I ↾}_{F [A]}) (F (a)))$
36		ffrn	$⊢ F : A ⟶ B \to F : A ⟶ ran F$
37	36	adantr	$⊢ (F : A ⟶ B \land A \in V) \to F : A ⟶ ran F$
38	37	funfvima2d	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to F (a) \in F [A]$
39		fvresi	$⊢ F (a) \in F [A] \to ({I ↾}_{F [A]}) (F (a)) = F (a)$
40	38 39	syl	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to ({I ↾}_{F [A]}) (F (a)) = F (a)$
41	40	mpteq2dva	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ ({I ↾}_{F [A]}) (F (a))) = (a \in A ⟼ F (a))$
42	35 41	eqtrd	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ ({I ↾}_{F [A]}) (⋃ F [F^{-1} [\{F (a)\}]])) = (a \in A ⟼ F (a))$
43	12	ad2antrr	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to F Fn A$
44	2	adantr	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to A \in V$
45		simpr	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to a \in A$
46	1	preimafvelsetpreimafv	$⊢ (F Fn A \land A \in V \land a \in A) \to F^{-1} [\{F (a)\}] \in P$
47	43 44 45 46	syl3anc	$⊢ ((F : A ⟶ B \land A \in V) \land a \in A) \to F^{-1} [\{F (a)\}] \in P$
48		eqidd	$⊢ (F : A ⟶ B \land A \in V) \to (a \in A ⟼ F^{-1} [\{F (a)\}]) = (a \in A ⟼ F^{-1} [\{F (a)\}])$
49		eqidd	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) = (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y]))$
50		imaeq2	$⊢ y = F^{-1} [\{F (a)\}] \to F [y] = F [F^{-1} [\{F (a)\}]]$
51	50	unieqd	$⊢ y = F^{-1} [\{F (a)\}] \to ⋃ F [y] = ⋃ F [F^{-1} [\{F (a)\}]]$
52	51	fveq2d	$⊢ y = F^{-1} [\{F (a)\}] \to ({I ↾}_{F [A]}) (⋃ F [y]) = ({I ↾}_{F [A]}) (⋃ F [F^{-1} [\{F (a)\}]])$
53	47 48 49 52	fmptco	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}]) = (a \in A ⟼ ({I ↾}_{F [A]}) (⋃ F [F^{-1} [\{F (a)\}]]))$
54		dffn5	$⊢ F Fn A \leftrightarrow F = (a \in A ⟼ F (a))$
55	12 54	sylib	$⊢ F : A ⟶ B \to F = (a \in A ⟼ F (a))$
56	55	adantr	$⊢ (F : A ⟶ B \land A \in V) \to F = (a \in A ⟼ F (a))$
57	42 53 56	3eqtr4rd	$⊢ (F : A ⟶ B \land A \in V) \to F = (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])$
58		f1of	$⊢ ({I ↾}_{F [A]}) : F [A] \underset{1-1 onto}{⟶} F [A] \to ({I ↾}_{F [A]}) : F [A] ⟶ F [A]$
59	22 58	mp1i	$⊢ F Fn A \to ({I ↾}_{F [A]}) : F [A] ⟶ F [A]$
60		fnima	$⊢ F Fn A \to F [A] = ran F$
61	60	eqcomd	$⊢ F Fn A \to ran F = F [A]$
62	61	feq2d	$⊢ F Fn A \to (({I ↾}_{F [A]}) : ran F ⟶ F [A] \leftrightarrow ({I ↾}_{F [A]}) : F [A] ⟶ F [A])$
63	59 62	mpbird	$⊢ F Fn A \to ({I ↾}_{F [A]}) : ran F ⟶ F [A]$
64	1	uniimaelsetpreimafv	$⊢ (F Fn A \land y \in P) \to ⋃ F [y] \in ran F$
65	63 64	cofmpt	$⊢ F Fn A \to ({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y]) = (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y]))$
66	65	eqcomd	$⊢ F Fn A \to (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) = ({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])$
67	31 66	syl	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) = ({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])$
68	67	coeq1d	$⊢ (F : A ⟶ B \land A \in V) \to (y \in P ⟼ ({I ↾}_{F [A]}) (⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}]) = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])$
69	57 68	eqtrd	$⊢ (F : A ⟶ B \land A \in V) \to F = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])$
70	30 69	jca	$⊢ (F : A ⟶ B \land A \in V) \to (((a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P \land (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A] \land ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B) \land F = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}]))$
71		foeq1	$⊢ g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \to (g : A \underset{onto}{⟶} P \leftrightarrow (a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P)$
72	71	3ad2ant1	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (g : A \underset{onto}{⟶} P \leftrightarrow (a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P)$
73		f1oeq1	$⊢ h = (y \in P ⟼ ⋃ F [y]) \to (h : P \underset{1-1 onto}{⟶} F [A] \leftrightarrow (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A])$
74	73	3ad2ant2	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (h : P \underset{1-1 onto}{⟶} F [A] \leftrightarrow (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A])$
75		f1eq1	$⊢ i = {I ↾}_{F [A]} \to (i : F [A] \underset{1-1}{⟶} B \leftrightarrow ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B)$
76	75	3ad2ant3	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (i : F [A] \underset{1-1}{⟶} B \leftrightarrow ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B)$
77	72 74 76	3anbi123d	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to ((g : A \underset{onto}{⟶} P \land h : P \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \leftrightarrow ((a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P \land (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A] \land ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B))$
78		simp3	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to i = {I ↾}_{F [A]}$
79		simp2	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to h = (y \in P ⟼ ⋃ F [y])$
80	78 79	coeq12d	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to i \circ h = ({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])$
81		simp1	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to g = (a \in A ⟼ F^{-1} [\{F (a)\}])$
82	80 81	coeq12d	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (i \circ h) \circ g = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])$
83	82	eqeq2d	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (F = (i \circ h) \circ g \leftrightarrow F = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}]))$
84	77 83	anbi12d	$⊢ (g = (a \in A ⟼ F^{-1} [\{F (a)\}]) \land h = (y \in P ⟼ ⋃ F [y]) \land i = {I ↾}_{F [A]}) \to (((g : A \underset{onto}{⟶} P \land h : P \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g) \leftrightarrow (((a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P \land (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A] \land ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B) \land F = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])))$
85	84	spc3egv	$⊢ ((a \in A ⟼ F^{-1} [\{F (a)\}]) \in V \land (y \in P ⟼ ⋃ F [y]) \in V \land {I ↾}_{F [A]} \in V) \to ((((a \in A ⟼ F^{-1} [\{F (a)\}]) : A \underset{onto}{⟶} P \land (y \in P ⟼ ⋃ F [y]) : P \underset{1-1 onto}{⟶} F [A] \land ({I ↾}_{F [A]}) : F [A] \underset{1-1}{⟶} B) \land F = (({I ↾}_{F [A]}) \circ (y \in P ⟼ ⋃ F [y])) \circ (a \in A ⟼ F^{-1} [\{F (a)\}])) \to \exists g \exists h \exists i ((g : A \underset{onto}{⟶} P \land h : P \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g))$
86	11 70 85	sylc	$⊢ (F : A ⟶ B \land A \in V) \to \exists g \exists h \exists i ((g : A \underset{onto}{⟶} P \land h : P \underset{1-1 onto}{⟶} F [A] \land i : F [A] \underset{1-1}{⟶} B) \land F = (i \circ h) \circ g)$

Metamath Proof Explorer

Theorem fundcmpsurbijinjpreimafv

Proof