Theorem coexg 7867

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898   × cxp 5619  dom cdm 5621  ran crn 5622   ∘ ccom 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632

This theorem is referenced by:  coex  7868  coexd  7869  suppco  8144  fsuppco2  9296  fsuppcor  9297  mapfienlem2  9299  wemapwe  9596  cofsmo  10169  relexpsucnnr  14936  supcvg  15767  imasle  17431  setcco  17994  estrcco  18040  pwsco1mhm  18744  pwsco2mhm  18745  efmndov  18793  efmndcl  18794  symgov  19300  symgcl  19301  gsumval3lem2  19822  gsumzf1o  19828  f1lindf  21763  evls1sca  22241  tngds  24566  climcncf  24823  motplusg  28523  tocycfv  33087  smatfval  33831  eulerpartlemmf  34411  hgt750lemg  34690  cossex  38544  tgrpov  40870  erngmul  40928  erngmul-rN  40936  dvamulr  41134  dvavadd  41137  dvhmulr  41208  mendmulr  43304  relexp0a  43836  choicefi  45324  climexp  45732  dvsinax  46038  stoweidlem27  46152  stoweidlem31  46156  stoweidlem59  46184  grimco  48016  uspgrbisymrelALT  48282  rngccoALTV  48398  ringccoALTV  48432  itcoval1  48791  itcoval2  48792  itcoval3  48793  itcovalsucov  48796