Theorem coexg 7881

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 6238	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7853	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7854	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7705	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 598	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5270	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 588	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   × cxp 5630  dom cdm 5632  ran crn 5633   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643

This theorem is referenced by:  coex  7882  coexd  7883  suppco  8158  fsuppco2  9318  fsuppcor  9319  mapfienlem2  9321  wemapwe  9618  cofsmo  10191  relexpsucnnr  14960  supcvg  15791  imasle  17456  setcco  18019  estrcco  18065  pwsco1mhm  18769  pwsco2mhm  18770  efmndov  18818  efmndcl  18819  symgov  19325  symgcl  19326  gsumval3lem2  19847  gsumzf1o  19853  f1lindf  21789  evls1sca  22279  tngds  24604  climcncf  24861  motplusg  28626  tocycfv  33202  smatfval  33972  eulerpartlemmf  34552  hgt750lemg  34831  cossex  38757  tgrpov  41121  erngmul  41179  erngmul-rN  41187  dvamulr  41385  dvavadd  41388  dvhmulr  41459  mendmulr  43538  relexp0a  44069  choicefi  45555  climexp  45962  dvsinax  46268  stoweidlem27  46382  stoweidlem31  46386  stoweidlem59  46414  grimco  48246  uspgrbisymrelALT  48512  rngccoALTV  48628  ringccoALTV  48662  itcoval1  49020  itcoval2  49021  itcoval3  49022  itcovalsucov  49025