Metamath Proof Explorer

Theorem funfocofob

Description: If the domain of a function G is a subset of the range of a function F , then the composition ( G o. F ) is surjective iff G is surjective. (Contributed by GL and AV, 29-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 fdmrn 
 |-  ( Fun F <-> F : dom F --> ran F )
2 1 biimpi 
 |-  ( Fun F -> F : dom F --> ran F )
3 2 3ad2ant1 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> F : dom F --> ran F )
4 3 adantr 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ ( G o. F ) : ( `' F " A ) -onto-> B ) -> F : dom F --> ran F )
5 eqid 
 |-  ( ran F i^i A ) = ( ran F i^i A )
6 eqid 
 |-  ( `' F " A ) = ( `' F " A )
7 eqid 
 |-  ( F |` ( `' F " A ) ) = ( F |` ( `' F " A ) )
8 simp2 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> G : A --> B )
9 8 adantr 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ ( G o. F ) : ( `' F " A ) -onto-> B ) -> G : A --> B )
10 eqid 
 |-  ( G |` ( ran F i^i A ) ) = ( G |` ( ran F i^i A ) )
11 simpr 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ ( G o. F ) : ( `' F " A ) -onto-> B ) -> ( G o. F ) : ( `' F " A ) -onto-> B )
12 4 5 6 7 9 10 11 fcoresfo 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ ( G o. F ) : ( `' F " A ) -onto-> B ) -> ( G |` ( ran F i^i A ) ) : ( ran F i^i A ) -onto-> B )
13 12 ex 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ( G o. F ) : ( `' F " A ) -onto-> B -> ( G |` ( ran F i^i A ) ) : ( ran F i^i A ) -onto-> B ) )
14 sseqin2 
 |-  ( A C_ ran F <-> ( ran F i^i A ) = A )
15 14 biimpi 
 |-  ( A C_ ran F -> ( ran F i^i A ) = A )
16 15 3ad2ant3 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ran F i^i A ) = A )
17 8 fdmd 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> dom G = A )
18 16 17 eqtr4d 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ran F i^i A ) = dom G )
19 18 reseq2d 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( G |` ( ran F i^i A ) ) = ( G |` dom G ) )
20 8 freld 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> Rel G )
21 resdm 
 |-  ( Rel G -> ( G |` dom G ) = G )
22 20 21 syl 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( G |` dom G ) = G )
23 19 22 eqtrd 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( G |` ( ran F i^i A ) ) = G )
24 eqidd 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> B = B )
25 23 16 24 foeq123d 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ( G |` ( ran F i^i A ) ) : ( ran F i^i A ) -onto-> B <-> G : A -onto-> B ) )
26 13 25 sylibd 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ( G o. F ) : ( `' F " A ) -onto-> B -> G : A -onto-> B ) )
27 simpr 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ G : A -onto-> B ) -> G : A -onto-> B )
28 simpl1 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ G : A -onto-> B ) -> Fun F )
29 simpl3 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ G : A -onto-> B ) -> A C_ ran F )
30 focofo 
 |-  ( ( G : A -onto-> B /\ Fun F /\ A C_ ran F ) -> ( G o. F ) : ( `' F " A ) -onto-> B )
31 27 28 29 30 syl3anc 
 |-  ( ( ( Fun F /\ G : A --> B /\ A C_ ran F ) /\ G : A -onto-> B ) -> ( G o. F ) : ( `' F " A ) -onto-> B )
32 31 ex 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( G : A -onto-> B -> ( G o. F ) : ( `' F " A ) -onto-> B ) )
33 26 32 impbid 
 |-  ( ( Fun F /\ G : A --> B /\ A C_ ran F ) -> ( ( G o. F ) : ( `' F " A ) -onto-> B <-> G : A -onto-> B ) )