MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mapss Structured version   Unicode version

Theorem mapss 7402
Description: Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
mapss  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( A  ^m  C
)  C_  ( B  ^m  C ) )

Proof of Theorem mapss
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 elmapi 7381 . . . . . 6  |-  ( f  e.  ( A  ^m  C )  ->  f : C --> A )
21adantl 464 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f : C
--> A )
3 simplr 753 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  A  C_  B
)
42, 3fssd 5665 . . . 4  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f : C
--> B )
5 simpll 751 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  B  e.  V )
6 elmapex 7380 . . . . . . 7  |-  ( f  e.  ( A  ^m  C )  ->  ( A  e.  _V  /\  C  e.  _V ) )
76simprd 461 . . . . . 6  |-  ( f  e.  ( A  ^m  C )  ->  C  e.  _V )
87adantl 464 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  C  e.  _V )
95, 8elmapd 7374 . . . 4  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  ( f  e.  ( B  ^m  C
)  <->  f : C --> B ) )
104, 9mpbird 232 . . 3  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f  e.  ( B  ^m  C ) )
1110ex 432 . 2  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( f  e.  ( A  ^m  C )  ->  f  e.  ( B  ^m  C ) ) )
1211ssrdv 3440 1  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( A  ^m  C
)  C_  ( B  ^m  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1836   _Vcvv 3051    C_ wss 3406   -->wf 5509  (class class class)co 6218    ^m cmap 7360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-fv 5521  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-1st 6721  df-2nd 6722  df-map 7362
This theorem is referenced by:  mapdom1  7623  ssfin3ds  8645  ingru  9126  resspsrbas  18206  resspsradd  18207  resspsrmul  18208  plyss  22704  eulerpartlem1  28529  eulerpartlemn  28543  diophrw  30897  diophin  30911  diophun  30912  eq0rabdioph  30915  eqrabdioph  30916  rabdiophlem1  30940  diophren  30952  dvnprodlem2  31949  etransclem24  32246  etransclem25  32247  etransclem26  32248  etransclem28  32250  etransclem35  32257  etransclem37  32259
  Copyright terms: Public domain W3C validator