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

Theorem coexg 6733
Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
Assertion
Ref Expression
coexg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  o.  B
)  e.  _V )

Proof of Theorem coexg
StepHypRef Expression
1 cossxp 5517 . 2  |-  ( A  o.  B )  C_  ( dom  B  X.  ran  A )
2 dmexg 6713 . . 3  |-  ( B  e.  W  ->  dom  B  e.  _V )
3 rnexg 6714 . . 3  |-  ( A  e.  V  ->  ran  A  e.  _V )
4 xpexg 6584 . . 3  |-  ( ( dom  B  e.  _V  /\ 
ran  A  e.  _V )  ->  ( dom  B  X.  ran  A )  e. 
_V )
52, 3, 4syl2anr 478 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( dom  B  X.  ran  A )  e.  _V )
6 ssexg 4580 . 2  |-  ( ( ( A  o.  B
)  C_  ( dom  B  X.  ran  A )  /\  ( dom  B  X.  ran  A )  e. 
_V )  ->  ( A  o.  B )  e.  _V )
71, 5, 6sylancr 663 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  o.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1802   _Vcvv 3093    C_ wss 3459    X. cxp 4984   dom cdm 4986   ran crn 4987    o. ccom 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997
This theorem is referenced by:  coex  6734  supp0cosupp0  6938  imacosupp  6939  fsuppco2  7861  fsuppcor  7862  mapfienlem2  7864  wemapwe  8139  wemapweOLD  8140  cofsmo  8649  supcvg  13643  imasle  14794  setcco  15281  pwsco1mhm  15872  pwsco2mhm  15873  symgov  16286  symgcl  16287  gsumval3OLD  16779  gsumval3lem2  16781  gsumzf1o  16788  evls1sca  18231  f1lindf  18727  tngds  21032  climcncf  21274  motplusg  23798  eulerpartlemmf  28184  relexpsucr  28923  mendmulr  31110  climexp  31519  dvsinax  31612  stoweidlem27  31698  stoweidlem31  31702  stoweidlem59  31730  estrcco  32482  rngccoOLD  32533  ringccoOLD  32591  tgrpov  36197  erngmul  36255  erngmul-rN  36263  dvamulr  36461  dvavadd  36464  dvhmulr  36536
  Copyright terms: Public domain W3C validator