Theorem coexg 7873

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   × cxp 5622  dom cdm 5624  ran crn 5625   ∘ ccom 5628

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 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635

This theorem is referenced by:  coex  7874  coexd  7875  suppco  8149  fsuppco2  9309  fsuppcor  9310  mapfienlem2  9312  wemapwe  9609  cofsmo  10182  relexpsucnnr  14978  supcvg  15812  imasle  17478  setcco  18041  estrcco  18087  pwsco1mhm  18791  pwsco2mhm  18792  efmndov  18840  efmndcl  18841  symgov  19350  symgcl  19351  gsumval3lem2  19872  gsumzf1o  19878  f1lindf  21812  evls1sca  22298  tngds  24623  climcncf  24877  motplusg  28624  tocycfv  33185  smatfval  33955  eulerpartlemmf  34535  hgt750lemg  34814  cossex  38844  tgrpov  41208  erngmul  41266  erngmul-rN  41274  dvamulr  41472  dvavadd  41475  dvhmulr  41546  mendmulr  43630  relexp0a  44161  choicefi  45647  climexp  46053  dvsinax  46359  stoweidlem27  46473  stoweidlem31  46477  stoweidlem59  46505  grimco  48377  uspgrbisymrelALT  48643  rngccoALTV  48759  ringccoALTV  48793  itcoval1  49151  itcoval2  49152  itcoval3  49153  itcovalsucov  49156