Theorem coexg 7707

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 6135	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7681	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7682	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7535	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 600	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5216	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 590	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  Vcvv 3408   ⊆ wss 3866   × cxp 5549  dom cdm 5551  ran crn 5552   ∘ ccom 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562

This theorem is referenced by:  coex  7708  suppco  7948  fsuppco2  9019  fsuppcor  9020  mapfienlem2  9022  wemapwe  9312  cofsmo  9883  relexpsucnnr  14588  supcvg  15420  imasle  17028  setcco  17589  estrcco  17637  pwsco1mhm  18258  pwsco2mhm  18259  efmndov  18308  efmndcl  18309  symgov  18776  symgcl  18777  gsumval3lem2  19291  gsumzf1o  19297  f1lindf  20784  evls1sca  21239  tngds  23546  climcncf  23797  motplusg  26633  tocycfv  31095  smatfval  31459  eulerpartlemmf  32054  hgt750lemg  32346  cossex  36279  tgrpov  38499  erngmul  38557  erngmul-rN  38565  dvamulr  38763  dvavadd  38766  dvhmulr  38837  mendmulr  40716  relexp0a  41001  choicefi  42413  climexp  42821  dvsinax  43129  stoweidlem27  43243  stoweidlem31  43247  stoweidlem59  43275  uspgrbisymrelALT  44990  rngccoALTV  45219  ringccoALTV  45282  itcoval1  45682  itcoval2  45683  itcoval3  45684  itcovalsucov  45687