Theorem 2fvidinvd

Description: Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-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	2fvidinvd	|- ( ph -> `' F = G )

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	2fcoidinvd	|- ( ph -> `' F = G )