Metamath Proof Explorer

Theorem f1ocoima

Description: The composition of two bijections as bijection onto the image of the range of the first bijection. (Contributed by AV, 15-Aug-2025)

Ref Expression
Assertion f1ocoima 
|- ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( G o. F ) : A -1-1-onto-> ( G " B ) )

Proof

Step Hyp Ref Expression
1 f1of1 
 |-  ( G : C -1-1-onto-> D -> G : C -1-1-> D )
2 1 anim1i 
 |-  ( ( G : C -1-1-onto-> D /\ B C_ C ) -> ( G : C -1-1-> D /\ B C_ C ) )
3 2 3adant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( G : C -1-1-> D /\ B C_ C ) )
4 f1ores 
 |-  ( ( G : C -1-1-> D /\ B C_ C ) -> ( G |` B ) : B -1-1-onto-> ( G " B ) )
5 3 4 syl 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( G |` B ) : B -1-1-onto-> ( G " B ) )
6 simp1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> F : A -1-1-onto-> B )
7 f1oco 
 |-  ( ( ( G |` B ) : B -1-1-onto-> ( G " B ) /\ F : A -1-1-onto-> B ) -> ( ( G |` B ) o. F ) : A -1-1-onto-> ( G " B ) )
8 5 6 7 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( ( G |` B ) o. F ) : A -1-1-onto-> ( G " B ) )
9 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
10 forn 
 |-  ( F : A -onto-> B -> ran F = B )
11 9 10 syl 
 |-  ( F : A -1-1-onto-> B -> ran F = B )
12 11 eqimssd 
 |-  ( F : A -1-1-onto-> B -> ran F C_ B )
13 12 3ad2ant1 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ran F C_ B )
14 cores 
 |-  ( ran F C_ B -> ( ( G |` B ) o. F ) = ( G o. F ) )
15 14 eqcomd 
 |-  ( ran F C_ B -> ( G o. F ) = ( ( G |` B ) o. F ) )
16 13 15 syl 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( G o. F ) = ( ( G |` B ) o. F ) )
17 16 f1oeq1d 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( ( G o. F ) : A -1-1-onto-> ( G " B ) <-> ( ( G |` B ) o. F ) : A -1-1-onto-> ( G " B ) ) )
18 8 17 mpbird 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D /\ B C_ C ) -> ( G o. F ) : A -1-1-onto-> ( G " B ) )