Theorem coexg 7916

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3947   × cxp 5673  dom cdm 5675  ran crn 5676   ∘ ccom 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686

This theorem is referenced by:  coex  7917  suppco  8187  fsuppco2  9394  fsuppcor  9395  mapfienlem2  9397  wemapwe  9688  cofsmo  10260  relexpsucnnr  14968  supcvg  15798  imasle  17465  setcco  18029  estrcco  18077  pwsco1mhm  18709  pwsco2mhm  18710  efmndov  18758  efmndcl  18759  symgov  19245  symgcl  19246  gsumval3lem2  19768  gsumzf1o  19774  f1lindf  21368  evls1sca  21833  tngds  24155  tngdsOLD  24156  climcncf  24407  motplusg  27782  tocycfv  32255  smatfval  32763  eulerpartlemmf  33362  hgt750lemg  33654  cossex  37277  tgrpov  39607  erngmul  39665  erngmul-rN  39673  dvamulr  39871  dvavadd  39874  dvhmulr  39945  coexd  41044  mendmulr  41915  relexp0a  42452  choicefi  43884  climexp  44307  dvsinax  44615  stoweidlem27  44729  stoweidlem31  44733  stoweidlem59  44761  uspgrbisymrelALT  46519  rngccoALTV  46839  ringccoALTV  46902  itcoval1  47302  itcoval2  47303  itcoval3  47304  itcovalsucov  47307