Theorem coexg 7975

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 6298	. 2 ⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2		dmexg 7947	. . 3 ⊢ (𝐵 ∈ 𝑊 → dom 𝐵 ∈ V)
3		rnexg 7948	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
4		xpexg 7796	. . 3 ⊢ ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
5	2, 3, 4	syl2anr 609	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6		ssexg 5288	. 2 ⊢ (((𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   × cxp 5656  dom cdm 5658  ran crn 5659   ∘ ccom 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669

This theorem is used by:  coex  7976  coexd  7977  suppco  8261  fsuppco2  9432  fsuppcor  9433  mapfienlem2  9435  wemapwe  9735  cofsmo  10386  relexpsucnnr  15221  supcvg  16069  imasle  17745  setcco  18308  estrcco  18354  pwsco1mhm  19078  pwsco2mhm  19079  efmndov  19127  efmndcl  19128  symgov  19649  symgcl  19650  gsumval3lem2  20171  gsumzf1o  20177  f1lindf  22183  evls1sca  22696  tngds  25022  climcncf  25276  motplusg  29062  tocycfv  33769  smatfval  34538  eulerpartlemmf  35118  hgt750lemg  35394  cossex  39707  tgrpov  42071  erngmul  42129  erngmul-rN  42137  dvamulr  42335  dvavadd  42338  dvhmulr  42409  mendmulr  44447  relexp0a  44977  choicefi  46487  climexp  46890  dvsinax  47196  stoweidlem27  47310  stoweidlem31  47314  stoweidlem59  47342  grimco  49260  uspgrbisymrelALT  49526  rngccoALTV  49641  ringccoALTV  49675  itcoval1  50106  itcoval2  50107  itcoval3  50108  itcovalsucov  50111