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