Metamath Proof Explorer

Theorem f1osng

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( a = A -> { a } = { A } )
2 1 f1oeq2d 
 |-  ( a = A -> ( { <. a , b >. } : { a } -1-1-onto-> { b } <-> { <. a , b >. } : { A } -1-1-onto-> { b } ) )
3 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
4 3 sneqd 
 |-  ( a = A -> { <. a , b >. } = { <. A , b >. } )
5 f1oeq1 
 |-  ( { <. a , b >. } = { <. A , b >. } -> ( { <. a , b >. } : { A } -1-1-onto-> { b } <-> { <. A , b >. } : { A } -1-1-onto-> { b } ) )
6 4 5 syl 
 |-  ( a = A -> ( { <. a , b >. } : { A } -1-1-onto-> { b } <-> { <. A , b >. } : { A } -1-1-onto-> { b } ) )
7 2 6 bitrd 
 |-  ( a = A -> ( { <. a , b >. } : { a } -1-1-onto-> { b } <-> { <. A , b >. } : { A } -1-1-onto-> { b } ) )
8 sneq 
 |-  ( b = B -> { b } = { B } )
9 8 f1oeq3d 
 |-  ( b = B -> ( { <. A , b >. } : { A } -1-1-onto-> { b } <-> { <. A , b >. } : { A } -1-1-onto-> { B } ) )
10 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
11 10 sneqd 
 |-  ( b = B -> { <. A , b >. } = { <. A , B >. } )
12 f1oeq1 
 |-  ( { <. A , b >. } = { <. A , B >. } -> ( { <. A , b >. } : { A } -1-1-onto-> { B } <-> { <. A , B >. } : { A } -1-1-onto-> { B } ) )
13 11 12 syl 
 |-  ( b = B -> ( { <. A , b >. } : { A } -1-1-onto-> { B } <-> { <. A , B >. } : { A } -1-1-onto-> { B } ) )
14 9 13 bitrd 
 |-  ( b = B -> ( { <. A , b >. } : { A } -1-1-onto-> { b } <-> { <. A , B >. } : { A } -1-1-onto-> { B } ) )
15 vex 
 |-  a e. _V
16 vex 
 |-  b e. _V
17 15 16 f1osn 
 |-  { <. a , b >. } : { a } -1-1-onto-> { b }
18 7 14 17 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-onto-> { B } )