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

Theorem mapss 7540
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 7519 . . . . . 6  |-  ( f  e.  ( A  ^m  C )  ->  f : C --> A )
21adantl 472 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f : C
--> A )
3 simplr 767 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  A  C_  B
)
42, 3fssd 5761 . . . 4  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f : C
--> B )
5 simpll 765 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  B  e.  V )
6 elmapex 7518 . . . . . . 7  |-  ( f  e.  ( A  ^m  C )  ->  ( A  e.  _V  /\  C  e.  _V ) )
76simprd 469 . . . . . 6  |-  ( f  e.  ( A  ^m  C )  ->  C  e.  _V )
87adantl 472 . . . . 5  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  C  e.  _V )
95, 8elmapd 7512 . . . 4  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  ( f  e.  ( B  ^m  C
)  <->  f : C --> B ) )
104, 9mpbird 240 . . 3  |-  ( ( ( B  e.  V  /\  A  C_  B )  /\  f  e.  ( A  ^m  C ) )  ->  f  e.  ( B  ^m  C ) )
1110ex 440 . 2  |-  ( ( B  e.  V  /\  A  C_  B )  -> 
( f  e.  ( A  ^m  C )  ->  f  e.  ( B  ^m  C ) ) )
1211ssrdv 3450 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 375    e. wcel 1898   _Vcvv 3057    C_ wss 3416   -->wf 5597  (class class class)co 6315    ^m cmap 7498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821  df-map 7500
This theorem is referenced by:  mapdom1  7763  ssfin3ds  8786  ingru  9266  resspsrbas  18688  resspsradd  18689  resspsrmul  18690  plyss  23202  eulerpartlem1  29249  eulerpartlemn  29263  poimirlem29  32014  poimirlem30  32015  poimirlem31  32016  poimirlem32  32017  poimir  32018  broucube  32019  diophrw  35646  diophin  35660  diophun  35661  eq0rabdioph  35664  eqrabdioph  35665  rabdiophlem1  35689  diophren  35701  ixpssmapc  37456  dvnprodlem2  37860  etransclem24  38161  etransclem25  38162  etransclem26  38163  etransclem28  38165  etransclem35  38172  etransclem37  38174  qndenserrnbllem  38201  qndenserrn  38206  hoissrrn  38409  hoissrrn2  38438  hspmbl  38489  opnvonmbllem2  38493
  Copyright terms: Public domain W3C validator