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 ) )