Theorem f1ocnv

Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
3		fneq1	⊢ ( ◡ ◡ 𝐹 = 𝐹 → ( ◡ ◡ 𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) )
4	3	biimprd	⊢ ( ◡ ◡ 𝐹 = 𝐹 → ( 𝐹 Fn 𝐴 → ◡ ◡ 𝐹 Fn 𝐴 ) )
5	2 4	sylbi	⊢ ( Rel 𝐹 → ( 𝐹 Fn 𝐴 → ◡ ◡ 𝐹 Fn 𝐴 ) )
6	1 5	mpcom	⊢ ( 𝐹 Fn 𝐴 → ◡ ◡ 𝐹 Fn 𝐴 )
7	6	anim1ci	⊢ ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) → ( ◡ 𝐹 Fn 𝐵 ∧ ◡ ◡ 𝐹 Fn 𝐴 ) )
8		dff1o4	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
9		dff1o4	⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 ↔ ( ◡ 𝐹 Fn 𝐵 ∧ ◡ ◡ 𝐹 Fn 𝐴 ) )
10	7 8 9	3imtr4i	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )