This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 simplr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
3 simprr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
4 simprl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
5 1 2 3 4 fcof1od ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
6 1 2 3 4 2fcoidinvd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → ◡ 𝐹 = 𝐺 )
7 5 6 jca ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ◡ 𝐹 = 𝐺 ) )