Theorem coexg 7925

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926   × cxp 5652  dom cdm 5654  ran crn 5655   ∘ ccom 5658

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665

This theorem is referenced by:  coex  7926  coexd  7927  suppco  8205  fsuppco2  9415  fsuppcor  9416  mapfienlem2  9418  wemapwe  9711  cofsmo  10283  relexpsucnnr  15044  supcvg  15872  imasle  17537  setcco  18096  estrcco  18142  pwsco1mhm  18810  pwsco2mhm  18811  efmndov  18859  efmndcl  18860  symgov  19365  symgcl  19366  gsumval3lem2  19887  gsumzf1o  19893  f1lindf  21782  evls1sca  22261  tngds  24587  climcncf  24844  motplusg  28521  tocycfv  33120  smatfval  33826  eulerpartlemmf  34407  hgt750lemg  34686  cossex  38437  tgrpov  40767  erngmul  40825  erngmul-rN  40833  dvamulr  41031  dvavadd  41034  dvhmulr  41105  mendmulr  43208  relexp0a  43740  choicefi  45224  climexp  45634  dvsinax  45942  stoweidlem27  46056  stoweidlem31  46060  stoweidlem59  46088  grimco  47902  uspgrbisymrelALT  48130  rngccoALTV  48246  ringccoALTV  48280  itcoval1  48643  itcoval2  48644  itcoval3  48645  itcovalsucov  48648