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→ 𝐵 ∧ ◡ 𝐹 = 𝐺 ) )