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

Metamath Proof Explorer

Theorem 2fvcoidd

Description: Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first 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 )
Assertion 2fvcoidd 
|- ( ph -> ( G o. F ) = ( _I |` A ) )

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 fcompt 
 |-  ( ( G : B --> A /\ F : A --> B ) -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )
5 2 1 4 syl2anc 
 |-  ( ph -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )
6 2fveq3 
 |-  ( a = x -> ( G ` ( F ` a ) ) = ( G ` ( F ` x ) ) )
7 id 
 |-  ( a = x -> a = x )
8 6 7 eqeq12d 
 |-  ( a = x -> ( ( G ` ( F ` a ) ) = a <-> ( G ` ( F ` x ) ) = x ) )
9 8 rspccv 
 |-  ( A. a e. A ( G ` ( F ` a ) ) = a -> ( x e. A -> ( G ` ( F ` x ) ) = x ) )
10 3 9 syl 
 |-  ( ph -> ( x e. A -> ( G ` ( F ` x ) ) = x ) )
11 10 imp 
 |-  ( ( ph /\ x e. A ) -> ( G ` ( F ` x ) ) = x )
12 11 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( G ` ( F ` x ) ) ) = ( x e. A |-> x ) )
13 mptresid 
 |-  ( _I |` A ) = ( x e. A |-> x )
14 12 13 eqtr4di 
 |-  ( ph -> ( x e. A |-> ( G ` ( F ` x ) ) ) = ( _I |` A ) )
15 5 14 eqtrd 
 |-  ( ph -> ( G o. F ) = ( _I |` A ) )