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 ffvelrn
 |-  ( ( 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 ) >. } ) )