Metamath Proof Explorer

Theorem mapsnend

Description: Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of Mendelson p. 255. (Contributed by NM, 17-Dec-2003) (Revised by Mario Carneiro, 15-Nov-2014) (Revised by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses mapsnend.a 
|- ( ph -> A e. V )
mapsnend.b 
|- ( ph -> B e. W )
Assertion mapsnend 
|- ( ph -> ( A ^m { B } ) ~~ A )

Proof

Step Hyp Ref Expression
1 mapsnend.a 
 |-  ( ph -> A e. V )
2 mapsnend.b 
 |-  ( ph -> B e. W )
3 ovexd 
 |-  ( ph -> ( A ^m { B } ) e. _V )
4 fvexd 
 |-  ( z e. ( A ^m { B } ) -> ( z ` B ) e. _V )
5 4 a1i 
 |-  ( ph -> ( z e. ( A ^m { B } ) -> ( z ` B ) e. _V ) )
6 snex 
 |-  { <. B , w >. } e. _V
7 6 2a1i 
 |-  ( ph -> ( w e. A -> { <. B , w >. } e. _V ) )
8 1 2 mapsnd 
 |-  ( ph -> ( A ^m { B } ) = { z | E. y e. A z = { <. B , y >. } } )
9 8 abeq2d 
 |-  ( ph -> ( z e. ( A ^m { B } ) <-> E. y e. A z = { <. B , y >. } ) )
10 9 anbi1d 
 |-  ( ph -> ( ( z e. ( A ^m { B } ) /\ w = ( z ` B ) ) <-> ( E. y e. A z = { <. B , y >. } /\ w = ( z ` B ) ) ) )
11 r19.41v 
 |-  ( E. y e. A ( z = { <. B , y >. } /\ w = ( z ` B ) ) <-> ( E. y e. A z = { <. B , y >. } /\ w = ( z ` B ) ) )
12 11 bicomi 
 |-  ( ( E. y e. A z = { <. B , y >. } /\ w = ( z ` B ) ) <-> E. y e. A ( z = { <. B , y >. } /\ w = ( z ` B ) ) )
13 12 a1i 
 |-  ( ph -> ( ( E. y e. A z = { <. B , y >. } /\ w = ( z ` B ) ) <-> E. y e. A ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) )
14 df-rex 
 |-  ( E. y e. A ( z = { <. B , y >. } /\ w = ( z ` B ) ) <-> E. y ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) )
15 14 a1i 
 |-  ( ph -> ( E. y e. A ( z = { <. B , y >. } /\ w = ( z ` B ) ) <-> E. y ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) ) )
16 10 13 15 3bitrd 
 |-  ( ph -> ( ( z e. ( A ^m { B } ) /\ w = ( z ` B ) ) <-> E. y ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) ) )
17 fveq1 
 |-  ( z = { <. B , y >. } -> ( z ` B ) = ( { <. B , y >. } ` B ) )
18 vex 
 |-  y e. _V
19 fvsng 
 |-  ( ( B e. W /\ y e. _V ) -> ( { <. B , y >. } ` B ) = y )
20 2 18 19 sylancl 
 |-  ( ph -> ( { <. B , y >. } ` B ) = y )
21 17 20 sylan9eqr 
 |-  ( ( ph /\ z = { <. B , y >. } ) -> ( z ` B ) = y )
22 21 eqeq2d 
 |-  ( ( ph /\ z = { <. B , y >. } ) -> ( w = ( z ` B ) <-> w = y ) )
23 equcom 
 |-  ( w = y <-> y = w )
24 22 23 bitrdi 
 |-  ( ( ph /\ z = { <. B , y >. } ) -> ( w = ( z ` B ) <-> y = w ) )
25 24 pm5.32da 
 |-  ( ph -> ( ( z = { <. B , y >. } /\ w = ( z ` B ) ) <-> ( z = { <. B , y >. } /\ y = w ) ) )
26 25 anbi2d 
 |-  ( ph -> ( ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) <-> ( y e. A /\ ( z = { <. B , y >. } /\ y = w ) ) ) )
27 anass 
 |-  ( ( ( y e. A /\ z = { <. B , y >. } ) /\ y = w ) <-> ( y e. A /\ ( z = { <. B , y >. } /\ y = w ) ) )
28 27 a1i 
 |-  ( ph -> ( ( ( y e. A /\ z = { <. B , y >. } ) /\ y = w ) <-> ( y e. A /\ ( z = { <. B , y >. } /\ y = w ) ) ) )
29 ancom 
 |-  ( ( ( y e. A /\ z = { <. B , y >. } ) /\ y = w ) <-> ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) )
30 29 a1i 
 |-  ( ph -> ( ( ( y e. A /\ z = { <. B , y >. } ) /\ y = w ) <-> ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) ) )
31 26 28 30 3bitr2d 
 |-  ( ph -> ( ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) <-> ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) ) )
32 31 exbidv 
 |-  ( ph -> ( E. y ( y e. A /\ ( z = { <. B , y >. } /\ w = ( z ` B ) ) ) <-> E. y ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) ) )
33 eleq1w 
 |-  ( y = w -> ( y e. A <-> w e. A ) )
34 opeq2 
 |-  ( y = w -> <. B , y >. = <. B , w >. )
35 34 sneqd 
 |-  ( y = w -> { <. B , y >. } = { <. B , w >. } )
36 35 eqeq2d 
 |-  ( y = w -> ( z = { <. B , y >. } <-> z = { <. B , w >. } ) )
37 33 36 anbi12d 
 |-  ( y = w -> ( ( y e. A /\ z = { <. B , y >. } ) <-> ( w e. A /\ z = { <. B , w >. } ) ) )
38 37 equsexvw 
 |-  ( E. y ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) <-> ( w e. A /\ z = { <. B , w >. } ) )
39 38 a1i 
 |-  ( ph -> ( E. y ( y = w /\ ( y e. A /\ z = { <. B , y >. } ) ) <-> ( w e. A /\ z = { <. B , w >. } ) ) )
40 16 32 39 3bitrd 
 |-  ( ph -> ( ( z e. ( A ^m { B } ) /\ w = ( z ` B ) ) <-> ( w e. A /\ z = { <. B , w >. } ) ) )
41 3 1 5 7 40 en2d 
 |-  ( ph -> ( A ^m { B } ) ~~ A )