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	$$⊢\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$$
	2fvidf1od.i	$$⊢\phi \to \forall b\in BF\left(G\left(b\right)\right)=b$$
Assertion	2fvidinvd	$$⊢\phi \to F^{-1}=G$$

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		2fvidf1od.i	$$⊢\phi \to \forall b\in BF\left(G\left(b\right)\right)=b$$
5	1 2 3	2fvcoidd	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
6	2 1 4	2fvcoidd	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
7	1 2 5 6	2fcoidinvd	$$⊢\phi \to F^{-1}=G$$