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

Theorem mapss 8441
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 ((𝐵𝑉𝐴𝐵) → (𝐴m 𝐶) ⊆ (𝐵m 𝐶))

Proof of Theorem mapss
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 elmapi 8417 . . . . . 6 (𝑓 ∈ (𝐴m 𝐶) → 𝑓:𝐶𝐴)
21adantl 482 . . . . 5 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝑓:𝐶𝐴)
3 simplr 765 . . . . 5 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝐴𝐵)
42, 3fssd 6521 . . . 4 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝑓:𝐶𝐵)
5 simpll 763 . . . . 5 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝐵𝑉)
6 elmapex 8416 . . . . . . 7 (𝑓 ∈ (𝐴m 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
76simprd 496 . . . . . 6 (𝑓 ∈ (𝐴m 𝐶) → 𝐶 ∈ V)
87adantl 482 . . . . 5 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝐶 ∈ V)
95, 8elmapd 8409 . . . 4 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → (𝑓 ∈ (𝐵m 𝐶) ↔ 𝑓:𝐶𝐵))
104, 9mpbird 258 . . 3 (((𝐵𝑉𝐴𝐵) ∧ 𝑓 ∈ (𝐴m 𝐶)) → 𝑓 ∈ (𝐵m 𝐶))
1110ex 413 . 2 ((𝐵𝑉𝐴𝐵) → (𝑓 ∈ (𝐴m 𝐶) → 𝑓 ∈ (𝐵m 𝐶)))
1211ssrdv 3970 1 ((𝐵𝑉𝐴𝐵) → (𝐴m 𝐶) ⊆ (𝐵m 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  Vcvv 3492  wss 3933  wf 6344  (class class class)co 7145  m cmap 8395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-map 8397
This theorem is referenced by:  mapdom1  8670  ssfin3ds  9740  ingru  10225  resspsrbas  20123  resspsradd  20124  resspsrmul  20125  plyss  24716  eulerpartlem1  31524  eulerpartlemn  31538  reprss  31787  poimirlem29  34802  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  poimir  34806  broucube  34807  diophrw  39234  diophin  39247  diophun  39248  eq0rabdioph  39251  eqrabdioph  39252  rabdiophlem1  39276  diophren  39288  k0004ss1  40379  ixpssmapc  41213  mapss2  41344  difmap  41346  inmap  41348  mapssbi  41352  iunmapss  41354  dvnprodlem2  42108  etransclem24  42420  etransclem25  42421  etransclem26  42422  etransclem28  42424  etransclem35  42431  etransclem37  42433  qndenserrnbllem  42456  qndenserrn  42461  hoissrrn  42708  hoissrrn2  42737  hspmbl  42788  opnvonmbllem2  42792  ovolval2lem  42802  ovolval2  42803  ovolval3  42806  ovolval4lem2  42809  ovnovollem3  42817  vonvolmbl  42820  smfmullem4  42946
  Copyright terms: Public domain W3C validator