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 6292	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7923	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7924	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7770	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 597	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5323	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951   × cxp 5683  dom cdm 5685  ran crn 5686   ∘ ccom 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696

This theorem is referenced by:  coex  7952  coexd  7953  suppco  8231  fsuppco2  9443  fsuppcor  9444  mapfienlem2  9446  wemapwe  9737  cofsmo  10309  relexpsucnnr  15064  supcvg  15892  imasle  17568  setcco  18128  estrcco  18174  pwsco1mhm  18845  pwsco2mhm  18846  efmndov  18894  efmndcl  18895  symgov  19401  symgcl  19402  gsumval3lem2  19924  gsumzf1o  19930  f1lindf  21842  evls1sca  22327  tngds  24668  tngdsOLD  24669  climcncf  24926  motplusg  28550  tocycfv  33129  smatfval  33794  eulerpartlemmf  34377  hgt750lemg  34669  cossex  38420  tgrpov  40750  erngmul  40808  erngmul-rN  40816  dvamulr  41014  dvavadd  41017  dvhmulr  41088  mendmulr  43196  relexp0a  43729  choicefi  45205  climexp  45620  dvsinax  45928  stoweidlem27  46042  stoweidlem31  46046  stoweidlem59  46074  grimco  47880  uspgrbisymrelALT  48071  rngccoALTV  48187  ringccoALTV  48221  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsucov  48589