Theorem coexg 7922

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905   × cxp 5659  dom cdm 5661  ran crn 5662   ∘ ccom 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672

This theorem is used by:  coex  7923  coexd  7924  suppco  8198  fsuppco2  9359  fsuppcor  9360  mapfienlem2  9362  wemapwe  9662  cofsmo  10257  relexpsucnnr  15067  supcvg  15915  imasle  17581  setcco  18144  estrcco  18190  pwsco1mhm  18895  pwsco2mhm  18896  efmndov  18944  efmndcl  18945  symgov  19458  symgcl  19459  gsumval3lem2  19980  gsumzf1o  19986  f1lindf  21981  evls1sca  22492  tngds  24814  climcncf  25068  motplusg  28820  tocycfv  33438  smatfval  34194  eulerpartlemmf  34774  hgt750lemg  35050  cossex  39186  tgrpov  41550  erngmul  41608  erngmul-rN  41616  dvamulr  41814  dvavadd  41817  dvhmulr  41888  mendmulr  43939  relexp0a  44470  choicefi  45945  climexp  46349  dvsinax  46655  stoweidlem27  46769  stoweidlem31  46773  stoweidlem59  46801  grimco  48682  uspgrbisymrelALT  48948  rngccoALTV  49064  ringccoALTV  49098  itcoval1  49471  itcoval2  49472  itcoval3  49473  itcovalsucov  49476