Theorem coexg 7914

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 6262	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7886	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7887	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7737	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 608	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5283	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 598	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907   × cxp 5649  dom cdm 5651  ran crn 5652   ∘ ccom 5655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662

This theorem is referenced by:  coex  7915  coexd  7916  suppco  8190  fsuppco2  9351  fsuppcor  9352  mapfienlem2  9354  wemapwe  9654  cofsmo  10241  relexpsucnnr  15050  supcvg  15898  imasle  17565  setcco  18128  estrcco  18174  pwsco1mhm  18879  pwsco2mhm  18880  efmndov  18928  efmndcl  18929  symgov  19442  symgcl  19443  gsumval3lem2  19964  gsumzf1o  19970  f1lindf  21929  evls1sca  22440  tngds  24762  climcncf  25016  motplusg  28765  tocycfv  33337  smatfval  34097  eulerpartlemmf  34677  hgt750lemg  34953  cossex  39015  tgrpov  41379  erngmul  41437  erngmul-rN  41445  dvamulr  41643  dvavadd  41646  dvhmulr  41717  mendmulr  43768  relexp0a  44299  choicefi  45776  climexp  46180  dvsinax  46486  stoweidlem27  46600  stoweidlem31  46604  stoweidlem59  46632  grimco  48510  uspgrbisymrelALT  48776  rngccoALTV  48892  ringccoALTV  48926  itcoval1  49295  itcoval2  49296  itcoval3  49297  itcovalsucov  49300