Theorem 2fvidf1od

Description: A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	2fvcoidd.f	|- ( ph -> F : A --> B )
	2fvcoidd.g	|- ( ph -> G : B --> A )
	2fvcoidd.i	|- ( ph -> A. a e. A ( G ` ( F ` a ) ) = a )
	2fvidf1od.i	|- ( ph -> A. b e. B ( F ` ( G ` b ) ) = b )
Assertion	2fvidf1od	|- ( ph -> F : A -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		2fvcoidd.f	|- ( ph -> F : A --> B )
2		2fvcoidd.g	|- ( ph -> G : B --> A )
3		2fvcoidd.i	|- ( ph -> A. a e. A ( G ` ( F ` a ) ) = a )
4		2fvidf1od.i	|- ( ph -> A. b e. B ( F ` ( G ` b ) ) = b )
5	1 2 3	2fvcoidd	|- ( ph -> ( G o. F ) = ( _I |` A ) )
6	2 1 4	2fvcoidd	|- ( ph -> ( F o. G ) = ( _I |` B ) )
7	1 2 5 6	fcof1od	|- ( ph -> F : A -1-1-onto-> B )