Theorem coexg 7869

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 6224	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7841	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7842	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7690	. . 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 2109  Vcvv 3438   ⊆ wss 3905   × cxp 5621  dom cdm 5623  ran crn 5624   ∘ ccom 5627

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

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-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634

This theorem is referenced by:  coex  7870  coexd  7871  suppco  8146  fsuppco2  9312  fsuppcor  9313  mapfienlem2  9315  wemapwe  9612  cofsmo  10182  relexpsucnnr  14950  supcvg  15781  imasle  17445  setcco  18008  estrcco  18054  pwsco1mhm  18724  pwsco2mhm  18725  efmndov  18773  efmndcl  18774  symgov  19281  symgcl  19282  gsumval3lem2  19803  gsumzf1o  19809  f1lindf  21747  evls1sca  22226  tngds  24552  climcncf  24809  motplusg  28505  tocycfv  33064  smatfval  33764  eulerpartlemmf  34345  hgt750lemg  34624  cossex  38398  tgrpov  40730  erngmul  40788  erngmul-rN  40796  dvamulr  40994  dvavadd  40997  dvhmulr  41068  mendmulr  43160  relexp0a  43692  choicefi  45181  climexp  45590  dvsinax  45898  stoweidlem27  46012  stoweidlem31  46016  stoweidlem59  46044  grimco  47877  uspgrbisymrelALT  48143  rngccoALTV  48259  ringccoALTV  48293  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657