This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1sng

Description: A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021)

Ref Expression
Assertion f1sng 
|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> W )

Proof

Step Hyp Ref Expression
1 f1osng 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-onto-> { B } )
2 f1of1 
 |-  ( { <. A , B >. } : { A } -1-1-onto-> { B } -> { <. A , B >. } : { A } -1-1-> { B } )
3 1 2 syl 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> { B } )
4 snssi 
 |-  ( B e. W -> { B } C_ W )
5 4 adantl 
 |-  ( ( A e. V /\ B e. W ) -> { B } C_ W )
6 f1ss 
 |-  ( ( { <. A , B >. } : { A } -1-1-> { B } /\ { B } C_ W ) -> { <. A , B >. } : { A } -1-1-> W )
7 3 5 6 syl2anc 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> W )