Theorem fcof1oinvd

Description: Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	fcof1oinvd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
	fcof1oinvd.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
	fcof1oinvd.b	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
Assertion	fcof1oinvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		fcof1oinvd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2		fcof1oinvd.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3		fcof1oinvd.b	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
4	3	coeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ◡ 𝐹 ∘ ( I ↾ 𝐵 ) ) )
5		coass	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) )
6		f1ococnv1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
7	1 6	syl	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
8	7	coeq1d	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( I ↾ 𝐴 ) ∘ 𝐺 ) )
9		fcoi2	⊢ ( 𝐺 : 𝐵 ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
10	2 9	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
11	8 10	eqtrd	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = 𝐺 )
12	5 11	eqtr3id	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) = 𝐺 )
13		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
14	1 13	syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
15		f1of	⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
16	14 15	syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
17		fcoi1	⊢ ( ◡ 𝐹 : 𝐵 ⟶ 𝐴 → ( ◡ 𝐹 ∘ ( I ↾ 𝐵 ) ) = ◡ 𝐹 )
18	16 17	syl	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( I ↾ 𝐵 ) ) = ◡ 𝐹 )
19	4 12 18	3eqtr3rd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )