Theorem coexg 7951

Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)

Assertion

Ref	Expression
coexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Proof of Theorem coexg

Step	Hyp	Ref	Expression
1		cossxp 6293	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7923	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7924	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7768	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 597	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5328	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962   × cxp 5686  dom cdm 5688  ran crn 5689   ∘ ccom 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699

This theorem is referenced by:  coex  7952  coexd  7953  suppco  8229  fsuppco2  9440  fsuppcor  9441  mapfienlem2  9443  wemapwe  9734  cofsmo  10306  relexpsucnnr  15060  supcvg  15888  imasle  17569  setcco  18136  estrcco  18184  pwsco1mhm  18857  pwsco2mhm  18858  efmndov  18906  efmndcl  18907  symgov  19415  symgcl  19416  gsumval3lem2  19938  gsumzf1o  19944  f1lindf  21859  evls1sca  22342  tngds  24683  tngdsOLD  24684  climcncf  24939  motplusg  28564  tocycfv  33111  smatfval  33755  eulerpartlemmf  34356  hgt750lemg  34647  cossex  38400  tgrpov  40730  erngmul  40788  erngmul-rN  40796  dvamulr  40994  dvavadd  40997  dvhmulr  41068  mendmulr  43172  relexp0a  43705  choicefi  45142  climexp  45560  dvsinax  45868  stoweidlem27  45982  stoweidlem31  45986  stoweidlem59  46014  grimco  47817  uspgrbisymrelALT  47998  rngccoALTV  48114  ringccoALTV  48148  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsucov  48517