Metamath Proof Explorer

Theorem k0004lem3

Description: When the value of a mapping on a singleton is known, the mapping is a completely known singleton. (Contributed by RP, 2-Apr-2021)

Ref Expression
Assertion k0004lem3 
|- ( ( A e. U /\ B e. V /\ C e. B ) -> ( ( F e. ( B ^m { A } ) /\ ( F ` A ) = C ) <-> F = { <. A , C >. } ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( ( F ` A ) = C -> { ( F ` A ) } = { C } )
2 eqimss 
 |-  ( { ( F ` A ) } = { C } -> { ( F ` A ) } C_ { C } )
3 1 2 syl 
 |-  ( ( F ` A ) = C -> { ( F ` A ) } C_ { C } )
4 fvex 
 |-  ( F ` A ) e. _V
5 4 snsssn 
 |-  ( { ( F ` A ) } C_ { C } -> ( F ` A ) = C )
6 3 5 impbii 
 |-  ( ( F ` A ) = C <-> { ( F ` A ) } C_ { C } )
7 elmapfn 
 |-  ( F e. ( B ^m { A } ) -> F Fn { A } )
8 simpl1 
 |-  ( ( ( A e. U /\ B e. V /\ C e. B ) /\ F e. ( B ^m { A } ) ) -> A e. U )
9 snidg 
 |-  ( A e. U -> A e. { A } )
10 8 9 syl 
 |-  ( ( ( A e. U /\ B e. V /\ C e. B ) /\ F e. ( B ^m { A } ) ) -> A e. { A } )
11 fnsnfv 
 |-  ( ( F Fn { A } /\ A e. { A } ) -> { ( F ` A ) } = ( F " { A } ) )
12 7 10 11 syl2an2 
 |-  ( ( ( A e. U /\ B e. V /\ C e. B ) /\ F e. ( B ^m { A } ) ) -> { ( F ` A ) } = ( F " { A } ) )
13 12 sseq1d 
 |-  ( ( ( A e. U /\ B e. V /\ C e. B ) /\ F e. ( B ^m { A } ) ) -> ( { ( F ` A ) } C_ { C } <-> ( F " { A } ) C_ { C } ) )
14 6 13 syl5bb 
 |-  ( ( ( A e. U /\ B e. V /\ C e. B ) /\ F e. ( B ^m { A } ) ) -> ( ( F ` A ) = C <-> ( F " { A } ) C_ { C } ) )
15 14 pm5.32da 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> ( ( F e. ( B ^m { A } ) /\ ( F ` A ) = C ) <-> ( F e. ( B ^m { A } ) /\ ( F " { A } ) C_ { C } ) ) )
16 snex 
 |-  { A } e. _V
17 simp2 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> B e. V )
18 simp3 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> C e. B )
19 18 snssd 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> { C } C_ B )
20 k0004lem2 
 |-  ( ( { A } e. _V /\ B e. V /\ { C } C_ B ) -> ( ( F e. ( B ^m { A } ) /\ ( F " { A } ) C_ { C } ) <-> F e. ( { C } ^m { A } ) ) )
21 16 17 19 20 mp3an2i 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> ( ( F e. ( B ^m { A } ) /\ ( F " { A } ) C_ { C } ) <-> F e. ( { C } ^m { A } ) ) )
22 snex 
 |-  { C } e. _V
23 22 16 elmap 
 |-  ( F e. ( { C } ^m { A } ) <-> F : { A } --> { C } )
24 fsng 
 |-  ( ( A e. U /\ C e. B ) -> ( F : { A } --> { C } <-> F = { <. A , C >. } ) )
25 24 3adant2 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> ( F : { A } --> { C } <-> F = { <. A , C >. } ) )
26 23 25 syl5bb 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> ( F e. ( { C } ^m { A } ) <-> F = { <. A , C >. } ) )
27 15 21 26 3bitrd 
 |-  ( ( A e. U /\ B e. V /\ C e. B ) -> ( ( F e. ( B ^m { A } ) /\ ( F ` A ) = C ) <-> F = { <. A , C >. } ) )