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 ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F : A ⟶ 1-1 onto B ∧ F -1 = G

Proof

Step Hyp Ref Expression
1 simpll ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F : A ⟶ B
2 simplr ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → G : B ⟶ A
3 simprr ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → G ∘ F = I ↾ A
4 simprl ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F ∘ G = I ↾ B
5 1 2 3 4 fcof1od ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F : A ⟶ 1-1 onto B
6 1 2 3 4 2fcoidinvd ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F -1 = G
7 5 6 jca ⊢ F : A ⟶ B ∧ G : B ⟶ A ∧ F ∘ G = I ↾ B ∧ G ∘ F = I ↾ A → F : A ⟶ 1-1 onto B ∧ F -1 = G