Theorem coexg 7904

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 6253	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7876	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7877	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7727	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 606	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5276	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3902   × cxp 5641  dom cdm 5643  ran crn 5644   ∘ ccom 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654

This theorem is referenced by:  coex  7905  coexd  7906  suppco  8179  fsuppco2  9342  fsuppcor  9343  mapfienlem2  9345  wemapwe  9645  cofsmo  10219  relexpsucnnr  15031  supcvg  15876  imasle  17543  setcco  18106  estrcco  18152  pwsco1mhm  18856  pwsco2mhm  18857  efmndov  18905  efmndcl  18906  symgov  19414  symgcl  19415  gsumval3lem2  19936  gsumzf1o  19942  f1lindf  21861  evls1sca  22373  tngds  24695  climcncf  24949  motplusg  28698  tocycfv  33249  smatfval  34052  eulerpartlemmf  34632  hgt750lemg  34908  cossex  38968  tgrpov  41332  erngmul  41390  erngmul-rN  41398  dvamulr  41596  dvavadd  41599  dvhmulr  41670  mendmulr  43721  relexp0a  44252  choicefi  45737  climexp  46141  dvsinax  46447  stoweidlem27  46561  stoweidlem31  46565  stoweidlem59  46593  grimco  48471  uspgrbisymrelALT  48737  rngccoALTV  48853  ringccoALTV  48887  itcoval1  49245  itcoval2  49246  itcoval3  49247  itcovalsucov  49250