Theorem f1ocnvb

Description: A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and codomain/range interchanged. (Contributed by NM, 8-Dec-2003)

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

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
2		f1ocnv	⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
3		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
4		f1oeq1	⊢ ( ◡ ◡ 𝐹 = 𝐹 → ( ◡ ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
5	3 4	sylbi	⊢ ( Rel 𝐹 → ( ◡ ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
6	2 5	imbitrid	⊢ ( Rel 𝐹 → ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
7	1 6	impbid2	⊢ ( Rel 𝐹 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 ) )