Metamath Proof Explorer

Theorem fsn2

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004)

Ref Expression
Hypothesis fsn2.1 
|- A e. _V
Assertion fsn2 
|- ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) )

Proof

Step Hyp Ref Expression
1 fsn2.1 
 |-  A e. _V
2 1 snid 
 |-  A e. { A }
3 ffvelcdm 
 |-  ( ( F : { A } --> B /\ A e. { A } ) -> ( F ` A ) e. B )
4 2 3 mpan2 
 |-  ( F : { A } --> B -> ( F ` A ) e. B )
5 ffn 
 |-  ( F : { A } --> B -> F Fn { A } )
6 dffn3 
 |-  ( F Fn { A } <-> F : { A } --> ran F )
7 6 biimpi 
 |-  ( F Fn { A } -> F : { A } --> ran F )
8 imadmrn 
 |-  ( F " dom F ) = ran F
9 fndm 
 |-  ( F Fn { A } -> dom F = { A } )
10 9 imaeq2d 
 |-  ( F Fn { A } -> ( F " dom F ) = ( F " { A } ) )
11 8 10 eqtr3id 
 |-  ( F Fn { A } -> ran F = ( F " { A } ) )
12 fnsnfv 
 |-  ( ( F Fn { A } /\ A e. { A } ) -> { ( F ` A ) } = ( F " { A } ) )
13 2 12 mpan2 
 |-  ( F Fn { A } -> { ( F ` A ) } = ( F " { A } ) )
14 11 13 eqtr4d 
 |-  ( F Fn { A } -> ran F = { ( F ` A ) } )
15 14 feq3d 
 |-  ( F Fn { A } -> ( F : { A } --> ran F <-> F : { A } --> { ( F ` A ) } ) )
16 7 15 mpbid 
 |-  ( F Fn { A } -> F : { A } --> { ( F ` A ) } )
17 5 16 syl 
 |-  ( F : { A } --> B -> F : { A } --> { ( F ` A ) } )
18 4 17 jca 
 |-  ( F : { A } --> B -> ( ( F ` A ) e. B /\ F : { A } --> { ( F ` A ) } ) )
19 snssi 
 |-  ( ( F ` A ) e. B -> { ( F ` A ) } C_ B )
20 fss 
 |-  ( ( F : { A } --> { ( F ` A ) } /\ { ( F ` A ) } C_ B ) -> F : { A } --> B )
21 20 ancoms 
 |-  ( ( { ( F ` A ) } C_ B /\ F : { A } --> { ( F ` A ) } ) -> F : { A } --> B )
22 19 21 sylan 
 |-  ( ( ( F ` A ) e. B /\ F : { A } --> { ( F ` A ) } ) -> F : { A } --> B )
23 18 22 impbii 
 |-  ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F : { A } --> { ( F ` A ) } ) )
24 fvex 
 |-  ( F ` A ) e. _V
25 1 24 fsn 
 |-  ( F : { A } --> { ( F ` A ) } <-> F = { <. A , ( F ` A ) >. } )
26 25 anbi2i 
 |-  ( ( ( F ` A ) e. B /\ F : { A } --> { ( F ` A ) } ) <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) )
27 23 26 bitri 
 |-  ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) )