Metamath Proof Explorer


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 )