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	$$⊢\phi \to F:A⟶B$$
	2fvcoidd.g	$$⊢\phi \to G:B⟶A$$
	2fvcoidd.i	$$⊢\phi \to \forall a\in AG\left(F\left(a\right)\right)=a$$
Assertion	2fvcoidd	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		2fvcoidd.f	$$⊢\phi \to F:A⟶B$$
2		2fvcoidd.g	$$⊢\phi \to G:B⟶A$$
3		2fvcoidd.i	$$⊢\phi \to \forall a\in AG\left(F\left(a\right)\right)=a$$
4		fcompt	$$⊢\left(G:B⟶A\wedge F:A⟶B\right)\to G\circ F=\left(x\in A⟼G\left(F\left(x\right)\right)\right)$$
5	2 1 4	syl2anc	$$⊢\phi \to G\circ F=\left(x\in A⟼G\left(F\left(x\right)\right)\right)$$
6		2fveq3	$$⊢a=x\to G\left(F\left(a\right)\right)=G\left(F\left(x\right)\right)$$
7		id	$$⊢a=x\to a=x$$
8	6 7	eqeq12d	$$⊢a=x\to \left(G\left(F\left(a\right)\right)=a\leftrightarrow G\left(F\left(x\right)\right)=x\right)$$
9	8	rspccv	$$⊢\forall a\in AG\left(F\left(a\right)\right)=a\to \left(x\in A\to G\left(F\left(x\right)\right)=x\right)$$
10	3 9	syl	$$⊢\phi \to \left(x\in A\to G\left(F\left(x\right)\right)=x\right)$$
11	10	imp	$$⊢\left(\phi \wedge x\in A\right)\to G\left(F\left(x\right)\right)=x$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in A⟼G\left(F\left(x\right)\right)\right)=\left(x\in A⟼x\right)$$
13		mptresid	$$⊢{\mathrm{I}\upharpoonright }_A=\left(x\in A⟼x\right)$$
14	12 13	eqtr4di	$$⊢\phi \to \left(x\in A⟼G\left(F\left(x\right)\right)\right)={\mathrm{I}\upharpoonright }_A$$
15	5 14	eqtrd	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$