This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcof1od

Description: A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 and fcofo . Formerly part of proof of fcof1o . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses fcof1od.f 
|- ( ph -> F : A --> B )
fcof1od.g 
|- ( ph -> G : B --> A )
fcof1od.a 
|- ( ph -> ( G o. F ) = ( _I |` A ) )
fcof1od.b 
|- ( ph -> ( F o. G ) = ( _I |` B ) )
Assertion fcof1od 
|- ( ph -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 fcof1od.f 
 |-  ( ph -> F : A --> B )
2 fcof1od.g 
 |-  ( ph -> G : B --> A )
3 fcof1od.a 
 |-  ( ph -> ( G o. F ) = ( _I |` A ) )
4 fcof1od.b 
 |-  ( ph -> ( F o. G ) = ( _I |` B ) )
5 fcof1 
 |-  ( ( F : A --> B /\ ( G o. F ) = ( _I |` A ) ) -> F : A -1-1-> B )
6 1 3 5 syl2anc 
 |-  ( ph -> F : A -1-1-> B )
7 fcofo 
 |-  ( ( F : A --> B /\ G : B --> A /\ ( F o. G ) = ( _I |` B ) ) -> F : A -onto-> B )
8 1 2 4 7 syl3anc 
 |-  ( ph -> F : A -onto-> B )
9 df-f1o 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
10 6 8 9 sylanbrc 
 |-  ( ph -> F : A -1-1-onto-> B )