Metamath Proof Explorer

Theorem fundcmpsurinjpreimafv

Description: Every function F : A --> B can be decomposed into a surjective function onto P and an injective function from P . (Contributed by AV, 12-Mar-2024) (Proof shortened by AV, 22-Mar-2024)

Ref Expression
Hypothesis fundcmpsurinj.p 
|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion fundcmpsurinjpreimafv 
|- ( ( F : A --> B /\ A e. V ) -> E. g E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) )

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p 
 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2 1 fundcmpsurbijinjpreimafv 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. f E. j ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) )
3 vex 
 |-  j e. _V
4 vex 
 |-  f e. _V
5 3 4 coex 
 |-  ( j o. f ) e. _V
6 simprl1 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) ) -> g : A -onto-> P )
7 simp3 
 |-  ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) -> j : ( F " A ) -1-1-> B )
8 f1of1 
 |-  ( f : P -1-1-onto-> ( F " A ) -> f : P -1-1-> ( F " A ) )
9 8 3ad2ant2 
 |-  ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) -> f : P -1-1-> ( F " A ) )
10 f1co 
 |-  ( ( j : ( F " A ) -1-1-> B /\ f : P -1-1-> ( F " A ) ) -> ( j o. f ) : P -1-1-> B )
11 7 9 10 syl2anc 
 |-  ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) -> ( j o. f ) : P -1-1-> B )
12 11 ad2antrl 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) ) -> ( j o. f ) : P -1-1-> B )
13 simprr 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) ) -> F = ( ( j o. f ) o. g ) )
14 6 12 13 3jca 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) ) -> ( g : A -onto-> P /\ ( j o. f ) : P -1-1-> B /\ F = ( ( j o. f ) o. g ) ) )
15 f1eq1 
 |-  ( h = ( j o. f ) -> ( h : P -1-1-> B <-> ( j o. f ) : P -1-1-> B ) )
16 coeq1 
 |-  ( h = ( j o. f ) -> ( h o. g ) = ( ( j o. f ) o. g ) )
17 16 eqeq2d 
 |-  ( h = ( j o. f ) -> ( F = ( h o. g ) <-> F = ( ( j o. f ) o. g ) ) )
18 15 17 3anbi23d 
 |-  ( h = ( j o. f ) -> ( ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) <-> ( g : A -onto-> P /\ ( j o. f ) : P -1-1-> B /\ F = ( ( j o. f ) o. g ) ) ) )
19 18 spcegv 
 |-  ( ( j o. f ) e. _V -> ( ( g : A -onto-> P /\ ( j o. f ) : P -1-1-> B /\ F = ( ( j o. f ) o. g ) ) -> E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) ) )
20 5 14 19 mpsyl 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) ) -> E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) )
21 20 ex 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) -> E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) ) )
22 21 exlimdvv 
 |-  ( ( F : A --> B /\ A e. V ) -> ( E. f E. j ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) -> E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) ) )
23 22 eximdv 
 |-  ( ( F : A --> B /\ A e. V ) -> ( E. g E. f E. j ( ( g : A -onto-> P /\ f : P -1-1-onto-> ( F " A ) /\ j : ( F " A ) -1-1-> B ) /\ F = ( ( j o. f ) o. g ) ) -> E. g E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) ) )
24 2 23 mpd 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h ( g : A -onto-> P /\ h : P -1-1-> B /\ F = ( h o. g ) ) )