Metamath Proof Explorer

Theorem fcof1o

Description: Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by AV, 15-Dec-2019)

		Ref	Expression
	Assertion	fcof1o	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = G)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to F : A ⟶ B$
2		simplr	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to G : B ⟶ A$
3		simprr	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to G \circ F = {I ↾}_{A}$
4		simprl	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to F \circ G = {I ↾}_{B}$
5	1 2 3 4	fcof1od	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to F : A \underset{1-1 onto}{⟶} B$
6	1 2 3 4	2fcoidinvd	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to F^{-1} = G$
7	5 6	jca	$⊢ ((F : A ⟶ B \land G : B ⟶ A) \land (F \circ G = {I ↾}_{B} \land G \circ F = {I ↾}_{A})) \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = G)$