Metamath Proof Explorer


Theorem f1cnv

Description: The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011)

Ref Expression
Assertion f1cnv ( 𝐹 : 𝐴1-1𝐵 𝐹 : ran 𝐹1-1-onto𝐴 )

Proof

Step Hyp Ref Expression
1 f1f1orn ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto→ ran 𝐹 )
2 f1ocnv ( 𝐹 : 𝐴1-1-onto→ ran 𝐹 𝐹 : ran 𝐹1-1-onto𝐴 )
3 1 2 syl ( 𝐹 : 𝐴1-1𝐵 𝐹 : ran 𝐹1-1-onto𝐴 )