Metamath Proof Explorer

Theorem 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 /\ A e. V ) -> E. g E. h E. p ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) )

Proof

Step Hyp Ref Expression
1 mptexg 
 |-  ( A e. V -> ( y e. A |-> ( F ` y ) ) e. _V )
2 1 adantl 
 |-  ( ( F : A --> B /\ A e. V ) -> ( y e. A |-> ( F ` y ) ) e. _V )
3 ffun 
 |-  ( F : A --> B -> Fun F )
4 funimaexg 
 |-  ( ( Fun F /\ A e. V ) -> ( F " A ) e. _V )
5 3 4 sylan 
 |-  ( ( F : A --> B /\ A e. V ) -> ( F " A ) e. _V )
6 5 resiexd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( _I |` ( F " A ) ) e. _V )
7 2 6 5 3jca 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( y e. A |-> ( F ` y ) ) e. _V /\ ( _I |` ( F " A ) ) e. _V /\ ( F " A ) e. _V ) )
8 eqid 
 |-  ( F " A ) = ( F " A )
9 eqid 
 |-  ( y e. A |-> ( F ` y ) ) = ( y e. A |-> ( F ` y ) )
10 eqid 
 |-  ( _I |` ( F " A ) ) = ( _I |` ( F " A ) )
11 8 9 10 fundcmpsurinjimaid 
 |-  ( F : A --> B -> ( ( y e. A |-> ( F ` y ) ) : A -onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B /\ F = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) ) )
12 11 adantr 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( y e. A |-> ( F ` y ) ) : A -onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B /\ F = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) ) )
13 simp1 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> g = ( y e. A |-> ( F ` y ) ) )
14 eqidd 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> A = A )
15 simp3 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> p = ( F " A ) )
16 13 14 15 foeq123d 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( g : A -onto-> p <-> ( y e. A |-> ( F ` y ) ) : A -onto-> ( F " A ) ) )
17 simpl 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> h = ( _I |` ( F " A ) ) )
18 simpr 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> p = ( F " A ) )
19 eqidd 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> B = B )
20 17 18 19 f1eq123d 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( h : p -1-1-> B <-> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
21 20 3adant1 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( h : p -1-1-> B <-> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
22 simpl 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ g = ( y e. A |-> ( F ` y ) ) ) -> h = ( _I |` ( F " A ) ) )
23 simpr 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ g = ( y e. A |-> ( F ` y ) ) ) -> g = ( y e. A |-> ( F ` y ) ) )
24 22 23 coeq12d 
 |-  ( ( h = ( _I |` ( F " A ) ) /\ g = ( y e. A |-> ( F ` y ) ) ) -> ( h o. g ) = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) )
25 24 ancoms 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) ) -> ( h o. g ) = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) )
26 25 3adant3 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( h o. g ) = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) )
27 26 eqeq2d 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( F = ( h o. g ) <-> F = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) ) )
28 16 21 27 3anbi123d 
 |-  ( ( g = ( y e. A |-> ( F ` y ) ) /\ h = ( _I |` ( F " A ) ) /\ p = ( F " A ) ) -> ( ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) <-> ( ( y e. A |-> ( F ` y ) ) : A -onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B /\ F = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) ) ) )
29 28 spc3egv 
 |-  ( ( ( y e. A |-> ( F ` y ) ) e. _V /\ ( _I |` ( F " A ) ) e. _V /\ ( F " A ) e. _V ) -> ( ( ( y e. A |-> ( F ` y ) ) : A -onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B /\ F = ( ( _I |` ( F " A ) ) o. ( y e. A |-> ( F ` y ) ) ) ) -> E. g E. h E. p ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) ) )
30 7 12 29 sylc 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h E. p ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) )