Theorem 2fcoidinvd

Description: Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	fcof1od.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcof1od.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
	fcof1od.a	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
	fcof1od.b	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
Assertion	2fcoidinvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		fcof1od.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcof1od.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3		fcof1od.a	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
4		fcof1od.b	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
5	1 2 3 4	fcof1od	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
6	5 2 4	fcof1oinvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )