Metamath Proof Explorer


Theorem mapsnd

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses mapsnd.1
|- ( ph -> A e. V )
mapsnd.2
|- ( ph -> B e. W )
Assertion mapsnd
|- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )

Proof

Step Hyp Ref Expression
1 mapsnd.1
 |-  ( ph -> A e. V )
2 mapsnd.2
 |-  ( ph -> B e. W )
3 snex
 |-  { B } e. _V
4 3 a1i
 |-  ( ph -> { B } e. _V )
5 1 4 elmapd
 |-  ( ph -> ( f e. ( A ^m { B } ) <-> f : { B } --> A ) )
6 ffn
 |-  ( f : { B } --> A -> f Fn { B } )
7 snidg
 |-  ( B e. W -> B e. { B } )
8 2 7 syl
 |-  ( ph -> B e. { B } )
9 fneu
 |-  ( ( f Fn { B } /\ B e. { B } ) -> E! y B f y )
10 6 8 9 syl2anr
 |-  ( ( ph /\ f : { B } --> A ) -> E! y B f y )
11 euabsn
 |-  ( E! y B f y <-> E. y { y | B f y } = { y } )
12 frel
 |-  ( f : { B } --> A -> Rel f )
13 relimasn
 |-  ( Rel f -> ( f " { B } ) = { y | B f y } )
14 12 13 syl
 |-  ( f : { B } --> A -> ( f " { B } ) = { y | B f y } )
15 fdm
 |-  ( f : { B } --> A -> dom f = { B } )
16 15 imaeq2d
 |-  ( f : { B } --> A -> ( f " dom f ) = ( f " { B } ) )
17 imadmrn
 |-  ( f " dom f ) = ran f
18 16 17 eqtr3di
 |-  ( f : { B } --> A -> ( f " { B } ) = ran f )
19 14 18 eqtr3d
 |-  ( f : { B } --> A -> { y | B f y } = ran f )
20 19 eqeq1d
 |-  ( f : { B } --> A -> ( { y | B f y } = { y } <-> ran f = { y } ) )
21 20 exbidv
 |-  ( f : { B } --> A -> ( E. y { y | B f y } = { y } <-> E. y ran f = { y } ) )
22 11 21 syl5bb
 |-  ( f : { B } --> A -> ( E! y B f y <-> E. y ran f = { y } ) )
23 22 adantl
 |-  ( ( ph /\ f : { B } --> A ) -> ( E! y B f y <-> E. y ran f = { y } ) )
24 10 23 mpbid
 |-  ( ( ph /\ f : { B } --> A ) -> E. y ran f = { y } )
25 frn
 |-  ( f : { B } --> A -> ran f C_ A )
26 25 sseld
 |-  ( f : { B } --> A -> ( y e. ran f -> y e. A ) )
27 vsnid
 |-  y e. { y }
28 eleq2
 |-  ( ran f = { y } -> ( y e. ran f <-> y e. { y } ) )
29 27 28 mpbiri
 |-  ( ran f = { y } -> y e. ran f )
30 26 29 impel
 |-  ( ( f : { B } --> A /\ ran f = { y } ) -> y e. A )
31 30 adantll
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> y e. A )
32 ffrn
 |-  ( f : { B } --> A -> f : { B } --> ran f )
33 feq3
 |-  ( ran f = { y } -> ( f : { B } --> ran f <-> f : { B } --> { y } ) )
34 32 33 syl5ibcom
 |-  ( f : { B } --> A -> ( ran f = { y } -> f : { B } --> { y } ) )
35 34 imp
 |-  ( ( f : { B } --> A /\ ran f = { y } ) -> f : { B } --> { y } )
36 35 adantll
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> f : { B } --> { y } )
37 2 ad2antrr
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> B e. W )
38 vex
 |-  y e. _V
39 fsng
 |-  ( ( B e. W /\ y e. _V ) -> ( f : { B } --> { y } <-> f = { <. B , y >. } ) )
40 37 38 39 sylancl
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> ( f : { B } --> { y } <-> f = { <. B , y >. } ) )
41 36 40 mpbid
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> f = { <. B , y >. } )
42 31 41 jca
 |-  ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> ( y e. A /\ f = { <. B , y >. } ) )
43 42 ex
 |-  ( ( ph /\ f : { B } --> A ) -> ( ran f = { y } -> ( y e. A /\ f = { <. B , y >. } ) ) )
44 43 eximdv
 |-  ( ( ph /\ f : { B } --> A ) -> ( E. y ran f = { y } -> E. y ( y e. A /\ f = { <. B , y >. } ) ) )
45 24 44 mpd
 |-  ( ( ph /\ f : { B } --> A ) -> E. y ( y e. A /\ f = { <. B , y >. } ) )
46 df-rex
 |-  ( E. y e. A f = { <. B , y >. } <-> E. y ( y e. A /\ f = { <. B , y >. } ) )
47 45 46 sylibr
 |-  ( ( ph /\ f : { B } --> A ) -> E. y e. A f = { <. B , y >. } )
48 47 ex
 |-  ( ph -> ( f : { B } --> A -> E. y e. A f = { <. B , y >. } ) )
49 f1osng
 |-  ( ( B e. W /\ y e. _V ) -> { <. B , y >. } : { B } -1-1-onto-> { y } )
50 2 38 49 sylancl
 |-  ( ph -> { <. B , y >. } : { B } -1-1-onto-> { y } )
51 50 adantr
 |-  ( ( ph /\ f = { <. B , y >. } ) -> { <. B , y >. } : { B } -1-1-onto-> { y } )
52 f1oeq1
 |-  ( f = { <. B , y >. } -> ( f : { B } -1-1-onto-> { y } <-> { <. B , y >. } : { B } -1-1-onto-> { y } ) )
53 52 bicomd
 |-  ( f = { <. B , y >. } -> ( { <. B , y >. } : { B } -1-1-onto-> { y } <-> f : { B } -1-1-onto-> { y } ) )
54 53 adantl
 |-  ( ( ph /\ f = { <. B , y >. } ) -> ( { <. B , y >. } : { B } -1-1-onto-> { y } <-> f : { B } -1-1-onto-> { y } ) )
55 51 54 mpbid
 |-  ( ( ph /\ f = { <. B , y >. } ) -> f : { B } -1-1-onto-> { y } )
56 f1of
 |-  ( f : { B } -1-1-onto-> { y } -> f : { B } --> { y } )
57 55 56 syl
 |-  ( ( ph /\ f = { <. B , y >. } ) -> f : { B } --> { y } )
58 57 3adant2
 |-  ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> { y } )
59 snssi
 |-  ( y e. A -> { y } C_ A )
60 59 3ad2ant2
 |-  ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> { y } C_ A )
61 58 60 fssd
 |-  ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> A )
62 61 rexlimdv3a
 |-  ( ph -> ( E. y e. A f = { <. B , y >. } -> f : { B } --> A ) )
63 48 62 impbid
 |-  ( ph -> ( f : { B } --> A <-> E. y e. A f = { <. B , y >. } ) )
64 5 63 bitrd
 |-  ( ph -> ( f e. ( A ^m { B } ) <-> E. y e. A f = { <. B , y >. } ) )
65 64 abbi2dv
 |-  ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )