Theorem f1ococnv1

Description: The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003)

	Ref	Expression
Assertion	f1ococnv1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		f1orel	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐹 )
2		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
3	1 2	sylib	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ ◡ 𝐹 = 𝐹 )
4	3	coeq2d	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ ◡ ◡ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
5		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
6		f1ococnv2	⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ( ◡ 𝐹 ∘ ◡ ◡ 𝐹 ) = ( I ↾ 𝐴 ) )
7	5 6	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ ◡ ◡ 𝐹 ) = ( I ↾ 𝐴 ) )
8	4 7	eqtr3d	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )