Metamath Proof Explorer

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 
|- I = ( F " A )
fundcmpsurinjimaid.g 
|- G = ( x e. A |-> ( F ` x ) )
fundcmpsurinjimaid.h 
|- H = ( _I |` I )
Assertion fundcmpsurinjimaid 
|- ( F : A --> B -> ( G : A -onto-> I /\ H : I -1-1-> B /\ F = ( H o. G ) ) )

Proof

Step Hyp Ref Expression
1 fundcmpsurinjimaid.i 
 |-  I = ( F " A )
2 fundcmpsurinjimaid.g 
 |-  G = ( x e. A |-> ( F ` x ) )
3 fundcmpsurinjimaid.h 
 |-  H = ( _I |` I )
4 fimadmfo 
 |-  ( F : A --> B -> F : A -onto-> ( F " A ) )
5 ffn 
 |-  ( F : A --> B -> F Fn A )
6 dffn5 
 |-  ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
7 5 6 sylib 
 |-  ( F : A --> B -> F = ( x e. A |-> ( F ` x ) ) )
8 7 eqcomd 
 |-  ( F : A --> B -> ( x e. A |-> ( F ` x ) ) = F )
9 2 8 syl5eq 
 |-  ( F : A --> B -> G = F )
10 eqidd 
 |-  ( F : A --> B -> A = A )
11 1 a1i 
 |-  ( F : A --> B -> I = ( F " A ) )
12 9 10 11 foeq123d 
 |-  ( F : A --> B -> ( G : A -onto-> I <-> F : A -onto-> ( F " A ) ) )
13 4 12 mpbird 
 |-  ( F : A --> B -> G : A -onto-> I )
14 f1oi 
 |-  ( _I |` I ) : I -1-1-onto-> I
15 f1of1 
 |-  ( ( _I |` I ) : I -1-1-onto-> I -> ( _I |` I ) : I -1-1-> I )
16 f1eq1 
 |-  ( H = ( _I |` I ) -> ( H : I -1-1-> I <-> ( _I |` I ) : I -1-1-> I ) )
17 3 16 ax-mp 
 |-  ( H : I -1-1-> I <-> ( _I |` I ) : I -1-1-> I )
18 17 biimpri 
 |-  ( ( _I |` I ) : I -1-1-> I -> H : I -1-1-> I )
19 fimass 
 |-  ( F : A --> B -> ( F " A ) C_ B )
20 1 19 eqsstrid 
 |-  ( F : A --> B -> I C_ B )
21 f1ss 
 |-  ( ( H : I -1-1-> I /\ I C_ B ) -> H : I -1-1-> B )
22 18 20 21 syl2an 
 |-  ( ( ( _I |` I ) : I -1-1-> I /\ F : A --> B ) -> H : I -1-1-> B )
23 22 ex 
 |-  ( ( _I |` I ) : I -1-1-> I -> ( F : A --> B -> H : I -1-1-> B ) )
24 14 15 23 mp2b 
 |-  ( F : A --> B -> H : I -1-1-> B )
25 3 fveq1i 
 |-  ( H ` ( F ` x ) ) = ( ( _I |` I ) ` ( F ` x ) )
26 5 adantr 
 |-  ( ( F : A --> B /\ x e. A ) -> F Fn A )
27 simpr 
 |-  ( ( F : A --> B /\ x e. A ) -> x e. A )
28 26 27 27 fnfvimad 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
29 28 1 eleqtrrdi 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. I )
30 fvresi 
 |-  ( ( F ` x ) e. I -> ( ( _I |` I ) ` ( F ` x ) ) = ( F ` x ) )
31 29 30 syl 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( _I |` I ) ` ( F ` x ) ) = ( F ` x ) )
32 25 31 syl5eq 
 |-  ( ( F : A --> B /\ x e. A ) -> ( H ` ( F ` x ) ) = ( F ` x ) )
33 32 mpteq2dva 
 |-  ( F : A --> B -> ( x e. A |-> ( H ` ( F ` x ) ) ) = ( x e. A |-> ( F ` x ) ) )
34 2 coeq2i 
 |-  ( H o. G ) = ( H o. ( x e. A |-> ( F ` x ) ) )
35 f1of 
 |-  ( ( _I |` I ) : I -1-1-onto-> I -> ( _I |` I ) : I --> I )
36 14 35 ax-mp 
 |-  ( _I |` I ) : I --> I
37 3 feq1i 
 |-  ( H : I --> I <-> ( _I |` I ) : I --> I )
38 36 37 mpbir 
 |-  H : I --> I
39 38 a1i 
 |-  ( F : A --> B -> H : I --> I )
40 39 29 cofmpt 
 |-  ( F : A --> B -> ( H o. ( x e. A |-> ( F ` x ) ) ) = ( x e. A |-> ( H ` ( F ` x ) ) ) )
41 34 40 syl5eq 
 |-  ( F : A --> B -> ( H o. G ) = ( x e. A |-> ( H ` ( F ` x ) ) ) )
42 33 41 7 3eqtr4rd 
 |-  ( F : A --> B -> F = ( H o. G ) )
43 13 24 42 3jca 
 |-  ( F : A --> B -> ( G : A -onto-> I /\ H : I -1-1-> B /\ F = ( H o. G ) ) )