Metamath Proof Explorer

Theorem fundcmpsurinj

Description: Every function F : A --> B can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024)

Ref Expression
Assertion fundcmpsurinj 
|- ( ( 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 abrexexg 
 |-  ( A e. V -> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } e. _V )
2 1 adantl 
 |-  ( ( F : A --> B /\ A e. V ) -> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } e. _V )
3 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
4 3 sneqd 
 |-  ( x = y -> { ( F ` x ) } = { ( F ` y ) } )
5 4 imaeq2d 
 |-  ( x = y -> ( `' F " { ( F ` x ) } ) = ( `' F " { ( F ` y ) } ) )
6 5 eqeq2d 
 |-  ( x = y -> ( z = ( `' F " { ( F ` x ) } ) <-> z = ( `' F " { ( F ` y ) } ) ) )
7 6 cbvrexvw 
 |-  ( E. x e. A z = ( `' F " { ( F ` x ) } ) <-> E. y e. A z = ( `' F " { ( F ` y ) } ) )
8 7 abbii 
 |-  { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) }
9 8 fundcmpsurinjpreimafv 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h ( g : A -onto-> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } /\ h : { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -1-1-> B /\ F = ( h o. g ) ) )
10 foeq3 
 |-  ( p = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -> ( g : A -onto-> p <-> g : A -onto-> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } ) )
11 f1eq2 
 |-  ( p = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -> ( h : p -1-1-> B <-> h : { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -1-1-> B ) )
12 10 11 3anbi12d 
 |-  ( p = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -> ( ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) <-> ( g : A -onto-> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } /\ h : { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -1-1-> B /\ F = ( h o. g ) ) ) )
13 12 2exbidv 
 |-  ( p = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -> ( E. g E. h ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) <-> E. g E. h ( g : A -onto-> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } /\ h : { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } -1-1-> B /\ F = ( h o. g ) ) ) )
14 2 9 13 spcedv 
 |-  ( ( F : A --> B /\ A e. V ) -> E. p E. g E. h ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) )
15 exrot3 
 |-  ( E. p E. g E. h ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) <-> E. g E. h E. p ( g : A -onto-> p /\ h : p -1-1-> B /\ F = ( h o. g ) ) )
16 14 15 sylib 
 |-  ( ( 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 ) ) )