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 )