Theorem coexg 7908

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917   × cxp 5639  dom cdm 5641  ran crn 5642   ∘ ccom 5645

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652

This theorem is referenced by:  coex  7909  coexd  7910  suppco  8188  fsuppco2  9361  fsuppcor  9362  mapfienlem2  9364  wemapwe  9657  cofsmo  10229  relexpsucnnr  14998  supcvg  15829  imasle  17493  setcco  18052  estrcco  18098  pwsco1mhm  18766  pwsco2mhm  18767  efmndov  18815  efmndcl  18816  symgov  19321  symgcl  19322  gsumval3lem2  19843  gsumzf1o  19849  f1lindf  21738  evls1sca  22217  tngds  24543  climcncf  24800  motplusg  28476  tocycfv  33073  smatfval  33792  eulerpartlemmf  34373  hgt750lemg  34652  cossex  38417  tgrpov  40749  erngmul  40807  erngmul-rN  40815  dvamulr  41013  dvavadd  41016  dvhmulr  41087  mendmulr  43180  relexp0a  43712  choicefi  45201  climexp  45610  dvsinax  45918  stoweidlem27  46032  stoweidlem31  46036  stoweidlem59  46064  grimco  47893  uspgrbisymrelALT  48147  rngccoALTV  48263  ringccoALTV  48297  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsucov  48661