Metamath Proof Explorer

Theorem fundcmpsurbijinj

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

Ref Expression
Assertion fundcmpsurbijinj 
|- ( ( F : A --> B /\ A e. V ) -> E. g E. h E. i E. p E. q ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( F : A --> B -> Fun F )
2 funimaexg 
 |-  ( ( Fun F /\ A e. V ) -> ( F " A ) e. _V )
3 1 2 sylan 
 |-  ( ( F : A --> B /\ A e. V ) -> ( F " A ) e. _V )
4 abrexexg 
 |-  ( A e. V -> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } e. _V )
5 4 adantl 
 |-  ( ( F : A --> B /\ A e. V ) -> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } e. _V )
6 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
7 6 sneqd 
 |-  ( y = x -> { ( F ` y ) } = { ( F ` x ) } )
8 7 imaeq2d 
 |-  ( y = x -> ( `' F " { ( F ` y ) } ) = ( `' F " { ( F ` x ) } ) )
9 8 eqeq2d 
 |-  ( y = x -> ( z = ( `' F " { ( F ` y ) } ) <-> z = ( `' F " { ( F ` x ) } ) ) )
10 9 cbvrexvw 
 |-  ( E. y e. A z = ( `' F " { ( F ` y ) } ) <-> E. x e. A z = ( `' F " { ( F ` x ) } ) )
11 10 abbii 
 |-  { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
12 11 fundcmpsurbijinjpreimafv 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h E. i ( ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
13 foeq3 
 |-  ( p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -> ( g : A -onto-> p <-> g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) )
14 13 adantl 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( g : A -onto-> p <-> g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) )
15 f1oeq23 
 |-  ( ( p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ q = ( F " A ) ) -> ( h : p -1-1-onto-> q <-> h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) ) )
16 15 ancoms 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( h : p -1-1-onto-> q <-> h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) ) )
17 f1eq2 
 |-  ( q = ( F " A ) -> ( i : q -1-1-> B <-> i : ( F " A ) -1-1-> B ) )
18 17 adantr 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( i : q -1-1-> B <-> i : ( F " A ) -1-1-> B ) )
19 14 16 18 3anbi123d 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) <-> ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) ) )
20 19 anbi1d 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> ( ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) ) )
21 20 3exbidv 
 |-  ( ( q = ( F " A ) /\ p = { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } ) -> ( E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> E. g E. h E. i ( ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) ) )
22 21 spc2egv 
 |-  ( ( ( F " A ) e. _V /\ { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } e. _V ) -> ( E. g E. h E. i ( ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) -> E. q E. p E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) ) )
23 22 imp 
 |-  ( ( ( ( F " A ) e. _V /\ { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } e. _V ) /\ E. g E. h E. i ( ( g : A -onto-> { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } /\ h : { z | E. y e. A z = ( `' F " { ( F ` y ) } ) } -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) ) -> E. q E. p E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
24 3 5 12 23 syl21anc 
 |-  ( ( F : A --> B /\ A e. V ) -> E. q E. p E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
25 exrot4 
 |-  ( E. q E. p E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> E. g E. h E. q E. p E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
26 excom13 
 |-  ( E. q E. p E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> E. i E. p E. q ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
27 26 2exbii 
 |-  ( E. g E. h E. q E. p E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> E. g E. h E. i E. p E. q ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
28 25 27 bitri 
 |-  ( E. q E. p E. g E. h E. i ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> E. g E. h E. i E. p E. q ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )
29 24 28 sylib 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h E. i E. p E. q ( ( g : A -onto-> p /\ h : p -1-1-onto-> q /\ i : q -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )