Metamath Proof Explorer

Theorem fundcmpsurbijinjpreimafv

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

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

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p 
 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2 simpr 
 |-  ( ( F : A --> B /\ A e. V ) -> A e. V )
3 2 mptexd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) e. _V )
4 1 setpreimafvex 
 |-  ( A e. V -> P e. _V )
5 4 adantl 
 |-  ( ( F : A --> B /\ A e. V ) -> P e. _V )
6 5 mptexd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( y e. P |-> U. ( F " y ) ) e. _V )
7 ffun 
 |-  ( F : A --> B -> Fun F )
8 funimaexg 
 |-  ( ( Fun F /\ A e. V ) -> ( F " A ) e. _V )
9 7 8 sylan 
 |-  ( ( F : A --> B /\ A e. V ) -> ( F " A ) e. _V )
10 9 resiexd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( _I |` ( F " A ) ) e. _V )
11 3 6 10 3jca 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) e. _V /\ ( y e. P |-> U. ( F " y ) ) e. _V /\ ( _I |` ( F " A ) ) e. _V ) )
12 ffn 
 |-  ( F : A --> B -> F Fn A )
13 fveq2 
 |-  ( a = x -> ( F ` a ) = ( F ` x ) )
14 13 sneqd 
 |-  ( a = x -> { ( F ` a ) } = { ( F ` x ) } )
15 14 imaeq2d 
 |-  ( a = x -> ( `' F " { ( F ` a ) } ) = ( `' F " { ( F ` x ) } ) )
16 15 cbvmptv 
 |-  ( a e. A |-> ( `' F " { ( F ` a ) } ) ) = ( x e. A |-> ( `' F " { ( F ` x ) } ) )
17 1 16 fundcmpsurinjlem2 
 |-  ( ( F Fn A /\ A e. V ) -> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P )
18 12 17 sylan 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P )
19 eqid 
 |-  ( y e. P |-> U. ( F " y ) ) = ( y e. P |-> U. ( F " y ) )
20 1 19 imasetpreimafvbij 
 |-  ( ( F Fn A /\ A e. V ) -> ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) )
21 12 20 sylan 
 |-  ( ( F : A --> B /\ A e. V ) -> ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) )
22 f1oi 
 |-  ( _I |` ( F " A ) ) : ( F " A ) -1-1-onto-> ( F " A )
23 f1of1 
 |-  ( ( _I |` ( F " A ) ) : ( F " A ) -1-1-onto-> ( F " A ) -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> ( F " A ) )
24 fimass 
 |-  ( F : A --> B -> ( F " A ) C_ B )
25 f1ss 
 |-  ( ( ( _I |` ( F " A ) ) : ( F " A ) -1-1-> ( F " A ) /\ ( F " A ) C_ B ) -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B )
26 24 25 sylan2 
 |-  ( ( ( _I |` ( F " A ) ) : ( F " A ) -1-1-> ( F " A ) /\ F : A --> B ) -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B )
27 26 ex 
 |-  ( ( _I |` ( F " A ) ) : ( F " A ) -1-1-> ( F " A ) -> ( F : A --> B -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
28 22 23 27 mp2b 
 |-  ( F : A --> B -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B )
29 28 adantr 
 |-  ( ( F : A --> B /\ A e. V ) -> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B )
30 18 21 29 3jca 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P /\ ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
31 12 adantr 
 |-  ( ( F : A --> B /\ A e. V ) -> F Fn A )
32 uniimaprimaeqfv 
 |-  ( ( F Fn A /\ a e. A ) -> U. ( F " ( `' F " { ( F ` a ) } ) ) = ( F ` a ) )
33 31 32 sylan 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> U. ( F " ( `' F " { ( F ` a ) } ) ) = ( F ` a ) )
34 33 fveq2d 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> ( ( _I |` ( F " A ) ) ` U. ( F " ( `' F " { ( F ` a ) } ) ) ) = ( ( _I |` ( F " A ) ) ` ( F ` a ) ) )
35 34 mpteq2dva 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( ( _I |` ( F " A ) ) ` U. ( F " ( `' F " { ( F ` a ) } ) ) ) ) = ( a e. A |-> ( ( _I |` ( F " A ) ) ` ( F ` a ) ) ) )
36 ffrn 
 |-  ( F : A --> B -> F : A --> ran F )
37 36 adantr 
 |-  ( ( F : A --> B /\ A e. V ) -> F : A --> ran F )
38 37 funfvima2d 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> ( F ` a ) e. ( F " A ) )
39 fvresi 
 |-  ( ( F ` a ) e. ( F " A ) -> ( ( _I |` ( F " A ) ) ` ( F ` a ) ) = ( F ` a ) )
40 38 39 syl 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> ( ( _I |` ( F " A ) ) ` ( F ` a ) ) = ( F ` a ) )
41 40 mpteq2dva 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( ( _I |` ( F " A ) ) ` ( F ` a ) ) ) = ( a e. A |-> ( F ` a ) ) )
42 35 41 eqtrd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( ( _I |` ( F " A ) ) ` U. ( F " ( `' F " { ( F ` a ) } ) ) ) ) = ( a e. A |-> ( F ` a ) ) )
43 12 ad2antrr 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> F Fn A )
44 2 adantr 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> A e. V )
45 simpr 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> a e. A )
46 1 preimafvelsetpreimafv 
 |-  ( ( F Fn A /\ A e. V /\ a e. A ) -> ( `' F " { ( F ` a ) } ) e. P )
47 43 44 45 46 syl3anc 
 |-  ( ( ( F : A --> B /\ A e. V ) /\ a e. A ) -> ( `' F " { ( F ` a ) } ) e. P )
48 eqidd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) )
49 eqidd 
 |-  ( ( F : A --> B /\ A e. V ) -> ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) = ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) )
50 imaeq2 
 |-  ( y = ( `' F " { ( F ` a ) } ) -> ( F " y ) = ( F " ( `' F " { ( F ` a ) } ) ) )
51 50 unieqd 
 |-  ( y = ( `' F " { ( F ` a ) } ) -> U. ( F " y ) = U. ( F " ( `' F " { ( F ` a ) } ) ) )
52 51 fveq2d 
 |-  ( y = ( `' F " { ( F ` a ) } ) -> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) = ( ( _I |` ( F " A ) ) ` U. ( F " ( `' F " { ( F ` a ) } ) ) ) )
53 47 48 49 52 fmptco 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) = ( a e. A |-> ( ( _I |` ( F " A ) ) ` U. ( F " ( `' F " { ( F ` a ) } ) ) ) ) )
54 dffn5 
 |-  ( F Fn A <-> F = ( a e. A |-> ( F ` a ) ) )
55 12 54 sylib 
 |-  ( F : A --> B -> F = ( a e. A |-> ( F ` a ) ) )
56 55 adantr 
 |-  ( ( F : A --> B /\ A e. V ) -> F = ( a e. A |-> ( F ` a ) ) )
57 42 53 56 3eqtr4rd 
 |-  ( ( F : A --> B /\ A e. V ) -> F = ( ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) )
58 f1of 
 |-  ( ( _I |` ( F " A ) ) : ( F " A ) -1-1-onto-> ( F " A ) -> ( _I |` ( F " A ) ) : ( F " A ) --> ( F " A ) )
59 22 58 mp1i 
 |-  ( F Fn A -> ( _I |` ( F " A ) ) : ( F " A ) --> ( F " A ) )
60 fnima 
 |-  ( F Fn A -> ( F " A ) = ran F )
61 60 eqcomd 
 |-  ( F Fn A -> ran F = ( F " A ) )
62 61 feq2d 
 |-  ( F Fn A -> ( ( _I |` ( F " A ) ) : ran F --> ( F " A ) <-> ( _I |` ( F " A ) ) : ( F " A ) --> ( F " A ) ) )
63 59 62 mpbird 
 |-  ( F Fn A -> ( _I |` ( F " A ) ) : ran F --> ( F " A ) )
64 1 uniimaelsetpreimafv 
 |-  ( ( F Fn A /\ y e. P ) -> U. ( F " y ) e. ran F )
65 63 64 cofmpt 
 |-  ( F Fn A -> ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) = ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) )
66 65 eqcomd 
 |-  ( F Fn A -> ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) = ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) )
67 31 66 syl 
 |-  ( ( F : A --> B /\ A e. V ) -> ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) = ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) )
68 67 coeq1d 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( y e. P |-> ( ( _I |` ( F " A ) ) ` U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) )
69 57 68 eqtrd 
 |-  ( ( F : A --> B /\ A e. V ) -> F = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) )
70 30 69 jca 
 |-  ( ( F : A --> B /\ A e. V ) -> ( ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P /\ ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) /\ F = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) ) )
71 foeq1 
 |-  ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) -> ( g : A -onto-> P <-> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P ) )
72 71 3ad2ant1 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( g : A -onto-> P <-> ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P ) )
73 f1oeq1 
 |-  ( h = ( y e. P |-> U. ( F " y ) ) -> ( h : P -1-1-onto-> ( F " A ) <-> ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) ) )
74 73 3ad2ant2 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( h : P -1-1-onto-> ( F " A ) <-> ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) ) )
75 f1eq1 
 |-  ( i = ( _I |` ( F " A ) ) -> ( i : ( F " A ) -1-1-> B <-> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
76 75 3ad2ant3 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( i : ( F " A ) -1-1-> B <-> ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) )
77 72 74 76 3anbi123d 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( ( g : A -onto-> P /\ h : P -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) <-> ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P /\ ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) ) )
78 simp3 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> i = ( _I |` ( F " A ) ) )
79 simp2 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> h = ( y e. P |-> U. ( F " y ) ) )
80 78 79 coeq12d 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( i o. h ) = ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) )
81 simp1 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) )
82 80 81 coeq12d 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( ( i o. h ) o. g ) = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) )
83 82 eqeq2d 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( F = ( ( i o. h ) o. g ) <-> F = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) ) )
84 77 83 anbi12d 
 |-  ( ( g = ( a e. A |-> ( `' F " { ( F ` a ) } ) ) /\ h = ( y e. P |-> U. ( F " y ) ) /\ i = ( _I |` ( F " A ) ) ) -> ( ( ( g : A -onto-> P /\ h : P -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) <-> ( ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P /\ ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) /\ F = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) ) ) )
85 84 spc3egv 
 |-  ( ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) e. _V /\ ( y e. P |-> U. ( F " y ) ) e. _V /\ ( _I |` ( F " A ) ) e. _V ) -> ( ( ( ( a e. A |-> ( `' F " { ( F ` a ) } ) ) : A -onto-> P /\ ( y e. P |-> U. ( F " y ) ) : P -1-1-onto-> ( F " A ) /\ ( _I |` ( F " A ) ) : ( F " A ) -1-1-> B ) /\ F = ( ( ( _I |` ( F " A ) ) o. ( y e. P |-> U. ( F " y ) ) ) o. ( a e. A |-> ( `' F " { ( F ` a ) } ) ) ) ) -> E. g E. h E. i ( ( g : A -onto-> P /\ h : P -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) ) )
86 11 70 85 sylc 
 |-  ( ( F : A --> B /\ A e. V ) -> E. g E. h E. i ( ( g : A -onto-> P /\ h : P -1-1-onto-> ( F " A ) /\ i : ( F " A ) -1-1-> B ) /\ F = ( ( i o. h ) o. g ) ) )