Theorem fundcmpsurinjimaid

Description: Every function F : A --> B can be decomposed into a surjective function onto the image ( F " A ) of the domain of F and an injective function from the image ( F " A ) . (Contributed by AV, 17-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinjimaid.i	⊢ 𝐼 = ( 𝐹 “ 𝐴 )
	fundcmpsurinjimaid.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) )
	fundcmpsurinjimaid.h	⊢ 𝐻 = ( I ↾ 𝐼 )
Assertion	fundcmpsurinjimaid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐺 : 𝐴 –onto→ 𝐼 ∧ 𝐻 : 𝐼 –1-1→ 𝐵 ∧ 𝐹 = ( 𝐻 ∘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinjimaid.i	⊢ 𝐼 = ( 𝐹 “ 𝐴 )
2		fundcmpsurinjimaid.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) )
3		fundcmpsurinjimaid.h	⊢ 𝐻 = ( I ↾ 𝐼 )
4		fimadmfo	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
5		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
6		dffn5	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
7	5 6	sylib	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
8	7	eqcomd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
9	2 8	syl5eq	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐺 = 𝐹 )
10		eqidd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = 𝐴 )
11	1	a1i	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐼 = ( 𝐹 “ 𝐴 ) )
12	9 10 11	foeq123d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐺 : 𝐴 –onto→ 𝐼 ↔ 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ) )
13	4 12	mpbird	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐺 : 𝐴 –onto→ 𝐼 )
14		f1oi	⊢ ( I ↾ 𝐼 ) : 𝐼 –1-1-onto→ 𝐼
15		f1of1	⊢ ( ( I ↾ 𝐼 ) : 𝐼 –1-1-onto→ 𝐼 → ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 )
16		f1eq1	⊢ ( 𝐻 = ( I ↾ 𝐼 ) → ( 𝐻 : 𝐼 –1-1→ 𝐼 ↔ ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 ) )
17	3 16	ax-mp	⊢ ( 𝐻 : 𝐼 –1-1→ 𝐼 ↔ ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 )
18	17	biimpri	⊢ ( ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 → 𝐻 : 𝐼 –1-1→ 𝐼 )
19		fimass	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
20	1 19	eqsstrid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐼 ⊆ 𝐵 )
21		f1ss	⊢ ( ( 𝐻 : 𝐼 –1-1→ 𝐼 ∧ 𝐼 ⊆ 𝐵 ) → 𝐻 : 𝐼 –1-1→ 𝐵 )
22	18 20 21	syl2an	⊢ ( ( ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐻 : 𝐼 –1-1→ 𝐵 )
23	22	ex	⊢ ( ( I ↾ 𝐼 ) : 𝐼 –1-1→ 𝐼 → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐻 : 𝐼 –1-1→ 𝐵 ) )
24	14 15 23	mp2b	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐻 : 𝐼 –1-1→ 𝐵 )
25	3	fveq1i	⊢ ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( I ↾ 𝐼 ) ‘ ( 𝐹 ‘ 𝑥 ) )
26	5	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
27		simpr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
28	26 27 27	fnfvimad	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) )
29	28 1	eleqtrrdi	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 )
30		fvresi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 → ( ( I ↾ 𝐼 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
31	29 30	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( I ↾ 𝐼 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
32	25 31	syl5eq	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
33	32	mpteq2dva	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
34	2	coeq2i	⊢ ( 𝐻 ∘ 𝐺 ) = ( 𝐻 ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
35		f1of	⊢ ( ( I ↾ 𝐼 ) : 𝐼 –1-1-onto→ 𝐼 → ( I ↾ 𝐼 ) : 𝐼 ⟶ 𝐼 )
36	14 35	ax-mp	⊢ ( I ↾ 𝐼 ) : 𝐼 ⟶ 𝐼
37	3	feq1i	⊢ ( 𝐻 : 𝐼 ⟶ 𝐼 ↔ ( I ↾ 𝐼 ) : 𝐼 ⟶ 𝐼 )
38	36 37	mpbir	⊢ 𝐻 : 𝐼 ⟶ 𝐼
39	38	a1i	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐻 : 𝐼 ⟶ 𝐼 )
40	39 29	cofmpt	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐻 ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
41	34 40	syl5eq	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐻 ∘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
42	33 41 7	3eqtr4rd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝐻 ∘ 𝐺 ) )
43	13 24 42	3jca	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐺 : 𝐴 –onto→ 𝐼 ∧ 𝐻 : 𝐼 –1-1→ 𝐵 ∧ 𝐹 = ( 𝐻 ∘ 𝐺 ) ) )