Theorem coexg 7836

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  Vcvv 3441   ⊆ wss 3897   × cxp 5612  dom cdm 5614  ran crn 5615   ∘ ccom 5618

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625

This theorem is referenced by:  coex  7837  suppco  8084  fsuppco2  9252  fsuppcor  9253  mapfienlem2  9255  wemapwe  9546  cofsmo  10118  relexpsucnnr  14827  supcvg  15659  imasle  17323  setcco  17887  estrcco  17935  pwsco1mhm  18559  pwsco2mhm  18560  efmndov  18608  efmndcl  18609  symgov  19079  symgcl  19080  gsumval3lem2  19594  gsumzf1o  19600  f1lindf  21127  evls1sca  21587  tngds  23909  tngdsOLD  23910  climcncf  24161  motplusg  27133  tocycfv  31604  smatfval  31984  eulerpartlemmf  32583  hgt750lemg  32875  cossex  36679  tgrpov  39009  erngmul  39067  erngmul-rN  39075  dvamulr  39273  dvavadd  39276  dvhmulr  39347  mendmulr  41264  relexp0a  41634  choicefi  43056  climexp  43471  dvsinax  43779  stoweidlem27  43893  stoweidlem31  43897  stoweidlem59  43925  uspgrbisymrelALT  45657  rngccoALTV  45886  ringccoALTV  45949  itcoval1  46349  itcoval2  46350  itcoval3  46351  itcovalsucov  46354