Metamath Proof Explorer

Theorem focofo

Description: Composition of onto functions. Generalisation of foco . (Contributed by AV, 29-Sep-2024)

Ref Expression
Assertion focofo 
|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ( F o. G ) : ( `' G " A ) -onto-> B )

Proof

Step Hyp Ref Expression
1 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
2 fcof 
 |-  ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )
3 1 2 sylan 
 |-  ( ( F : A -onto-> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )
4 3 3adant3 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ( F o. G ) : ( `' G " A ) --> B )
5 rnco 
 |-  ran ( F o. G ) = ran ( F |` ran G )
6 1 freld 
 |-  ( F : A -onto-> B -> Rel F )
7 6 3ad2ant1 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> Rel F )
8 fdm 
 |-  ( F : A --> B -> dom F = A )
9 8 eqcomd 
 |-  ( F : A --> B -> A = dom F )
10 1 9 syl 
 |-  ( F : A -onto-> B -> A = dom F )
11 10 sseq1d 
 |-  ( F : A -onto-> B -> ( A C_ ran G <-> dom F C_ ran G ) )
12 11 biimpa 
 |-  ( ( F : A -onto-> B /\ A C_ ran G ) -> dom F C_ ran G )
13 relssres 
 |-  ( ( Rel F /\ dom F C_ ran G ) -> ( F |` ran G ) = F )
14 13 rneqd 
 |-  ( ( Rel F /\ dom F C_ ran G ) -> ran ( F |` ran G ) = ran F )
15 7 12 14 3imp3i2an 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F |` ran G ) = ran F )
16 forn 
 |-  ( F : A -onto-> B -> ran F = B )
17 16 3ad2ant1 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran F = B )
18 15 17 eqtrd 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F |` ran G ) = B )
19 5 18 eqtrid 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F o. G ) = B )
20 dffo2 
 |-  ( ( F o. G ) : ( `' G " A ) -onto-> B <-> ( ( F o. G ) : ( `' G " A ) --> B /\ ran ( F o. G ) = B ) )
21 4 19 20 sylanbrc 
 |-  ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ( F o. G ) : ( `' G " A ) -onto-> B )